Grace/Cumulus/Algebra/Group/Abelian.g17

Open in Workbench Download source

Imports

Cyclic

Declarations

Source

1-- Abelian groups: powers distribute over products, the elements killed2-- by a fixed exponent form a subgroup, and so do the elements of finite3-- order4-- 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.Abelian10import Cyclic1112-- The elements killed by the exponent n, and the elements of finite order.13def exponentKernel (G : Set, n : Nat) : Set := { x ∈ G.carrier | groupPow(G, x, n) = G.one }14def torsion (G : Set) : Set := { x ∈ G.carrier | HasFiniteOrder(G, x) }1516theorem exponentKernel.subset (G : Set, n : Nat)17  shows exponentKernel(G, n) ⊆ G.carrier18proof19  intros x hx20  have parts := exponentKernel.membership.forward with hx21  exact parts.left2223theorem torsion.subset (G : Set)24  shows torsion(G) ⊆ G.carrier25proof26  intros x hx27  have parts := torsion.membership.forward with hx28  exact parts.left2930-- In an abelian group, raising to a fixed power is an endomorphism.31defgraph powerEndomorphism (G : Set, n : Nat) (x ∈ G.carrier) : G.carrier := groupPow(G, x, n)32requires group : Group(G)33proof34  exact Group.pow_mem with *3536section Torsion37variable (G : Set)38hypothesis group : Group(G)3940theorem HasFiniteOrder.inv (x : G)41  requires finite : HasFiniteOrder(G, x)42  shows HasFiniteOrder(G, x⁻¹)43proof44  obtain ⟨n, nNat, positive, vanishes⟩ := finite45  have inverted : x⁻¹ ^ n = (x ^ n)⁻¹ := inv_pow with *46  have inverseVanishes : x⁻¹ ^ n = G.one47    rw [inverted, vanishes, inv_one]48    rfl49  exact HasFiniteOrder.of_pow with positive, inverseVanishes5051theorem exponentKernel.of_order_dvd (x : G) (n : Nat)52  requires finite : HasFiniteOrder(G, x)53  requires divides : elementOrder(G, x) ∣ n54  shows x ∈ exponentKernel(G, n)55proof56  have vanishes : x ^ n = G.one := elementOrder.pow_eq_one_of_dvd with *57  have xIn : x ∈ G by assumption58  exact exponentKernel.membership.backward with ⟨xIn, vanishes⟩5960theorem exponentKernel.subset_torsion (n : Nat)61  requires positive : 0 < n62  shows exponentKernel(G, n) ⊆ torsion(G)63proof64  intros x hx65  obtain ⟨xIn, vx⟩ := exponentKernel.membership.forward with hx66  have finite := HasFiniteOrder.of_pow with positive, vx67  exact torsion.membership.backward with ⟨xIn, finite⟩6869end Torsion7071section AbelianPowers72variable (G : Set)73hypothesis abelian : AbelianGroup(G)7475theorem AbelianGroup.mul_pow (x y : G) (n : Nat)76  shows (x * y) ^ n = x ^ n * y ^ n77proof78  have group := AbelianGroup.to_group with abelian79  induction n80  | zero =>81    rw [pow_zero, pow_zero, pow_zero, one_mul]82    rfl83  | succ(k) using ih =>84    have shuffle : x ^ k * y ^ k * (x * y) = x ^ k * x * (y ^ k * y) := mul_mul_mul_comm with *85    rw [← add.right_one, pow_succ, pow_succ, pow_succ, ih, shuffle]86    rfl8788theorem exponentKernel.subgroup (n : Nat)89  shows Subgroup(exponentKernel(G, n), G)90proof91  have group := AbelianGroup.to_group with abelian92  have unitIn : G.one ∈ exponentKernel(G, n)93    have unitPower : G.one ^ n = G.one := one_pow with *94    exact exponentKernel.membership.backward with ⟨(Group.one_mem with group), unitPower⟩95  apply Subgroup.mk with group, (exponentKernel.subset at G, n), unitIn96  . intros x hx y hy97    obtain ⟨xIn, vx⟩ := exponentKernel.membership.forward with hx98    obtain ⟨yIn, vy⟩ := exponentKernel.membership.forward with hy99    have vanishes : (x * y) ^ n = G.one100      rw [AbelianGroup.mul_pow, vx, vy, one_mul]101      rfl102    exact exponentKernel.membership.backward with ⟨(Group.mul_mem with *), vanishes⟩103  . intros x hx104    obtain ⟨xIn, vx⟩ := exponentKernel.membership.forward with hx105    have vanishes : x⁻¹ ^ n = G.one106      rw [inv_pow, vx, inv_one]107      rfl108    exact exponentKernel.membership.backward with ⟨(Group.inv_mem with *), vanishes⟩109110theorem exponentKernel.normal (n : Nat)111  shows NormalSubgroup(exponentKernel(G, n), G)112proof113  have subgroup := exponentKernel.subgroup with *114  exact NormalSubgroup.of_abelian with abelian, subgroup115116theorem AbelianGroup.finite_order_mul (x y : G)117  requires finiteX : HasFiniteOrder(G, x)118  requires finiteY : HasFiniteOrder(G, y)119  shows HasFiniteOrder(G, x * y)120proof121  have group := AbelianGroup.to_group with abelian122  obtain ⟨m, mNat, mPositive, mVanishes⟩ := finiteX123  obtain ⟨n, nNat, nPositive, nVanishes⟩ := finiteY124  have distributed : (x * y) ^ (m * n) = x ^ (m * n) * y ^ (m * n) := AbelianGroup.mul_pow with *125  have xPower : x ^ (m * n) = (x ^ m) ^ n := pow_mul with *126  have swap := mul.commutative at n, m127  have yPower : y ^ (n * m) = (y ^ n) ^ m := pow_mul with *128  have unitM : G.one ^ m = G.one := one_pow with *129  have unitN : G.one ^ n = G.one := one_pow with *130  have mNonzero : m ≠ 0131    intro zero132    rw zero at mPositive133    exact Less.irreflexive at 0 with mPositive134  have nNonzero : n ≠ 0135    intro zero136    rw zero at nPositive137    exact Less.irreflexive at 0 with nPositive138  have productNonzero := mul.nonzero with mNonzero, nNonzero139  have productPositive := Less.add_positive at 0, m * n with productNonzero140  have zeroAdd : 0 + m * n = m * n by ring141  rw zeroAdd at productPositive142  have vanishes : (x * y) ^ (m * n) = G.one143    rw [distributed, xPower, mVanishes, unitN, swap, yPower, nVanishes, unitM, one_mul]144    rfl145  exact HasFiniteOrder.of_pow with productPositive, vanishes146147theorem torsion.subgroup148  shows Subgroup(torsion(G), G)149proof150  have group := AbelianGroup.to_group with abelian151  have unitFinite := HasFiniteOrder.one with group152  have unitIn : G.one ∈ torsion(G) := torsion.membership.backward with ⟨(Group.one_mem with group), unitFinite⟩153  apply Subgroup.mk with group, (torsion.subset at G), unitIn154  . intros x hx y hy155    obtain ⟨xIn, finiteX⟩ := torsion.membership.forward with hx156    obtain ⟨yIn, finiteY⟩ := torsion.membership.forward with hy157    have finite : HasFiniteOrder(G, x * y) := AbelianGroup.finite_order_mul with *158    exact torsion.membership.backward with ⟨(Group.mul_mem with *), finite⟩159  . intros x hx160    obtain ⟨xIn, finiteX⟩ := torsion.membership.forward with hx161    have finite : HasFiniteOrder(G, x⁻¹) := HasFiniteOrder.inv with *162    exact torsion.membership.backward with ⟨(Group.inv_mem with *), finite⟩163164theorem torsion.normal165  shows NormalSubgroup(torsion(G), G)166proof167  have subgroup := torsion.subgroup with abelian168  exact NormalSubgroup.of_abelian with abelian, subgroup169170theorem powerEndomorphism.hom (n : Nat)171  shows powerEndomorphism(G, n) : G →* G172proof173  have group := AbelianGroup.to_group with abelian174  have function := powerEndomorphism.function at G, n with *175  apply GroupHom.mk with group, group, function176  intros x hx y hy177  have closed : x * y ∈ G by typecheck178  have vx := powerEndomorphism.value at G, n, x with *179  have vy := powerEndomorphism.value at G, n, y with *180  have output := powerEndomorphism.value at G, n, x * y with *181  have distributed : (x * y) ^ n = x ^ n * y ^ n := AbelianGroup.mul_pow with *182  cc183184theorem powerEndomorphism.kernel (n : Nat)185  shows kernel(powerEndomorphism(G, n), G, G) = exponentKernel(G, n)186proof187  have group := AbelianGroup.to_group with abelian188  ext x189  constructor190  . intro hx191    obtain ⟨xIn, vx⟩ := kernel.membership.forward with hx192    have value := powerEndomorphism.value at G, n, x with *193    have vanishes : x ^ n = G.one by cc194    exact exponentKernel.membership.backward with ⟨xIn, vanishes⟩195  . intro hx196    obtain ⟨xIn, vx⟩ := exponentKernel.membership.forward with hx197    have value := powerEndomorphism.value at G, n, x with *198    have vanishes : powerEndomorphism(G, n)(x) = G.one by cc199    exact kernel.of_value with xIn, vanishes200201end AbelianPowers202