Grace/Cumulus/Algebra/Group/ElementOrder.g17

Open in Workbench Download source

Imports

Cyclic · Cardinal.Dominance

Declarations

Source

1-- Orders of elements in finite groups: every element of a finite group2-- has finite order, the cyclic subgroup it generates has exactly that3-- many elements, so by Lagrange the order divides the order of the group4-- and the group order annihilates every 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.ElementOrder11import Cyclic12import Cardinal.Dominance1314section Orders15variable (G : Set)16hypothesis group : Group(G)1718theorem pow_eq_one_of_pow_add_eq (g : G) (m k : Nat)19  requires equal : g ^ (m + k) = g ^ m20  shows g ^ k = G.one21proof22  have split : g ^ (m + k) = g ^ m * g ^ k := pow_add with *23  have products : g ^ m * g ^ k = g ^ m * G.one24    rw [← split, equal, mul_one]25    rfl26  exact mul_left_cancel at G, g ^ m, g ^ k, G.one with *2728theorem HasFiniteOrder.of_pow_eq (g : G) (m n : Nat)29  requires below : m < n30  requires equal : g ^ m = g ^ n31  shows HasFiniteOrder(G, g)32proof33  obtain ⟨j, jNat, shape⟩ := below34  have form : m + succ(j) = n35    rw ← shape36    exact add.successor_shift at m, j37  have shifted : g ^ (m + succ(j)) = g ^ m by cc38  have vanishes : g ^ succ(j) = G.one := pow_eq_one_of_pow_add_eq with *39  have positive : 0 < succ(j) by arith40  exact HasFiniteOrder.of_pow with positive, vanishes4142end Orders4344-- Powers as a function on the naturals.45defgraph powerMap (G g : Set) (n ∈ ℕ) : G.carrier := groupPow(G, g, n)46requires group : Group(G)47requires hg : g ∈ G.carrier48proof49  have nNat := nat.omega.backward with member50  exact Group.pow_mem with group, hg, nNat5152-- The exponents below the order enumerate the cyclic subgroup.53defgraph orderMap (G g : Set) (n ∈ elementOrder(G, g)) : powers(G, g) := groupPow(G, g, n)54requires group : Group(G)55requires hg : g ∈ G.carrier56requires finite : HasFiniteOrder(G, g)57proof58  have natural := elementOrder.natural with finite59  have nNat := natural.member at elementOrder(G, g) with n, member60  exact powers.pow_mem with group, hg, nNat6162section FiniteOrders63variable (G : Set)64hypothesis group : Group(G)6566theorem powerMap.injective_of_infinite_order (g : G)67  requires infinite : ¬HasFiniteOrder(G, g)68  shows InjectiveBetween(powerMap(G, g), ℕ, G.carrier)69proof70  have function := powerMap.function at G, g with *71  constructor72  . exact function73  . intros m hm n hn z hz hmz hnz74    have mNat := nat.omega.backward with hm75    have nNat := nat.omega.backward with hn76    have vm := FunctionBetween.apply_value with function, hm, hmz77    have vn := FunctionBetween.apply_value with function, hn, hnz78    have valueM := powerMap.value at G, g, m with *79    have valueN := powerMap.value at G, g, n with *80    have equal : g ^ m = g ^ n by cc81    have comparison := Less.trichotomy at m, n with mNat, nNat82    rcases comparison with less | same | greater83    . exfalso84      have finite := HasFiniteOrder.of_pow_eq at G, g, m, n with *85      exact infinite with finite86    . exact same87    . exfalso88      have reversed : g ^ n = g ^ m by cc89      have finite := HasFiniteOrder.of_pow_eq at G, g, n, m with *90      exact infinite with finite9192-- Every element of a finite group has finite order.93theorem Group.finite_order (g : G)94  requires finite : Finite(G)95  shows HasFiniteOrder(G, g)96proof97  by_contra98  have injective := powerMap.injective_of_infinite_order with *99  have dominated := Dominated.of_injective with injective100  have finiteNaturals := Finite.of_dominated with finite, dominated101  exact omega.infinite with finiteNaturals102103theorem elementOrder.le_of_pow_eq (g : G) (m n : Nat)104  requires finite : HasFiniteOrder(G, g)105  requires below : m < n106  requires equal : g ^ m = g ^ n107  shows elementOrder(G, g) ≤ n108proof109  have natural := elementOrder.natural with finite110  obtain ⟨j, jNat, shape⟩ := below111  have form : m + succ(j) = n112    rw ← shape113    exact add.successor_shift at m, j114  have shifted : g ^ (m + succ(j)) = g ^ m by cc115  have vanishes : g ^ succ(j) = G.one := pow_eq_one_of_pow_add_eq with *116  have positive : 0 < succ(j) by arith117  have least := elementOrder.least with finite, positive, vanishes118  have bound : succ(j) ≤ n119    witness m120    rw ← form121    ring122  exact LessEqual.transitive with least, bound123124-- Below the order, distinct exponents give distinct powers.125theorem elementOrder.pow_injective_below (g : G) (m n : Nat)126  requires finite : HasFiniteOrder(G, g)127  requires mBelow : m < elementOrder(G, g)128  requires nBelow : n < elementOrder(G, g)129  requires equal : g ^ m = g ^ n130  shows m = n131proof132  have natural := elementOrder.natural with finite133  have mNat : Nat(m) by typecheck134  have nNat : Nat(n) by typecheck135  have comparison := Less.trichotomy at m, n with mNat, nNat136  rcases comparison with less | same | greater137  . exfalso138    have bound := elementOrder.le_of_pow_eq at G, g, m, n with *139    have strict := LessEqual.transitive_Less with bound, nBelow140    exact Less.irreflexive with strict141  . exact same142  . exfalso143    have reversed : g ^ n = g ^ m by cc144    have bound := elementOrder.le_of_pow_eq at G, g, n, m with *145    have strict := LessEqual.transitive_Less with bound, mBelow146    exact Less.irreflexive with strict147148theorem orderMap.injective (g : G)149  requires finite : HasFiniteOrder(G, g)150  shows InjectiveBetween(orderMap(G, g), elementOrder(G, g), powers(G, g))151proof152  have natural := elementOrder.natural with finite153  have function := orderMap.function at G, g with *154  constructor155  . exact function156  . intros m hm n hn z hz hmz hnz157    have mNat := natural.member at elementOrder(G, g) with m, hm158    have nNat := natural.member at elementOrder(G, g) with n, hn159    have mBelow := Less.of_membership at m, elementOrder(G, g) with hm160    have nBelow := Less.of_membership at n, elementOrder(G, g) with hn161    have vm := FunctionBetween.apply_value with function, hm, hmz162    have vn := FunctionBetween.apply_value with function, hn, hnz163    have valueM := orderMap.value at G, g, m with *164    have valueN := orderMap.value at G, g, n with *165    have equal : g ^ m = g ^ n by cc166    exact elementOrder.pow_injective_below with *167168theorem orderMap.surjective (g : G)169  requires finite : HasFiniteOrder(G, g)170  shows SurjectiveBetween(orderMap(G, g), elementOrder(G, g), powers(G, g))171proof172  have natural := elementOrder.natural with finite173  have nonzero := elementOrder.nonzero with finite174  have function := orderMap.function at G, g with *175  constructor176  . exact function177  . intros y hy178    obtain ⟨yIn, n, nIn, yEq⟩ := powers.membership.forward with hy179    have nNat := nat.omega.backward with nIn180    have remainderNat : Nat(n % elementOrder(G, g)) by typecheck181    have below := mod.less at n, elementOrder(G, g) with nonzero182    have member := membership.of_Less with remainderNat, natural, below183    have reduced : g ^ n = g ^ (n % elementOrder(G, g)) := elementOrder.pow_mod with *184    have value := orderMap.value at G, g, n % elementOrder(G, g) with *185    have edge := FunctionBetween.relates_apply with function, member186    refine ⟨n % elementOrder(G, g), member, ?_⟩187    rw [value, ← reduced] at edge188    rw yEq189    exact edge190191theorem orderMap.bijective (g : G)192  requires finite : HasFiniteOrder(G, g)193  shows BijectiveBetween(orderMap(G, g), elementOrder(G, g), powers(G, g))194proof195  constructor196  . exact orderMap.injective with *197  . exact orderMap.surjective with *198199theorem powers.has_cardinality (g : G)200  requires finite : HasFiniteOrder(G, g)201  shows HasCardinality(powers(G, g), elementOrder(G, g))202proof203  have natural := elementOrder.natural with finite204  have bijective := orderMap.bijective with *205  have equipotent : Equipotent(elementOrder(G, g), powers(G, g))206    witness orderMap(G, g)207    exact bijective208  have reversed := Equipotent.symmetric with equipotent209  unfold HasCardinality210  exact ⟨natural, reversed⟩211212theorem powers.cardinality (g : G)213  requires finite : HasFiniteOrder(G, g)214  shows cardinality(powers(G, g)) = elementOrder(G, g)215proof216  have hasCardinality := powers.has_cardinality with *217  exact cardinality.eq_of_has with hasCardinality218219theorem powers.finite (g : G)220  requires finite : HasFiniteOrder(G, g)221  shows Finite(powers(G, g))222proof223  have hasCardinality := powers.has_cardinality with *224  exact Finite.from_cardinality with hasCardinality225226-- The order of an element divides the order of the group.227theorem elementOrder.dvd_card (g : G)228  requires finite : Finite(G)229  shows elementOrder(G, g) ∣ cardinality(G)230proof231  have finiteOrder := Group.finite_order with *232  have subgroup := powers.subgroup with *233  have divides := lagrange.theorem with group, subgroup, finite234  have same := powers.cardinality with *235  rw order.value at divides236  rwa same at divides237238theorem Group.pow_card (g : G)239  requires finite : Finite(G)240  shows g ^ cardinality(G) = G.one241proof242  have finiteOrder := Group.finite_order with *243  have cardNat := cardinality.nat with finite244  have divides := elementOrder.dvd_card with *245  exact elementOrder.pow_eq_one_of_dvd at G, g, cardinality(G) with *246247theorem elementOrder.le_card (g : G)248  requires finite : Finite(G)249  shows elementOrder(G, g) ≤ cardinality(G)250proof251  have finiteOrder := Group.finite_order with *252  have natural := elementOrder.natural with finiteOrder253  have cardNat := cardinality.nat with finite254  have subgroup := powers.subgroup with *255  have subset := Subgroup.subset with subgroup256  have bound := cardinality.monotone with finite, subset257  have same := powers.cardinality with *258  rwa same at bound259260end FiniteOrders261