Grace/Cumulus/Algebra/Group/Subgroup.g17

Open in Workbench Download source

Imports

Basic · Set.Core

Declarations

Source

1-- Subgroups: subsets of a group containing the unit and closed under the2-- operation and inverses, the subgroups every group has, intersections,3-- and the one-step criterion4-- 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.Subgroup10import Basic11import Set.Core1213-- Subgroup(H, G): H is a subgroup of the group G. Under this hypothesis a14-- binder (h : H) is a set variable with h ∈ H, and h * k and h⁻¹ are the15-- operation and inverse of G.16predicate Subgroup (H G : Set) :=17  Group(G) ∧ H ⊆ G.carrier ∧ G.one ∈ H ∧18  (∀ x y ∈ H, x * y ∈ H) ∧ (∀ x ∈ H, x⁻¹ ∈ H)1920notation infixl 70 "*" => call2(G.mul, _, _) via hypothesis Subgroup(H, G) for H21notation postfix 90 "⁻¹" => apply(G.inv, _) via hypothesis Subgroup(H, G) for H2223theorem Subgroup.group (H G : Set)24  requires subgroup : Subgroup(H, G)25  shows Group(G)26proof27  obtain ⟨group, rest⟩ := subgroup28  exact group2930section SubgroupLaws31variable (G H : Set)32hypothesis subgroup : Subgroup(H, G)3334theorem Subgroup.subset35  shows H ⊆ G.carrier36proof37  obtain ⟨g, bounded, rest⟩ := subgroup38  exact bounded3940-- Closure: the carrier membership of a subgroup element is a typing rule,41-- and the subgroup membership of a product, the unit, and an inverse are42-- instances, so each is synthesized.43theorem Subgroup.mem_carrier (h : H)44  shows h ∈ G.carrier45proof46  have bounded := Subgroup.subset with subgroup47  have hIn : h ∈ H by assumption48  exact bounded with h, hIn4950instance Subgroup.one_mem51  shows G.one ∈ H52proof53  obtain ⟨g, bounded, unitIn, rest⟩ := subgroup54  exact unitIn5556instance Subgroup.mul_mem (h k : H)57  shows h * k ∈ H58proof59  obtain ⟨g, bounded, unitIn, closed, inverses⟩ := subgroup60  have hIn : h ∈ H by assumption61  have kIn : k ∈ H by assumption62  exact closed with h, hIn, k, kIn6364instance Subgroup.inv_mem (h : H)65  shows h⁻¹ ∈ H66proof67  obtain ⟨g, bounded, unitIn, closed, inverses⟩ := subgroup68  have hIn : h ∈ H by assumption69  exact inverses with h, hIn7071theorem Subgroup.nonempty72  shows Nonempty(H)73proof74  have unitIn : G.one ∈ H := Subgroup.one_mem with *75  exact ⟨G.one, unitIn⟩7677theorem Subgroup.trivial_subset78  shows {G.one} ⊆ H79proof80  intros x hx81  have equal := singleton.membership.forward with hx82  rw equal83  exact Subgroup.one_mem with *8485theorem Subgroup.eq_trivial_iff86  shows H = {G.one} ↔ ∀ x ∈ H, x = G.one87proof88  have trivialSubset := Subgroup.trivial_subset with subgroup89  constructor90  . intros equal x hx91    rw equal at hx92    exact singleton.membership.forward with hx93  . intro trivial94    apply Subset.antisymmetric95    . intros x hx96      have equal := trivial with x, hx97      rw equal98      exact singleton.self99    . exact trivialSubset100101end SubgroupLaws102103section SubgroupCancellation104variable (G H : Set)105hypothesis group : Group(G)106hypothesis subgroup : Subgroup(H, G)107108-- Membership in a subgroup is unchanged by a factor from the subgroup.109theorem Subgroup.mul_mem_cancel_left (h : H) (x : G)110  shows h * x ∈ H ↔ x ∈ H111proof112  constructor113  . intro member114    have product : h⁻¹ * (h * x) ∈ H := Subgroup.mul_mem with *115    rwa inv_mul_cancel_left at product116  . intro member117    exact Subgroup.mul_mem with *118119theorem Subgroup.mul_mem_cancel_right (h : H) (x : G)120  shows x * h ∈ H ↔ x ∈ H121proof122  constructor123  . intro member124    have product : x * h * h⁻¹ ∈ H := Subgroup.mul_mem with *125    rwa mul_inv_cancel_right at product126  . intro member127    exact Subgroup.mul_mem with *128129theorem Subgroup.inv_mem_iff (x : G)130  shows x⁻¹ ∈ H ↔ x ∈ H131proof132  constructor133  . intro member134    have twice : (x⁻¹)⁻¹ ∈ H := Subgroup.inv_mem with *135    rwa inv_inv at twice136  . intro member137    exact Subgroup.inv_mem with *138139end SubgroupCancellation140141section SubgroupConstructions142variable (G : Set)143hypothesis group : Group(G)144145-- The constructor.146theorem Subgroup.mk (H : Set)147  requires bounded : H ⊆ G148  requires unitIn : G.one ∈ H149  requires closed : ∀ x y ∈ H, x * y ∈ H150  requires inverses : ∀ x ∈ H, x⁻¹ ∈ H151  shows Subgroup(H, G)152proof153  unfold Subgroup154  refine ⟨group, bounded, unitIn, closed, inverses⟩155156-- The subgroups every group has.157theorem Subgroup.whole158  shows Subgroup(G.carrier, G)159proof160  have reflexive := Subset.reflexive at G.carrier161  have unitIn : G.one ∈ G := Group.one_mem with *162  apply Subgroup.mk with group, reflexive, unitIn163  . intros x hx y hy164    exact Group.mul_mem with *165  . intros x hx166    exact Group.inv_mem with *167168theorem Subgroup.trivial169  shows Subgroup({G.one}, G)170proof171  have unitIn : G.one ∈ G := Group.one_mem with *172  have selfIn := singleton.self at G.one173  have bounded : {G.one} ⊆ G174    intros x hx175    have equal := singleton.membership.forward with hx176    rwa equal177  apply Subgroup.mk with group, bounded, selfIn178  . intros x hx y hy179    have ex := singleton.membership.forward with hx180    have ey := singleton.membership.forward with hy181    rw [ex, ey, one_mul]182    exact selfIn183  . intros x hx184    have ex := singleton.membership.forward with hx185    rw [ex, inv_one]186    exact selfIn187188theorem Subgroup.intersection (H K : Set)189  requires subgroupH : Subgroup(H, G)190  requires subgroupK : Subgroup(K, G)191  shows Subgroup(H ∩ K, G)192proof193  have bounded := Subset.transitive with (intersection.subset_left at H, K), (Subgroup.subset with subgroupH)194  have unitIn : G.one ∈ H ∩ K := intersection.membership.backward with ⟨(Subgroup.one_mem with subgroupH), (Subgroup.one_mem with subgroupK)⟩195  apply Subgroup.mk with group, bounded, unitIn196  . intros x hx y hy197    obtain ⟨xH, xK⟩ := intersection.membership.forward with hx198    obtain ⟨yH, yK⟩ := intersection.membership.forward with hy199    exact intersection.membership.backward with ⟨(Subgroup.mul_mem with *), (Subgroup.mul_mem with *)⟩200  . intros x hx201    obtain ⟨xH, xK⟩ := intersection.membership.forward with hx202    exact intersection.membership.backward with ⟨(Subgroup.inv_mem with *), (Subgroup.inv_mem with *)⟩203204-- The one-step subgroup criterion: a nonempty subset closed under205-- x, y ↦ x * y⁻¹ is a subgroup.206theorem Subgroup.of_mul_inv (H : Set)207  requires bounded : H ⊆ G208  requires inhabited : Nonempty(H)209  requires closed : ∀ x y ∈ H, x * y⁻¹ ∈ H210  shows Subgroup(H, G)211proof212  obtain ⟨h, hH⟩ := inhabited213  have hIn := bounded with h, hH214  have unitIn : G.one ∈ H215    have product := closed with h, hH, h, hH216    rwa Group.mul_inv at product217  have inverses : ∀ x ∈ H, x⁻¹ ∈ H218    intros x hx219    have xIn := bounded with x, hx220    have product := closed with G.one, unitIn, x, hx221    rwa one_mul at product222  apply Subgroup.mk with group, bounded, unitIn223  . intros x hx y hy224    have yIn := bounded with y, hy225    have invY := inverses with y, hy226    have product := closed with x, hx, y⁻¹, invY227    rwa inv_inv at product228  . exact inverses229230end SubgroupConstructions231