Isomorfismo entre relaciones de equivalencia y particiones

Este ejercicio es el 16º de una serie cuyo objetivo es demostrar que el tipo de las particiones de un conjunto X es isomorfo al tipo de las relaciones de equivalencia sobre X.

Los anteriores son
1. Igualdad de bloques de una partición cuando tienen elementos comunes.
2. Pertenencia a bloques de una partición con elementos comunes.
3. Pertenencia a su propia clase de equivalencia.
4. Las clases de equivalencia contienen a las clases de equivalencia de sus elementos.
5. Las clases de equivalencia son iguales a las de sus elementos.
6. Las clases de equivalencia son no vacías.
7. Las clases de equivalencia recubren el conjunto.
8. Las clases de equivalencia son disjuntas.
9. El cociente aplica relaciones de equivalencia en particiones.
10. Las relaciones definidas por particiones son reflexivas.
11. Las relaciones definidas por particiones son simétricas.
12. Las relaciones definidas por particiones son transitivas.
13. Aplicación de particiones en relaciones de equivalencia.
14. La función relacionP es inversa por la izquierda de la función cociente
15. La función relacionP es inversa por la derecha de la función cociente.

En Lean, el tipo de los isomorfimos de un tipo α en un tipo β está definido mediante la siguiente estructura

y se equiv α β se denota por α ≃ β. Por tanto, para demostrar que los dos tipos don isomorfos hay que definir dos funciones entre ellos y demostrar que una es la inversa de la otra.

Demostrar que los tipos de las relaciones de equivalencia sobre A y el de las particiones de A son isomorfos.

Para ello, completar la siguiente teoría de Lean:

[expand title=»Soluciones con Lean»]

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

La función `relacionP` es inversa por la derecha de la función `cociente`

Este ejercicio es el 15º de una serie cuyo objetivo es demostrar que el tipo de las particiones de un conjunto X es isomorfo al tipo de las relaciones de equivalencia sobre X.

Los anteriores son
1. Igualdad de bloques de una partición cuando tienen elementos comunes.
2. Pertenencia a bloques de una partición con elementos comunes.
3. Pertenencia a su propia clase de equivalencia.
4. Las clases de equivalencia contienen a las clases de equivalencia de sus elementos.
5. Las clases de equivalencia son iguales a las de sus elementos.
6. Las clases de equivalencia son no vacías.
7. Las clases de equivalencia recubren el conjunto.
8. Las clases de equivalencia son disjuntas.
9. El cociente aplica relaciones de equivalencia en particiones.
10. Las relaciones definidas por particiones son reflexivas.
11. Las relaciones definidas por particiones son simétricas.
12. Las relaciones definidas por particiones son transitivas.
13. Aplicación de particiones en relaciones de equivalencia.
14. La función relacionP es inversa por la izquierda de la función cociente

En los ejercicios 9 y 13 se han definido las funciones

tales que
+ cociente R es el conjunto cociente de la relación de equivalencia R y
+ relacionP P es la relación de equivalencia definida por la partición P de forma que los elementos relacionados son los que pertenecen a los mismos bloques de P.

Demostrar que relacionP es inversa por la derecha de cociente.

Para ello, completar la siguiente teoría de Lean:

[expand title=»Soluciones con Lean»]

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

La función `relacionP` es inversa por la izquierda de la función `cociente`

Este ejercicio es el 14º de una serie cuyo objetivo es demostrar que el tipo de las particiones de un conjunto X es isomorfo al tipo de las relaciones de equivalencia sobre X.

Los anteriores son
1. Igualdad de bloques de una partición cuando tienen elementos comunes.
2. Pertenencia a bloques de una partición con elementos comunes.
3. Pertenencia a su propia clase de equivalencia.
4. Las clases de equivalencia contienen a las clases de equivalencia de sus elementos.
5. Las clases de equivalencia son iguales a las de sus elementos.
6. Las clases de equivalencia son no vacías.
7. Las clases de equivalencia recubren el conjunto.
8. Las clases de equivalencia son disjuntas.
9. El cociente aplica relaciones de equivalencia en particiones.
10. Las relaciones definidas por particiones son reflexivas.
11. Las relaciones definidas por particiones son simétricas.
12. Las relaciones definidas por particiones son transitivas.
13. Aplicación de particiones en relaciones de equivalencia.

En los ejercicios 9 y 13 se han definido las funciones

tales que

  • cociente R es el conjunto cociente de la relación de equivalencia R y
  • relacionP P es la relación de equivalencia definida por la partición P de forma que los elementos relacionados son los que pertenecen a los mismos bloques de P.

Demostrar que relacionP es inversa por la izquierda de cociente.

Para ello, completar la siguiente teoría de Lean:

[expand title=»Soluciones con Lean»]

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

Aplicación de particiones en relaciones de equivalencia

Este ejercicio es el 13º de una serie cuyo objetivo es demostrar que el tipo de las particiones de un conjunto X es isomorfo al tipo de las relaciones de equivalencia sobre X.

Los anteriores son
1. Igualdad de bloques de una partición cuando tienen elementos comunes.
2. Pertenencia a bloques de una partición con elementos comunes.
3. Pertenencia a su propia clase de equivalencia.
4. Las clases de equivalencia contienen a las clases de equivalencia de sus elementos.
5. Las clases de equivalencia son iguales a las de sus elementos.
6. Las clases de equivalencia son no vacías.
7. Las clases de equivalencia recubren el conjunto.
8. Las clases de equivalencia son disjuntas.
9. El cociente aplica relaciones de equivalencia en particiones.
10. Las relaciones definidas por particiones son reflexivas.
11. Las relaciones definidas por particiones son simétricas.
12. Las relaciones definidas por particiones son transitivas.

Definir la función

tal que relacionP P es la relación de equivalencia definida por la partición P.

Para ello, completar la siguiente teoría de Lean:

[expand title=»Soluciones con Lean»]

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

Las relaciones definidas por particiones son transitivas

Este ejercicio es el 12º de una serie cuyo objetivo es demostrar que el tipo de las particiones de un conjunto X es isomorfo al tipo de las relaciones de equivalencia sobre X.

Los anteriores son
1. Igualdad de bloques de una partición cuando tienen elementos comunes.
2. Pertenencia a bloques de una partición con elementos comunes.
3. Pertenencia a su propia clase de equivalencia.
4. Las clases de equivalencia contienen a las clases de equivalencia de sus elementos.
5. Las clases de equivalencia son iguales a las de sus elementos.
6. Las clases de equivalencia son no vacías.
7. Las clases de equivalencia recubren el conjunto.
8. Las clases de equivalencia son disjuntas.
9. El cociente aplica relaciones de equivalencia en particiones.
10. Las relaciones definidas por particiones son reflexivas.
11. Las relaciones definidas por particiones son simétricas.

Demostrar que la relación definida por una partición es transitiva.

Para ello, completar la siguiente teoría de Lean:

[expand title=»Soluciones con Lean»]

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]