Grace/Cumulus/Algebra/Group/Generated.g17

Open in Workbench Download source

Imports

Normal

Declarations

Source

1-- The subgroup generated by a subset: the intersection of all subgroups2-- containing it, with its universal property3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Algebra.Group.Generated9import Normal1011def generatedSubgroup (G S : Set) : Set :=12  { x ∈ G.carrier | ∀ H, Subgroup(H, G) → S ⊆ H → x ∈ H }1314theorem generatedSubgroup.subset (G S : Set)15  shows generatedSubgroup(G, S) ⊆ G.carrier16proof17  intros x hx18  have parts := generatedSubgroup.membership.forward with hx19  exact parts.left2021theorem generatedSubgroup.contains (G S : Set)22  requires bounded : S ⊆ G.carrier23  shows S ⊆ generatedSubgroup(G, S)24proof25  intros x hx26  apply generatedSubgroup.membership.backward27  constructor28  . exact bounded with x, hx29  . intros H subgroup included30    exact included with x, hx3132theorem generatedSubgroup.least (G S H : Set)33  requires subgroup : Subgroup(H, G)34  requires included : S ⊆ H35  shows generatedSubgroup(G, S) ⊆ H36proof37  intros x hx38  have parts := generatedSubgroup.membership.forward with hx39  exact parts.right with H, subgroup, included4041theorem generatedSubgroup.mono (G S T : Set)42  requires included : S ⊆ T43  shows generatedSubgroup(G, S) ⊆ generatedSubgroup(G, T)44proof45  intros x hx46  have parts := generatedSubgroup.membership.forward with hx47  apply generatedSubgroup.membership.backward48  refine ⟨parts.left, ?_⟩49  intros H subgroup containsT50  have containsS := Subset.transitive with included, containsT51  exact parts.right with H, subgroup, containsS5253theorem generatedSubgroup.eq_of_subgroup (G H : Set)54  requires subgroup : Subgroup(H, G)55  shows generatedSubgroup(G, H) = H56proof57  have bounded := Subgroup.subset with subgroup58  have includes := generatedSubgroup.contains at G, H with bounded59  have least := generatedSubgroup.least with subgroup, (Subset.reflexive at H)60  exact Subset.antisymmetric with least, includes6162theorem generatedSubgroup.singleton_mem (G g : Set)63  requires bounded : g ∈ G.carrier64  shows g ∈ generatedSubgroup(G, {g})65proof66  have subset : {g} ⊆ G.carrier67    intros x hx68    have equal := singleton.membership.forward with hx69    rwa equal70  have contains := generatedSubgroup.contains at G, {g} with subset71  exact contains with g, singleton.self at g7273section GeneratedLaws74variable (G : Set)75hypothesis group : Group(G)7677theorem generatedSubgroup.subgroup (S : Set)78  shows Subgroup(generatedSubgroup(G, S), G)79proof80  have unitIn : G.one ∈ generatedSubgroup(G, S)81    apply generatedSubgroup.membership.backward82    refine ⟨(Group.one_mem with group), ?_⟩83    intros H subgroup included84    exact Subgroup.one_mem with subgroup85  apply Subgroup.mk with group, (generatedSubgroup.subset at G, S), unitIn86  . intros x hx y hy87    have px := generatedSubgroup.membership.forward with hx88    have py := generatedSubgroup.membership.forward with hy89    have xIn := px.left90    have yIn := py.left91    apply generatedSubgroup.membership.backward92    refine ⟨(Group.mul_mem with *), ?_⟩93    intros H subgroup included94    have xH := px.right with H, subgroup, included95    have yH := py.right with H, subgroup, included96    exact Subgroup.mul_mem with *97  . intros x hx98    have px := generatedSubgroup.membership.forward with hx99    have xIn := px.left100    apply generatedSubgroup.membership.backward101    refine ⟨(Group.inv_mem with *), ?_⟩102    intros H subgroup included103    have xH := px.right with H, subgroup, included104    exact Subgroup.inv_mem with *105106theorem generatedSubgroup.idempotent (S : Set)107  shows generatedSubgroup(G, generatedSubgroup(G, S)) = generatedSubgroup(G, S)108proof109  have subgroup := generatedSubgroup.subgroup at G, S with group110  exact generatedSubgroup.eq_of_subgroup with subgroup111112theorem generatedSubgroup.empty113  shows generatedSubgroup(G, ∅) = {G.one}114proof115  have trivial := Subgroup.trivial with group116  have least := generatedSubgroup.least with trivial, (empty.subset at {G.one})117  have subgroup := generatedSubgroup.subgroup at G, ∅ with group118  have includes := Subgroup.trivial_subset with subgroup119  exact Subset.antisymmetric with least, includes120121theorem generatedSubgroup.whole122  shows generatedSubgroup(G, G.carrier) = G.carrier123proof124  have whole := Subgroup.whole with group125  exact generatedSubgroup.eq_of_subgroup with whole126127theorem generatedSubgroup.one_mem (S : Set)128  shows G.one ∈ generatedSubgroup(G, S)129proof130  have subgroup := generatedSubgroup.subgroup at G, S with group131  exact Subgroup.one_mem with subgroup132133theorem generatedSubgroup.pow_mem (g : G) (n : Nat)134  shows g ^ n ∈ generatedSubgroup(G, {g})135proof136  have subgroup := generatedSubgroup.subgroup at G, {g} with group137  have member : g ∈ generatedSubgroup(G, {g}) := generatedSubgroup.singleton_mem with *138  exact Subgroup.pow_mem with *139140-- The join of two subgroups is generated by their union.141theorem generatedSubgroup.union_left (H K : Set)142  requires subgroupH : Subgroup(H, G)143  shows H ⊆ generatedSubgroup(G, H ∪ K)144proof145  have mono := generatedSubgroup.mono at G, H, H ∪ K with (union2.subset_left at H, K)146  have same := generatedSubgroup.eq_of_subgroup with subgroupH147  rwa same at mono148149theorem generatedSubgroup.union_right (H K : Set)150  requires subgroupK : Subgroup(K, G)151  shows K ⊆ generatedSubgroup(G, H ∪ K)152proof153  have mono := generatedSubgroup.mono at G, K, H ∪ K with (union2.subset_right at H, K)154  have same := generatedSubgroup.eq_of_subgroup with subgroupK155  rwa same at mono156157theorem generatedSubgroup.union_least (H K L : Set)158  requires subgroupL : Subgroup(L, G)159  requires includesH : H ⊆ L160  requires includesK : K ⊆ L161  shows generatedSubgroup(G, H ∪ K) ⊆ L162proof163  have included := union2.subset with includesH, includesK164  exact generatedSubgroup.least with subgroupL, included165166end GeneratedLaws167168-- The image of a generated subgroup is generated by the image.169theorem generatedSubgroup.image_subset (f G H S : Set)170  requires hom : f : G →* H171  requires bounded : S ⊆ G.carrier172  shows functionImage(f, generatedSubgroup(G, S), H.carrier) ⊆173    generatedSubgroup(H, functionImage(f, S, H.carrier))174proof175  have group := GroupHom.source with hom176  have target := GroupHom.target with hom177  have targetSubgroup := generatedSubgroup.subgroup at H, functionImage(f, S, H.carrier) with target178  have preimage := GroupHom.preimage_subgroup with hom, targetSubgroup179  have contains : S ⊆ functionPreimage(f, G.carrier, generatedSubgroup(H, functionImage(f, S, H.carrier)))180    intros x hx181    have xIn := bounded with x, hx182    have fx : f(x) ∈ H.carrier by typecheck183    have imageIn : f(x) ∈ functionImage(f, S, H.carrier)184      apply functionImage.membership.backward185      refine ⟨fx, x, hx, rfl⟩186    have generated := generatedSubgroup.contains at H, functionImage(f, S, H.carrier) with (functionImage.subset at f, S, H.carrier)187    have value := generated with f(x), imageIn188    exact functionPreimage.of_apply with xIn, value189  have least := generatedSubgroup.least with preimage, contains190  intros y hy191  obtain ⟨yIn, x, hx, yEq⟩ := functionImage.membership.forward with hy192  have inPreimage := least with x, hx193  have parts := functionPreimage.membership.forward with inPreimage194  rw yEq195  exact parts.right196