Grace/Cumulus/Algebra/Group/Lagrange.g17

Open in Workbench Download source

Imports

Coset · Combinatorics.Partitions · NumberTheory.Divisibility

Declarations

Source

1-- Lagrange's theorem: the order of a group and the index of a subgroup,2-- every coset in bijection with the subgroup by translation, the cosets a3-- partition of the group, so the order of a finite group is the index times4-- the order of the subgroup, and the order of the subgroup divides it5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Algebra.Group.Lagrange11import Coset12import Combinatorics.Partitions13import NumberTheory.Divisibility1415-- The order of a group is the size of its carrier, and the index of a16-- subgroup the number of its left cosets.17def order (G : Set) : Set := cardinality(G.carrier)18def index (G H : Set) : Set := cardinality(leftCosets(G, H))1920theorem order.value (G : Set)21  shows order(G) = cardinality(G.carrier)22proof23  simp [order]2425theorem index.value (G H : Set)26  shows index(G, H) = cardinality(leftCosets(G, H))27proof28  simp [index]2930theorem order.nat (G : Set)31  requires finite : Finite(G.carrier)32  shows Nat(order(G))33proof34  rw order.value35  exact cardinality.nat with finite3637-- Translation by g carries the subgroup onto the coset g • H.38defgraph cosetMap (G H g : Set) (h ∈ H) : g • H := g * h39requires group : Group(G)40requires subgroup : Subgroup(H, G)41requires hg : g ∈ G.carrier42proof43  exact leftCoset.mul_mem with *4445section Lagrange46variable (G H : Set)47hypothesis group : Group(G)48hypothesis subgroup : Subgroup(H, G)4950-- Every coset is in bijection with the subgroup: h ↦ g * h is injective by51-- cancellation and reaches every member of g • H.52theorem cosetMap.injective (g : G)53  shows InjectiveBetween(cosetMap(G, H, g), H, g • H)54proof55  have function := cosetMap.function at G, H, g with *56  constructor57  . exact function58  . intros x hx y hy z hz hxz hyz59    have xValue := FunctionBetween.apply_value with function, hx, hxz60    have yValue := FunctionBetween.apply_value with function, hy, hyz61    have xImage := cosetMap.value at G, H, g, x with *62    have yImage := cosetMap.value at G, H, g, y with *63    have equal : g * x = g * y by cc64    exact mul_left_cancel with *6566theorem cosetMap.surjective (g : G)67  shows SurjectiveBetween(cosetMap(G, H, g), H, g • H)68proof69  have function := cosetMap.function at G, H, g with *70  constructor71  . exact function72  . intros y hy73    obtain ⟨yIn, h, hH, yEq⟩ := leftCoset.membership.forward with hy74    have image := cosetMap.value at G, H, g, h with *75    have related := FunctionBetween.relates_apply with function, hH76    witness h77    constructor78    . exact hH79    . rw [image, ← yEq] at related80      exact related8182theorem cosetMap.bijective (g : G)83  shows BijectiveBetween(cosetMap(G, H, g), H, g • H)84proof85  constructor86  . exact cosetMap.injective with *87  . exact cosetMap.surjective with *8889theorem leftCoset.equipotent (g : G)90  shows H ≃ g • H91proof92  witness cosetMap(G, H, g)93  exact cosetMap.bijective with *9495theorem leftCoset.cardinality (g : G)96  requires finite : Finite(H)97  shows cardinality(g • H) = cardinality(H)98proof99  have bijective := cosetMap.bijective with *100  symm101  exact cardinality.bijective with finite, bijective102103-- The cosets partition the group: two cosets are equal or disjoint, and104-- every element lies in its own coset.105theorem leftCoset.eq_or_disjoint (x y : G)106  shows x • H = y • H ∨ Disjoint(x • H, y • H)107proof108  by_contra neither109  apply neither110  right111  apply Disjoint.iff.backward112  intros z hzx hzy113  apply neither114  left115  exact leftCoset.eq_of_common with *116117theorem leftCosets.cover118  shows ⋃(leftCosets(G, H)) = G.carrier119proof120  ext x121  constructor122  . intro hx123    obtain ⟨C, hC, hxC⟩ := union.membership.forward with hx124    have bounded := leftCosets.subset_powerset at G, H125    have subset := powerset.membership_iff.forward with (bounded with C, hC)126    exact subset with x, hxC127  . intro hx128    have self : x ∈ x • H := leftCoset.self with *129    have member := leftCosets.coset_member at G, H, x with hx130    exact union.membership.backward with ⟨x • H, member, self⟩131132theorem leftCosets.pairwise_disjoint133  shows PairwiseDisjoint(leftCosets(G, H))134proof135  intros C hC D hD different136  obtain ⟨boundC, x, hx, CEq⟩ := leftCosets.membership.forward with hC137  obtain ⟨boundD, y, hy, DEq⟩ := leftCosets.membership.forward with hD138  rw [CEq, DEq] at different139  rw [CEq, DEq]140  have split := leftCoset.eq_or_disjoint at G, H, x, y with *141  cases split with equal | disjoint142  . exfalso143    exact different with equal144  . exact disjoint145146theorem leftCosets.member_cardinality (C : Set)147  requires hC : C ∈ leftCosets(G, H)148  requires finite : Finite(H)149  shows cardinality(C) = cardinality(H)150proof151  obtain ⟨bound, g, hg, CEq⟩ := leftCosets.membership.forward with hC152  rw CEq153  exact leftCoset.cardinality with *154155-- Finiteness passes from the group to the subgroup, to the cosets, and to156-- the coset space.157theorem Subgroup.finite158  requires finite : Finite(G)159  shows Finite(H)160proof161  exact Finite.subset with finite, (Subgroup.subset with subgroup)162163theorem leftCosets.member_finite (C : Set)164  requires hC : C ∈ leftCosets(G, H)165  requires finite : Finite(G)166  shows Finite(C)167proof168  have bounded := leftCosets.subset_powerset at G, H169  have subset := powerset.membership_iff.forward with (bounded with C, hC)170  exact Finite.subset with finite, subset171172theorem leftCosets.finite173  requires finite : Finite(G)174  shows Finite(leftCosets(G, H))175proof176  have finitePowerset := Finite.powerset with finite177  exact Finite.subset with finitePowerset, (leftCosets.subset_powerset at G, H)178179instance index.nat180  requires finite : Finite(G)181  shows Nat(index(G, H))182proof183  rw index.value184  exact cardinality.nat with (leftCosets.finite with *)185186-- Lagrange's theorem: a finite group is the disjoint union of its cosets,187-- each of the size of the subgroup, so its order is the index times the188-- order of the subgroup. The index is a natural number by index.nat, so189-- the product is the natural one.190theorem lagrange191  requires finite : Finite(G)192  shows order(G) = index(G, H) * cardinality(H)193proof194  have finiteH := Subgroup.finite with *195  have finiteCosets := leftCosets.finite with *196  have subgroupNat := cardinality.nat with finiteH197  have cosetsNat := cardinality.nat with finiteCosets198  have indexNat := index.nat with *199  have blocks : ∀ C ∈ leftCosets(G, H), Finite(C)200    intros C hC201    exact leftCosets.member_finite with *202  have sizes : ∀ C ∈ leftCosets(G, H), cardinality(C) = cardinality(H)203    intros C hC204    exact leftCosets.member_cardinality with *205  have disjoint := leftCosets.pairwise_disjoint with *206  calc207    order(G) = cardinality(G) := order.value at G208    _ = cardinality(⋃(leftCosets(G, H))) := by rw leftCosets.cover209    _ = cardinality(leftCosets(G, H)) * cardinality(H) :=210      cardinality.big_union_constant with finiteCosets, blocks, disjoint, sizes211    _ = index(G, H) * cardinality(H) := by rw index.value212213-- Lagrange's theorem as divisibility: the index is the quotient.214theorem lagrange.theorem215  requires finite : Finite(G)216  shows cardinality(H) ∣ order(G)217proof218  have subgroupNat := cardinality.nat with (Subgroup.finite with *)219  have indexNat := index.nat with *220  have count := lagrange with *221  witness index(G, H)222  rw count223  exact mul.commutative with *224225theorem Subgroup.card_le226  requires finite : Finite(G)227  shows cardinality(H) ≤ order(G)228proof229  rw order.value230  exact cardinality.monotone with finite, (Subgroup.subset with subgroup)231232end Lagrange233234section Index235variable (G : Set)236hypothesis group : Group(G)237238-- The whole group is its only coset, so it has index one; the trivial239-- subgroup has as many cosets as the group has elements.240theorem leftCosets.whole241  shows leftCosets(G, G.carrier) = {G.carrier}242proof243  have subgroup := Subgroup.whole with group244  ext C245  constructor246  . intro hC247    obtain ⟨bound, g, hg, CEq⟩ := leftCosets.membership.forward with hC248    have criterion : g • G.carrier = G.carrier ↔ g ∈ G :=249      leftCoset.eq_self_iff with *250    have whole := criterion.backward with hg251    rw [CEq, whole]252    exact singleton.self253  . intro hC254    have equal := singleton.membership.forward with hC255    have unitIn : G.one ∈ G := Group.one_mem with *256    have one : G.one • G.carrier = G.carrier := leftCoset.one with *257    have member := leftCosets.coset_member at G, G.carrier, G.one with258      unitIn259    rw one at member260    rw equal261    exact member262263theorem index.whole264  shows index(G, G.carrier) = 1265proof266  rw [index.value, leftCosets.whole]267  exact cardinality.singleton at G.carrier268269theorem index.trivial270  requires finite : Finite(G)271  shows index(G, {G.one}) = order(G)272proof273  have subgroup := Subgroup.trivial with group274  have indexNat := index.nat with *275  have count := lagrange with *276  rw [count, cardinality.singleton, mul.right_unit]277  rfl278279end Index280