Grace/Cumulus/Algebra/Group/Coset.g17

Open in Workbench Download source

Imports

Subgroup

Declarations

Source

1-- Left and right cosets of a subgroup: each coset is generated by any of2-- its members, two cosets that share a point coincide, membership through3-- the difference of representatives, and the set of all left cosets4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Algebra.Group.Coset10import Subgroup1112-- The left coset g * H and the right coset H * g of a subset H of G.13def leftCoset (G g H : Set) : Set := { y ∈ G.carrier | ∃ h ∈ H, y = G.mul(g, h) }14def rightCoset (G g H : Set) : Set := { y ∈ G.carrier | ∃ h ∈ H, y = G.mul(h, g) }1516-- The set of all left cosets of H.17def leftCosets (G H : Set) : Set :=18  { C ∈ 𝒫(G.carrier) | ∃ g ∈ G.carrier, C = leftCoset(G, g, H) }1920-- The left coset leftCoset(G, g, H) is written g • H wherever a hypothesis21-- in scope supplies the group.22notation infixr 73 "•" => leftCoset(G, _, _) via hypothesis Group(G) for G.carrier23notation infixr 73 "•" => leftCoset(G, _, _) via hypothesis Subgroup(H, G) for G.carrier2425theorem leftCoset.subset (G g H : Set)26  shows leftCoset(G, g, H) ⊆ G.carrier27proof28  intros y hy29  have parts := leftCoset.membership.forward with hy30  exact parts.left3132theorem rightCoset.subset (G g H : Set)33  shows rightCoset(G, g, H) ⊆ G.carrier34proof35  intros y hy36  have parts := rightCoset.membership.forward with hy37  exact parts.left3839theorem leftCosets.subset_powerset (G H : Set)40  shows leftCosets(G, H) ⊆ 𝒫(G.carrier)41proof42  intros C hC43  have parts := leftCosets.membership.forward with hC44  exact parts.left4546theorem leftCosets.coset_member (G H g : Set)47  requires hg : g ∈ G.carrier48  shows leftCoset(G, g, H) ∈ leftCosets(G, H)49proof50  have subset := leftCoset.subset at G, g, H51  have bounded := powerset.membership_iff.backward with subset52  exact leftCosets.membership.backward with ⟨bounded, g, hg, rfl⟩5354section Cosets55variable (G H : Set)56hypothesis group : Group(G)57hypothesis subgroup : Subgroup(H, G)5859theorem leftCoset.mul_mem (g : G) (h : H)60  shows g * h ∈ g • H61proof62  have product : g * h ∈ G by typecheck63  have hIn : h ∈ H by assumption64  exact leftCoset.membership.backward with ⟨product, h, hIn, rfl⟩6566theorem rightCoset.mul_mem (g : G) (h : H)67  shows h * g ∈ rightCoset(G, g, H)68proof69  have product : h * g ∈ G by typecheck70  have hIn : h ∈ H by assumption71  exact rightCoset.membership.backward with ⟨product, h, hIn, rfl⟩7273theorem leftCoset.self (g : G)74  shows g ∈ g • H75proof76  have product : g * G.one ∈ g • H := leftCoset.mul_mem with *77  rwa mul_one at product7879theorem rightCoset.self (g : G)80  shows g ∈ rightCoset(G, g, H)81proof82  have product : G.one * g ∈ rightCoset(G, g, H) := rightCoset.mul_mem with *83  rwa one_mul at product8485-- Membership in a coset through the difference of representatives.86theorem leftCoset.mem_iff (x y : G)87  shows y ∈ x • H ↔ x⁻¹ * y ∈ H88proof89  constructor90  . intro member91    obtain ⟨yIn, h, hH, yEq⟩ := leftCoset.membership.forward with member92    rw [yEq, inv_mul_cancel_left]93    exact hH94  . intro member95    have cancel : x * (x⁻¹ * y) = y := mul_inv_cancel_left with *96    have yIn : y ∈ G by assumption97    apply leftCoset.membership.backward98    refine ⟨yIn, x⁻¹ * y, member, ?_⟩99    symm100    exact cancel101102theorem rightCoset.mem_iff (x y : G)103  shows y ∈ rightCoset(G, x, H) ↔ y * x⁻¹ ∈ H104proof105  constructor106  . intro member107    obtain ⟨yIn, h, hH, yEq⟩ := rightCoset.membership.forward with member108    rw [yEq, mul_inv_cancel_right]109    exact hH110  . intro member111    have cancel : y * x⁻¹ * x = y := inv_mul_cancel_right with *112    have yIn : y ∈ G by assumption113    apply rightCoset.membership.backward114    refine ⟨yIn, y * x⁻¹, member, ?_⟩115    symm116    exact cancel117118-- Any member of a coset generates it.119theorem leftCoset.of_member (g : G) (y : Set)120  requires hy : y ∈ g • H121  shows y • H = g • H122proof123  obtain ⟨yIn, h0, h0In, yEq⟩ := leftCoset.membership.forward with hy124  ext z125  constructor126  . intro hz127    obtain ⟨zIn, h, hH, zEq⟩ := leftCoset.membership.forward with hz128    have product : h0 * h ∈ H := Subgroup.mul_mem with *129    apply leftCoset.membership.backward130    refine ⟨zIn, h0 * h, product, ?_⟩131    rw [zEq, yEq, mul_assoc]132    rfl133  . intro hz134    obtain ⟨zIn, h, hH, zEq⟩ := leftCoset.membership.forward with hz135    have product : h0⁻¹ * h ∈ H := Subgroup.mul_mem with *136    apply leftCoset.membership.backward137    refine ⟨zIn, h0⁻¹ * h, product, ?_⟩138    rw [zEq, yEq, mul_assoc, mul_inv_cancel_left]139    rfl140141theorem leftCoset.eq_of_common (g k : G) (z : Set)142  requires hz : z ∈ g • H143  requires hz2 : z ∈ k • H144  shows g • H = k • H145proof146  have first : z • H = g • H := leftCoset.of_member with *147  have second : z • H = k • H := leftCoset.of_member with *148  rwa first at second149150theorem leftCoset.eq_iff (x y : G)151  shows x • H = y • H ↔ x⁻¹ * y ∈ H152proof153  have criterion : y ∈ x • H ↔ x⁻¹ * y ∈ H := leftCoset.mem_iff with *154  have selfY : y ∈ y • H := leftCoset.self with *155  constructor156  . intro equal157    have member : y ∈ x • H by rwa equal158    exact criterion.forward with member159  . intro member160    have inside := criterion.backward with member161    have equal : y • H = x • H := leftCoset.of_member with *162    symm163    exact equal164165theorem leftCoset.one166  shows G.one • H = H167proof168  ext y169  constructor170  . intro hy171    obtain ⟨yIn, h, hH, yEq⟩ := leftCoset.membership.forward with hy172    rw [yEq, one_mul]173    exact hH174  . intro hy175    have yIn : y ∈ G := Subgroup.mem_carrier with *176    have identity : G.one * y = y := one_mul with *177    apply leftCoset.membership.backward178    refine ⟨yIn, y, hy, ?_⟩179    symm180    exact identity181182theorem leftCoset.eq_self_iff (x : G)183  shows x • H = H ↔ x ∈ H184proof185  have criterion : x • H = G.one • H ↔ x⁻¹ * G.one ∈ H :=186    leftCoset.eq_iff with *187  have inverseCriterion : x⁻¹ ∈ H ↔ x ∈ H := Subgroup.inv_mem_iff with *188  rw [leftCoset.one, mul_one] at criterion189  constructor190  . intro equal191    have member := criterion.forward with equal192    exact inverseCriterion.forward with member193  . intro member194    have inverse := inverseCriterion.backward with member195    exact criterion.backward with inverse196197theorem leftCosets.representative (C : Set)198  requires hC : C ∈ leftCosets(G, H)199  shows ∃ g ∈ G, g ∈ C200proof201  obtain ⟨bound, g, hg, same⟩ := leftCosets.membership.forward with hC202  have self : g ∈ g • H := leftCoset.self with *203  witness g204  constructor205  . exact hg206  . rw same207    exact self208209end Cosets210