Grace/Cumulus/Algebra/Group/Cyclic.g17

Open in Workbench Download source

Imports

Lagrange · Generated

Declarations

Source

1-- Cyclic subgroups: the powers of an element, elements of finite order2-- and the order of an element as the least positive exponent giving the3-- unit, powers repeating with period the order, and the powers forming4-- the subgroup generated by the element5-- 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.Cyclic11import Lagrange12import Generated1314-- The powers of g in G.15def powers (G g : Set) : Set := { x ∈ G.carrier | ∃ n ∈ ℕ, x = groupPow(G, g, n) }1617-- Elements of finite order, the positive exponents giving the unit, and the18-- order of an element: the least such exponent.19predicate HasFiniteOrder (G g : Set) := ∃ n, Nat(n) ∧ 0 < n ∧ groupPow(G, g, n) = G.one2021def unitPowers (G g : Set) : Set := { n ∈ ℕ | 0 < n ∧ groupPow(G, g, n) = G.one }2223def elementOrder (G g : Set) : Set := leastNatural(unitPowers(G, g))2425theorem powers.subset (G g : Set)26  shows powers(G, g) ⊆ G.carrier27proof28  intros x hx29  have parts := powers.membership.forward with hx30  exact parts.left3132theorem unitPowers.subset_naturals (G g : Set)33  shows unitPowers(G, g) ⊆ ℕ34proof35  intros n hn36  have parts := unitPowers.membership.forward with hn37  exact parts.left3839theorem unitPowers.of_pow (G g : Set, n : Nat)40  requires positive : 0 < n41  requires vanishes : groupPow(G, g, n) = G.one42  shows n ∈ unitPowers(G, g)43proof44  have nNat : Nat(n) by typecheck45  have natIn := nat.omega.forward with nNat46  apply unitPowers.membership.backward47  refine ⟨natIn, positive, vanishes⟩4849theorem HasFiniteOrder.nonempty (G g : Set)50  requires finite : HasFiniteOrder(G, g)51  shows Nonempty(unitPowers(G, g))52proof53  obtain ⟨n, nNat, positive, vanishes⟩ := finite54  have member := unitPowers.of_pow with positive, vanishes55  exact ⟨n, member⟩5657theorem HasFiniteOrder.of_pow (G g : Set, n : Nat)58  requires positive : 0 < n59  requires vanishes : groupPow(G, g, n) = G.one60  shows HasFiniteOrder(G, g)61proof62  have nNat : Nat(n) by typecheck63  unfold HasFiniteOrder64  exact ⟨n, nNat, positive, vanishes⟩6566theorem elementOrder.member (G g : Set)67  requires finite : HasFiniteOrder(G, g)68  shows elementOrder(G, g) ∈ unitPowers(G, g)69proof70  have inhabited := HasFiniteOrder.nonempty with finite71  have naturals := unitPowers.subset_naturals at G, g72  unfold elementOrder73  exact leastNatural.member with inhabited, naturals7475theorem elementOrder.natural (G g : Set)76  requires finite : HasFiniteOrder(G, g)77  shows Nat(elementOrder(G, g))78proof79  have member := elementOrder.member with finite80  have parts := unitPowers.membership.forward with member81  exact nat.omega.backward with parts.left8283theorem elementOrder.positive (G g : Set)84  requires finite : HasFiniteOrder(G, g)85  shows 0 < elementOrder(G, g)86proof87  have member := elementOrder.member with finite88  have parts := unitPowers.membership.forward with member89  exact parts.right.left9091theorem elementOrder.nonzero (G g : Set)92  requires finite : HasFiniteOrder(G, g)93  shows elementOrder(G, g) ≠ 094proof95  have positive := elementOrder.positive with finite96  have natural := elementOrder.natural with finite97  intro zero98  rw zero at positive99  exact Less.irreflexive at 0 with positive100101theorem elementOrder.pow_order (G g : Set)102  requires finite : HasFiniteOrder(G, g)103  shows groupPow(G, g, elementOrder(G, g)) = G.one104proof105  have member := elementOrder.member with finite106  have parts := unitPowers.membership.forward with member107  exact parts.right.right108109theorem elementOrder.least (G g : Set, m : Nat)110  requires finite : HasFiniteOrder(G, g)111  requires positive : 0 < m112  requires vanishes : groupPow(G, g, m) = G.one113  shows elementOrder(G, g) ≤ m114proof115  have inhabited := HasFiniteOrder.nonempty with finite116  have naturals := unitPowers.subset_naturals at G, g117  have member := unitPowers.of_pow with positive, vanishes118  unfold elementOrder119  exact leastNatural.least with inhabited, naturals, member120121section Powers122variable (G : Set)123hypothesis group : Group(G)124125instance powers.pow_mem (g : G) (n : Nat)126  shows g ^ n ∈ powers(G, g)127proof128  have closed : g ^ n ∈ G by typecheck129  have nNat : Nat(n) by typecheck130  have natIn := nat.omega.forward with nNat131  apply powers.membership.backward132  refine ⟨closed, n, natIn, rfl⟩133134theorem powers.one_mem (g : G)135  shows G.one ∈ powers(G, g)136proof137  have member : g ^ 0 ∈ powers(G, g) := powers.pow_mem with *138  rwa pow_zero at member139140theorem powers.self_mem (g : G)141  shows g ∈ powers(G, g)142proof143  have member : g ^ 1 ∈ powers(G, g) := powers.pow_mem with *144  rwa pow_one at member145146theorem powers.mul_mem (g : G) (x y : Set)147  requires hx : x ∈ powers(G, g)148  requires hy : y ∈ powers(G, g)149  shows x * y ∈ powers(G, g)150proof151  obtain ⟨xIn, m, mIn, xEq⟩ := powers.membership.forward with hx152  obtain ⟨yIn, n, nIn, yEq⟩ := powers.membership.forward with hy153  have mNat := nat.omega.backward with mIn154  have nNat := nat.omega.backward with nIn155  have split : g ^ (m + n) = g ^ m * g ^ n := pow_add with *156  have member : g ^ (m + n) ∈ powers(G, g) := powers.pow_mem with *157  rw [xEq, yEq, ← split]158  exact member159160theorem powers.commutative (g : G)161  shows Commutative(powers(G, g), G.mul)162proof163  intros x hx y hy164  obtain ⟨xIn, m, mIn, xEq⟩ := powers.membership.forward with hx165  obtain ⟨yIn, n, nIn, yEq⟩ := powers.membership.forward with hy166  have mNat := nat.omega.backward with mIn167  have nNat := nat.omega.backward with nIn168  have swap : g ^ m * g ^ n = g ^ n * g ^ m := pow_mul_comm with *169  rw [xEq, yEq]170  exact swap171172theorem powers.subset_generated (g : G)173  shows powers(G, g) ⊆ generatedSubgroup(G, {g})174proof175  intros x hx176  obtain ⟨xIn, n, nIn, xEq⟩ := powers.membership.forward with hx177  have nNat := nat.omega.backward with nIn178  have member : g ^ n ∈ generatedSubgroup(G, {g}) := generatedSubgroup.pow_mem with *179  rwa xEq180181theorem powers.subset_subgroup (H g : Set)182  requires subgroup : Subgroup(H, G)183  requires hg : g ∈ H184  shows powers(G, g) ⊆ H185proof186  intros x hx187  obtain ⟨xIn, n, nIn, xEq⟩ := powers.membership.forward with hx188  have nNat := nat.omega.backward with nIn189  have member : g ^ n ∈ H := Subgroup.pow_mem with *190  rwa xEq191192theorem HasFiniteOrder.one193  shows HasFiniteOrder(G, G.one)194proof195  have one : G.one ^ 1 = G.one := pow_one with *196  have positive : 0 < 1 by arith197  exact HasFiniteOrder.of_pow with positive, one198199theorem elementOrder.pow_mul (g : G) (k : Nat)200  requires finite : HasFiniteOrder(G, g)201  shows g ^ mul(elementOrder(G, g), k) = G.one202proof203  have natural := elementOrder.natural with finite204  have vanishes := elementOrder.pow_order with finite205  have split : g ^ (elementOrder(G, g) * k) = (g ^ elementOrder(G, g)) ^ k := pow_mul with *206  have unitPower : G.one ^ k = G.one := one_pow with *207  rw [split, vanishes]208  exact unitPower209210theorem elementOrder.pow_mod (g : G) (n : Nat)211  requires finite : HasFiniteOrder(G, g)212  shows g ^ n = g ^ (n % elementOrder(G, g))213proof214  have natural := elementOrder.natural with finite215  have nonzero := elementOrder.nonzero with finite216  obtain ⟨q, qNat, shape⟩ := mod.equation at n, elementOrder(G, g) with nonzero217  have remainderNat : Nat(n % elementOrder(G, g)) by typecheck218  have multipleNat : Nat(elementOrder(G, g) * q) by typecheck219  have split : g ^ (elementOrder(G, g) * q + n % elementOrder(G, g)) =220      g ^ (elementOrder(G, g) * q) * g ^ (n % elementOrder(G, g)) := pow_add with *221  have vanishes : g ^ mul(elementOrder(G, g), q) = G.one := elementOrder.pow_mul with *222  have expanded : g ^ n = g ^ (elementOrder(G, g) * q + n % elementOrder(G, g))223    rw ← shape224    rfl225  rw [expanded, split, vanishes, one_mul]226  rfl227228theorem elementOrder.pow_eq_one_of_dvd (g : G) (n : Nat)229  requires finite : HasFiniteOrder(G, g)230  requires divides : elementOrder(G, g) ∣ n231  shows g ^ n = G.one232proof233  have natural := elementOrder.natural with finite234  obtain ⟨k, kNat, shape⟩ := divides235  have vanishes : g ^ mul(elementOrder(G, g), k) = G.one := elementOrder.pow_mul with *236  rw ← shape237  exact vanishes238239theorem elementOrder.dvd_of_pow_eq_one (g : G) (n : Nat)240  requires finite : HasFiniteOrder(G, g)241  requires vanishes : g ^ n = G.one242  shows elementOrder(G, g) ∣ n243proof244  have natural := elementOrder.natural with finite245  have nonzero := elementOrder.nonzero with finite246  obtain ⟨q, qNat, shape⟩ := mod.equation at n, elementOrder(G, g) with nonzero247  have below := mod.less at n, elementOrder(G, g) with nonzero248  have remainderNat : Nat(n % elementOrder(G, g)) by typecheck249  have reduced : g ^ n = g ^ (n % elementOrder(G, g)) := elementOrder.pow_mod with *250  have remainderVanishes : g ^ (n % elementOrder(G, g)) = G.one by cc251  have remainderZero : n % elementOrder(G, g) = 0252    by_contra253    have positive := Less.add_positive at 0, n % elementOrder(G, g) with this254    have zeroAdd : 0 + n % elementOrder(G, g) = n % elementOrder(G, g) by ring255    rw zeroAdd at positive256    have least := elementOrder.least with finite, positive, remainderVanishes257    have strict := LessEqual.transitive_Less with least, below258    exact Less.irreflexive with strict259  rw remainderZero at shape260  have multiple : elementOrder(G, g) * q = n261    have addZero : elementOrder(G, g) * q + 0 = elementOrder(G, g) * q by ring262    rw addZero at shape263    symm264    exact shape265  unfold Divides266  exact ⟨q, qNat, multiple⟩267268theorem elementOrder.pow_eq_one_iff (g : G) (n : Nat)269  requires finite : HasFiniteOrder(G, g)270  shows g ^ n = G.one ↔ elementOrder(G, g) ∣ n271proof272  constructor273  . intro vanishes274    exact elementOrder.dvd_of_pow_eq_one with *275  . intro divides276    exact elementOrder.pow_eq_one_of_dvd with *277278-- The order of the unit is one, and an element of order one is the unit.279theorem elementOrder.one280  shows elementOrder(G, G.one) = 1281proof282  have finite := HasFiniteOrder.one with group283  have natural := elementOrder.natural with finite284  have positive := elementOrder.positive with finite285  have one : G.one ^ 1 = G.one := pow_one with *286  have onePositive : 0 < 1 by arith287  have least := elementOrder.least with finite, onePositive, one288  have lower : 1 ≤ elementOrder(G, G.one) by arith289  exact LessEqual.antisymmetric with least, lower290291theorem elementOrder.eq_one_iff (g : G)292  requires finite : HasFiniteOrder(G, g)293  shows elementOrder(G, g) = 1 ↔ g = G.one294proof295  have one : g ^ 1 = g := pow_one with *296  constructor297  . intro equal298    have vanishes := elementOrder.pow_order with finite299    rw [equal, one] at vanishes300    exact vanishes301  . intro equal302    rw equal303    exact elementOrder.one with group304305-- Inverses of powers are powers when the element has finite order.306theorem powers.inv_mem (g : G) (x : Set)307  requires finite : HasFiniteOrder(G, g)308  requires hx : x ∈ powers(G, g)309  shows x⁻¹ ∈ powers(G, g)310proof311  have natural := elementOrder.natural with finite312  have nonzero := elementOrder.nonzero with finite313  obtain ⟨xIn, n, nIn, xEq⟩ := powers.membership.forward with hx314  have nNat := nat.omega.backward with nIn315  have shape := natural.zero_or_successor at elementOrder(G, g)316  cases shape with zero | successor317  . exfalso318    exact nonzero with zero319  . obtain ⟨k, kNat, orderEq⟩ := successor320    have split : g ^ (n + n * k) = g ^ n * g ^ (n * k) := pow_add with *321    have step := mul.succ_right at k, n322    have swap := mul.commutative at n, elementOrder(G, g)323    have vanishes : g ^ mul(elementOrder(G, g), n) = G.one := elementOrder.pow_mul with *324    have product : g ^ n * g ^ (n * k) = G.one325      rw [← split, ← step, ← orderEq, ← swap]326      exact vanishes327    have inverted : g ^ (n * k) = (g ^ n)⁻¹ := eq_inv_of_mul_eq_one_right with *328    have member : g ^ (n * k) ∈ powers(G, g) := powers.pow_mem with *329    rw [xEq, ← inverted]330    exact member331332theorem powers.subgroup (g : G)333  requires finite : HasFiniteOrder(G, g)334  shows Subgroup(powers(G, g), G)335proof336  have unitIn : G.one ∈ powers(G, g) := powers.one_mem with *337  apply Subgroup.mk with group, (powers.subset at G, g), unitIn338  . intros x hx y hy339    exact powers.mul_mem with *340  . intros x hx341    exact powers.inv_mem with *342343theorem powers.eq_generated (g : G)344  requires finite : HasFiniteOrder(G, g)345  shows powers(G, g) = generatedSubgroup(G, {g})346proof347  have subgroup := powers.subgroup with *348  have included := powers.subset_generated with *349  have selfIn : g ∈ powers(G, g) := powers.self_mem with *350  have singleton : {g} ⊆ powers(G, g)351    intros x hx352    have equal := singleton.membership.forward with hx353    rwa equal354  have least := generatedSubgroup.least with subgroup, singleton355  exact Subset.antisymmetric with included, least356357end Powers358359theorem powers.normal_of_abelian (G g : Set)360  requires abelian : AbelianGroup(G)361  requires hg : g ∈ G.carrier362  requires finite : HasFiniteOrder(G, g)363  shows NormalSubgroup(powers(G, g), G)364proof365  have group := AbelianGroup.to_group with abelian366  have subgroup := powers.subgroup with *367  exact NormalSubgroup.of_abelian with abelian, subgroup368369section HomPowers370variable (f G H : Set)371hypothesis hom : f : G →* H372373-- Homomorphisms carry powers to powers and preserve finite order.374theorem GroupHom.image_powers (g : G)375  shows functionImage(f, powers(G, g), H.carrier) = powers(H, f(g))376proof377  have group := GroupHom.source with hom378  have target := GroupHom.target with hom379  have function := GroupHom.function with hom380  have fg : f(g) ∈ H by typecheck381  ext y382  constructor383  . intro hy384    obtain ⟨yIn, x, hx, yEq⟩ := functionImage.membership.forward with hy385    obtain ⟨xIn, n, nIn, xEq⟩ := powers.membership.forward with hx386    have nNat := nat.omega.backward with nIn387    have preserved : f(g ^ n) = f(g) ^ n := GroupHom.map_pow with *388    have member : f(g) ^ n ∈ powers(H, f(g)) := powers.pow_mem with *389    rw [yEq, xEq, preserved]390    exact member391  . intro hy392    obtain ⟨yIn, n, nIn, yEq⟩ := powers.membership.forward with hy393    have nNat := nat.omega.backward with nIn394    have preserved : f(g ^ n) = f(g) ^ n := GroupHom.map_pow with *395    have member : g ^ n ∈ powers(G, g) := powers.pow_mem with *396    apply functionImage.membership.backward397    refine ⟨yIn, g ^ n, member, ?_⟩398    rw [yEq, preserved]399    rfl400401theorem GroupHom.finite_order (g : G)402  requires finite : HasFiniteOrder(G, g)403  shows HasFiniteOrder(H, f(g))404proof405  have group := GroupHom.source with hom406  have target := GroupHom.target with hom407  obtain ⟨n, nNat, positive, vanishes⟩ := finite408  have preserved : f(g ^ n) = f(g) ^ n := GroupHom.map_pow with *409  have unitValue := GroupHom.map_one with hom410  have imageVanishes : f(g) ^ n = H.one by cc411  exact HasFiniteOrder.of_pow with positive, imageVanishes412413theorem GroupHom.order_dvd (g : G)414  requires finite : HasFiniteOrder(G, g)415  shows elementOrder(H, f(g)) ∣ elementOrder(G, g)416proof417  have group := GroupHom.source with hom418  have target := GroupHom.target with hom419  have fg : f(g) ∈ H by typecheck420  have imageFinite := GroupHom.finite_order with hom, finite421  have natural := elementOrder.natural with finite422  have vanishes := elementOrder.pow_order with finite423  have preserved : f(g ^ elementOrder(G, g)) = f(g) ^ elementOrder(G, g) := GroupHom.map_pow with *424  have unitValue := GroupHom.map_one with hom425  have imageVanishes : f(g) ^ elementOrder(G, g) = H.one by cc426  exact elementOrder.dvd_of_pow_eq_one with *427428end HomPowers429