{"id":859,"date":"2021-10-15T05:00:22","date_gmt":"2021-10-15T03:00:22","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=859"},"modified":"2021-10-04T17:39:24","modified_gmt":"2021-10-04T15:39:24","slug":"isomorfismo-entre-relaciones-de-equivalencia-y-particiones","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/isomorfismo-entre-relaciones-de-equivalencia-y-particiones\/","title":{"rendered":"Isomorfismo entre relaciones de equivalencia y particiones"},"content":{"rendered":"<p>Este ejercicio es el 16\u00ba de una serie cuyo objetivo es demostrar que el tipo de las particiones de un conjunto <code>X<\/code> es isomorfo al tipo de las relaciones de equivalencia sobre <code>X<\/code>.<\/p>\n<p>Los anteriores son<br \/>\n1. <a href=\"https:\/\/bit.ly\/2YfsvBZ\">Igualdad de bloques de una partici\u00f3n cuando tienen elementos comunes<\/a>.<br \/>\n2. <a href=\"https:\/\/bit.ly\/3l2onxZ\">Pertenencia a bloques de una partici\u00f3n con elementos comunes<\/a>.<br \/>\n3. <a href=\"https:\/\/bit.ly\/3FlVKUy\">Pertenencia a su propia clase de equivalencia<\/a>.<br \/>\n4. <a href=\"https:\/\/bit.ly\/3uwL1Sd\">Las clases de equivalencia contienen a las clases de equivalencia de sus elementos<\/a>.<br \/>\n5. <a href=\"https:\/\/bit.ly\/2Y7FJjO\">Las clases de equivalencia son iguales a las de sus elementos<\/a>.<br \/>\n6. <a href=\"https:\/\/bit.ly\/39YHuCv\">Las clases de equivalencia son no vac\u00edas<\/a>.<br \/>\n7. <a href=\"https:\/\/bit.ly\/3a1wmFc\">Las clases de equivalencia recubren el conjunto<\/a>.<br \/>\n8. <a href=\"https:\/\/bit.ly\/3FfAX54\">Las clases de equivalencia son disjuntas<\/a>.<br \/>\n9. <a href=\"https:\/\/bit.ly\/3FmAtKv\">El cociente aplica relaciones de equivalencia en particiones<\/a>.<br \/>\n10. <a href=\"https:\/\/bit.ly\/3B2lLpc\">Las relaciones definidas por particiones son reflexivas<\/a>.<br \/>\n11. <a href=\"https:\/\/bit.ly\/2ZWmY3O\">Las relaciones definidas por particiones son sim\u00e9tricas<\/a>.<br \/>\n12. <a href=\"https:\/\/bit.ly\/3B9e54J\">Las relaciones definidas por particiones son transitivas<\/a>.<br \/>\n13. <a href=\"https:\/\/bit.ly\/3a8AuTP\">Aplicaci\u00f3n de particiones en relaciones de equivalencia<\/a>.<br \/>\n14. <a href=\"https:\/\/bit.ly\/3l8kwz8\">La funci\u00f3n <code>relacionP<\/code> es inversa por la izquierda de la funci\u00f3n <code>cociente<\/code><\/a><br \/>\n15. <a href=\"https:\/\/bit.ly\/3FfqzKo\">La funci\u00f3n <code>relacionP<\/code> es inversa por la derecha de la funci\u00f3n <code>cociente<\/code><\/a>.<\/p>\n<p>En Lean, el tipo de los isomorfimos de un tipo <code>\u03b1<\/code> en un tipo <code>\u03b2<\/code> est\u00e1 definido mediante la siguiente estructura<\/p>\n<pre lang=\"lean\">\n   structure equiv (\u03b1 : Sort*) (\u03b2 : Sort*) :=\n   (to_fun    : \u03b1 \u2192 \u03b2)\n   (inv_fun   : \u03b2 \u2192 \u03b1)\n   (left_inv  : left_inverse inv_fun to_fun)\n   (right_inv : right_inverse inv_fun to_fun)\n<\/pre>\n<p>y se <code>equiv \u03b1 \u03b2<\/code> se denota por <code>\u03b1 \u2243 \u03b2<\/code>. 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.<\/p>\n<p>Demostrar que los tipos de las relaciones de equivalencia sobre <code>A<\/code> y el de las particiones de <code>A<\/code> son isomorfos.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n<pre lang=\"lean\">\nimport tactic\n\n@[ext] structure particion (A : Type) :=\n(Bloques    : set (set A))\n(Hno_vacios : \u2200 X \u2208 Bloques, (X : set A).nonempty)\n(Hrecubren  : \u2200 a, \u2203 X \u2208 Bloques, a \u2208 X)\n(Hdisjuntos : \u2200 X Y \u2208 Bloques, (X \u2229 Y : set A).nonempty \u2192 X = Y)\n\nnamespace particion\n\nvariable  {A : Type}\nvariables {X Y : set A}\nvariable  {P : particion A}\nvariable  (R : A \u2192 A \u2192 Prop)\n\ndef clase (a : A) :=\n  {b : A | R b a}\n\ndef clases : (A \u2192 A \u2192 Prop) \u2192 set (set A) :=\n  \u03bb R, {B : set A | \u2203 x : A, B = clase R x}\n\nlemma pertenece_clase_syss\n  {a b : A}\n  : b \u2208 clase R a \u2194 R b a :=\nby refl\n\nlemma clases_no_vacias\n  (hR: equivalence R)\n  : \u2200 (X : set A), X \u2208 clases R \u2192 X.nonempty :=\nbegin\n  rintros _ \u27e8a, rfl\u27e9,\n  use a,\n  rw pertenece_clase_syss,\n  apply hR.1,\nend\n\nlemma clases_recubren\n  (hR: equivalence R)\n  : \u2200 a, \u2203 X \u2208 clases R, a \u2208 X :=\nbegin\n  intro a,\n  use clase R a,\n  split,\n  { use a, },\n  { exact hR.1 a, },\nend\n\nlemma subclase_si_pertenece\n  {R : A \u2192 A \u2192 Prop}\n  (hR: equivalence R)\n  {a b : A}\n  : a \u2208 clase R b \u2192 clase R a \u2286 clase R b :=\n\u03bb hab z hza, hR.2.2 hza hab\n\nlemma clases_iguales_si_pertenece\n  {R : A \u2192 A \u2192 Prop}\n  (hR: equivalence R)\n  {a b : A}\n  : a \u2208 clase R b \u2192 clase R a = clase R b :=\n\u03bb hab, set.subset.antisymm\n        (subclase_si_pertenece hR hab)\n        (subclase_si_pertenece hR (hR.2.1 hab))\n\nlemma clases_disjuntas\n  (hR: equivalence R)\n  : \u2200 X Y \u2208 clases R, (X \u2229 Y : set A).nonempty \u2192 X = Y :=\nbegin\n  rintros X Y \u27e8a, rfl\u27e9 \u27e8b, rfl\u27e9 \u27e8c, hca, hcb\u27e9,\n  exact clases_iguales_si_pertenece hR (hR.2.2 (hR.2.1 hca) hcb),\nend\n\ndef cociente : {R : A \u2192 A \u2192 Prop \/\/ equivalence R} \u2192 particion A :=\n  \u03bb R, { Bloques    := {B : set A | \u2203 x : A, B = clase R.1 x},\n         Hno_vacios := clases_no_vacias R.1 R.2,\n         Hrecubren  := clases_recubren R.1 R.2,\n         Hdisjuntos := clases_disjuntas R.1 R.2, }\n\ndef relacion : (particion A) \u2192 (A \u2192 A \u2192 Prop) :=\n  \u03bb P a b, \u2200 X \u2208 Bloques P, a \u2208 X \u2192 b \u2208 X\n\nlemma reflexiva\n  (P : particion A)\n  : reflexive (relacion P) :=\n\u03bb a X hXC haX, haX\n\nlemma iguales_si_comun\n  (hX : X \u2208 Bloques P)\n  (hY : Y \u2208 Bloques P)\n  {a : A}\n  (haX : a \u2208 X)\n  (haY : a \u2208 Y)\n  : X = Y :=\nHdisjuntos P X Y hX hY \u27e8a, haX, haY\u27e9\n\nlemma pertenece_si_pertenece\n  (hX : X \u2208 Bloques P)\n  (hY : Y \u2208 Bloques P)\n  {a b : A}\n  (haX : a \u2208 X)\n  (haY : a \u2208 Y)\n  (hbX : b \u2208 X)\n  : b \u2208 Y :=\nbegin\n  convert hbX,\n  exact iguales_si_comun hY hX haY haX,\nend\n\nlemma simetrica\n  (P : particion A)\n  : symmetric (relacion P) :=\nbegin\n  intros a b h X hX hbX,\n  obtain \u27e8Y, hY, haY\u27e9 := Hrecubren P a,\n  specialize h Y hY haY,\n  exact pertenece_si_pertenece hY hX h hbX haY,\nend\n\nlemma transitiva\n  (P : particion A)\n  : transitive (relacion P) :=\n\u03bb a b c hab hbc X hX haX, hbc X hX (hab X hX haX)\n\ndef relacionP : particion A \u2192 {R : A \u2192 A \u2192 Prop \/\/ equivalence R} :=\n  \u03bb P, \u27e8\u03bb a b, \u2200 X \u2208 Bloques P, a \u2208 X \u2192 b \u2208 X,\n        \u27e8reflexiva P, simetrica P, transitiva P\u27e9\u27e9\n\nlemma inversa_izq :\n  function.left_inverse relacionP (@cociente A) :=\nbegin\n  rintro \u27e8R, hR\u27e9,\n  simp [relacionP, cociente],\n  ext a b,\n  exact \u27e8\u03bb hab, hR.2.1 (hab a (hR.1 a)),\n         \u03bb hab c hac, hR.2.2 (hR.2.1 hab) hac\u27e9,\nend\n\nlemma inversa_dcha :\n  function.right_inverse relacionP (@cociente A) :=\nbegin\n  intro P,\n  ext X,\n  show (\u2203 (a : A), X = clase _ a) \u2194 X \u2208 Bloques P,\n  split,\n  { rintro \u27e8a, rfl\u27e9,\n    obtain \u27e8X, hX, haX\u27e9 := Hrecubren P a,\n    convert hX,\n    ext b,\n    rw pertenece_clase_syss,\n    split,\n    { intro hba,\n      obtain \u27e8Y, hY, hbY\u27e9 := Hrecubren P b,\n      specialize hba Y hY hbY,\n      convert hbY,\n      exact iguales_si_comun hX hY haX hba, },\n    { intros hbX Y hY hbY,\n      apply pertenece_si_pertenece hX hY hbX hbY haX, }},\n  { intro hX,\n    rcases Hno_vacios P X hX with \u27e8a, ha\u27e9,\n    use a,\n    ext b,\n    split,\n    { intro hbX,\n      rw pertenece_clase_syss,\n      intros Y hY hbY,\n      exact pertenece_si_pertenece hX hY hbX hbY ha, },\n    { rw pertenece_clase_syss,\n      intro hba,\n      obtain \u27e8Y, hY, hbY\u27e9 := Hrecubren P b,\n      specialize hba Y hY hbY,\n      exact pertenece_si_pertenece hY hX hba ha hbY, }}\nend\n\ntheorem equivalencia_particiones\n  (A : Type)\n  : {R : A \u2192 A \u2192 Prop \/\/ equivalence R} \u2243 particion A :=\nsorry\n\nend particion\n<\/pre>\n<p>[expand title=\u00bbSoluciones con Lean\u00bb]<\/p>\n<pre lang=\"lean\">\r\nimport tactic\r\n\r\n@[ext] structure particion (A : Type) :=\r\n(Bloques    : set (set A))\r\n(Hno_vacios : \u2200 X \u2208 Bloques, (X : set A).nonempty)\r\n(Hrecubren  : \u2200 a, \u2203 X \u2208 Bloques, a \u2208 X)\r\n(Hdisjuntos : \u2200 X Y \u2208 Bloques, (X \u2229 Y : set A).nonempty \u2192 X = Y)\r\n\r\nnamespace particion\r\n\r\nvariable  {A : Type}\r\nvariables {X Y : set A}\r\nvariable  {P : particion A}\r\nvariable  (R : A \u2192 A \u2192 Prop)\r\n\r\ndef clase (a : A) :=\r\n  {b : A | R b a}\r\n\r\ndef clases : (A \u2192 A \u2192 Prop) \u2192 set (set A) :=\r\n  \u03bb R, {B : set A | \u2203 x : A, B = clase R x}\r\n\r\nlemma pertenece_clase_syss\r\n  {a b : A}\r\n  : b \u2208 clase R a \u2194 R b a :=\r\nby refl\r\n\r\nlemma clases_no_vacias\r\n  (hR: equivalence R)\r\n  : \u2200 (X : set A), X \u2208 clases R \u2192 X.nonempty :=\r\nbegin\r\n  rintros _ \u27e8a, rfl\u27e9,\r\n  use a,\r\n  rw pertenece_clase_syss,\r\n  apply hR.1,\r\nend\r\n\r\nlemma clases_recubren\r\n  (hR: equivalence R)\r\n  : \u2200 a, \u2203 X \u2208 clases R, a \u2208 X :=\r\nbegin\r\n  intro a,\r\n  use clase R a,\r\n  split,\r\n  { use a, },\r\n  { exact hR.1 a, },\r\nend\r\n\r\nlemma subclase_si_pertenece\r\n  {R : A \u2192 A \u2192 Prop}\r\n  (hR: equivalence R)\r\n  {a b : A}\r\n  : a \u2208 clase R b \u2192 clase R a \u2286 clase R b :=\r\n\u03bb hab z hza, hR.2.2 hza hab\r\n\r\nlemma clases_iguales_si_pertenece\r\n  {R : A \u2192 A \u2192 Prop}\r\n  (hR: equivalence R)\r\n  {a b : A}\r\n  : a \u2208 clase R b \u2192 clase R a = clase R b :=\r\n\u03bb hab, set.subset.antisymm\r\n        (subclase_si_pertenece hR hab)\r\n        (subclase_si_pertenece hR (hR.2.1 hab))\r\n\r\nlemma clases_disjuntas\r\n  (hR: equivalence R)\r\n  : \u2200 X Y \u2208 clases R, (X \u2229 Y : set A).nonempty \u2192 X = Y :=\r\nbegin\r\n  rintros X Y \u27e8a, rfl\u27e9 \u27e8b, rfl\u27e9 \u27e8c, hca, hcb\u27e9,\r\n  exact clases_iguales_si_pertenece hR (hR.2.2 (hR.2.1 hca) hcb),\r\nend\r\n\r\ndef cociente : {R : A \u2192 A \u2192 Prop \/\/ equivalence R} \u2192 particion A :=\r\n  \u03bb R, { Bloques    := {B : set A | \u2203 x : A, B = clase R.1 x},\r\n         Hno_vacios := clases_no_vacias R.1 R.2,\r\n         Hrecubren  := clases_recubren R.1 R.2,\r\n         Hdisjuntos := clases_disjuntas R.1 R.2, }\r\n\r\ndef relacion : (particion A) \u2192 (A \u2192 A \u2192 Prop) :=\r\n  \u03bb P a b, \u2200 X \u2208 Bloques P, a \u2208 X \u2192 b \u2208 X\r\n\r\nlemma reflexiva\r\n  (P : particion A)\r\n  : reflexive (relacion P) :=\r\n\u03bb a X hXC haX, haX\r\n\r\nlemma iguales_si_comun\r\n  (hX : X \u2208 Bloques P)\r\n  (hY : Y \u2208 Bloques P)\r\n  {a : A}\r\n  (haX : a \u2208 X)\r\n  (haY : a \u2208 Y)\r\n  : X = Y :=\r\nHdisjuntos P X Y hX hY \u27e8a, haX, haY\u27e9\r\n\r\nlemma pertenece_si_pertenece\r\n  (hX : X \u2208 Bloques P)\r\n  (hY : Y \u2208 Bloques P)\r\n  {a b : A}\r\n  (haX : a \u2208 X)\r\n  (haY : a \u2208 Y)\r\n  (hbX : b \u2208 X)\r\n  : b \u2208 Y :=\r\nbegin\r\n  convert hbX,\r\n  exact iguales_si_comun hY hX haY haX,\r\nend\r\n\r\nlemma simetrica\r\n  (P : particion A)\r\n  : symmetric (relacion P) :=\r\nbegin\r\n  intros a b h X hX hbX,\r\n  obtain \u27e8Y, hY, haY\u27e9 := Hrecubren P a,\r\n  specialize h Y hY haY,\r\n  exact pertenece_si_pertenece hY hX h hbX haY,\r\nend\r\n\r\nlemma transitiva\r\n  (P : particion A)\r\n  : transitive (relacion P) :=\r\n\u03bb a b c hab hbc X hX haX, hbc X hX (hab X hX haX)\r\n\r\ndef relacionP : particion A \u2192 {R : A \u2192 A \u2192 Prop \/\/ equivalence R} :=\r\n  \u03bb P, \u27e8\u03bb a b, \u2200 X \u2208 Bloques P, a \u2208 X \u2192 b \u2208 X,\r\n        \u27e8reflexiva P, simetrica P, transitiva P\u27e9\u27e9\r\n\r\nlemma inversa_izq :\r\n  function.left_inverse relacionP (@cociente A) :=\r\nbegin\r\n  rintro \u27e8R, hR\u27e9,\r\n  simp [relacionP, cociente],\r\n  ext a b,\r\n  exact \u27e8\u03bb hab, hR.2.1 (hab a (hR.1 a)),\r\n         \u03bb hab c hac, hR.2.2 (hR.2.1 hab) hac\u27e9,\r\nend\r\n\r\nlemma inversa_dcha :\r\n  function.right_inverse relacionP (@cociente A) :=\r\nbegin\r\n  intro P,\r\n  ext X,\r\n  show (\u2203 (a : A), X = clase _ a) \u2194 X \u2208 Bloques P,\r\n  split,\r\n  { rintro \u27e8a, rfl\u27e9,\r\n    obtain \u27e8X, hX, haX\u27e9 := Hrecubren P a,\r\n    convert hX,\r\n    ext b,\r\n    rw pertenece_clase_syss,\r\n    split,\r\n    { intro hba,\r\n      obtain \u27e8Y, hY, hbY\u27e9 := Hrecubren P b,\r\n      specialize hba Y hY hbY,\r\n      convert hbY,\r\n      exact iguales_si_comun hX hY haX hba, },\r\n    { intros hbX Y hY hbY,\r\n      apply pertenece_si_pertenece hX hY hbX hbY haX, }},\r\n  { intro hX,\r\n    rcases Hno_vacios P X hX with \u27e8a, ha\u27e9,\r\n    use a,\r\n    ext b,\r\n    split,\r\n    { intro hbX,\r\n      rw pertenece_clase_syss,\r\n      intros Y hY hbY,\r\n      exact pertenece_si_pertenece hX hY hbX hbY ha, },\r\n    { rw pertenece_clase_syss,\r\n      intro hba,\r\n      obtain \u27e8Y, hY, hbY\u27e9 := Hrecubren P b,\r\n      specialize hba Y hY hbY,\r\n      exact pertenece_si_pertenece hY hX hba ha hbY, }}\r\nend\r\n\r\ntheorem equivalencia_particiones\r\n  (A : Type)\r\n  : {R : A \u2192 A \u2192 Prop \/\/ equivalence R} \u2243 particion A :=\r\n{ to_fun    := cociente,\r\n  inv_fun   := relacionP,\r\n  left_inv  := inversa_izq,\r\n  right_inv := inversa_dcha, }\r\n\r\nend particion\r\n<\/pre>\n<p>Se puede interactuar con la prueba anterior en <a href=\"https:\/\/leanprover-community.github.io\/lean-web-editor\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus\/main\/src\/Isomorfismo_entre_relaciones_de_equivalencia_y_particiones.lean\" rel=\"noopener noreferrer\" target=\"_blank\">esta sesi\u00f3n con Lean<\/a>.<\/p>\n<p>En los comentarios se pueden escribir otras soluciones, escribiendo el c\u00f3digo entre una l\u00ednea con &#60;pre lang=&quot;lean&quot;&#62; y otra con &#60;\/pre&#62;<br \/>\n[\/expand]<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Este ejercicio es el 16\u00ba 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\u00f3n cuando tienen elementos comunes. 2. Pertenencia a bloques de una partici\u00f3n 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\u00edas. 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&#8230;<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":""},"categories":[281,30],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/859"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/comments?post=859"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/859\/revisions"}],"predecessor-version":[{"id":860,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/859\/revisions\/860"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=859"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=859"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=859"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}