Orders of elements and cardinalities

Let g have finite order n and let f divide n. The order of g ^ k is n / gcd n k, so f divides it exactly when f * gcd n k divides n. That condition is decided one prime of f at a time: it fails at p exactly when k is divisible by p ^ (v_p n - v_p f + 1), the room n leaves at p after f, plus one.

In a finite additive group with one, the cardinality casts to 0, as Mathlib's Nat.cast_card_eq_zero records, so the cardinality minus one casts to -1.

By Euler's theorem, raising an n-th root of unity to the power q ^ φ(n), for q prime to n, does nothing.

An element squaring to 1 only sees the parity of its exponent, so identities between products of powers of such elements reduce to congruences modulo 2 between the exponents.

If conjugation by s raises an element t of finite order to a power q, then q is prime to the order of t, since conjugation preserves orders, and so s normalizes the cyclic subgroup ⟨t⟩. This is the finite shadow of a relation s t s⁻¹ = t ^ q, such as the one between Frobenius and tame inertia.

Main results

• IsOfFinOrder.dvd_orderOf_pow_iff, and its additive counterpart: divisibility of the order of a power as non-divisibility of its exponent by a prime power at each prime of f.
• TauCeti.natCast_natCard_sub_one_eq_neg_one: in a finite additive group with one of cardinality q, the cast of q - 1 is -1, a companion of Mathlib's Nat.cast_card_eq_zero.
• TauCeti.pow_pow_totient_eq_self: x ^ q ^ φ(n) = x whenever x ^ n = 1 and q is prime to n.
• TauCeti.mul_pow_eq_of_sq_eq_one: in a commutative monoid, exponents of elements squaring to 1 only matter modulo 2.
• TauCeti.coprime_orderOf_of_mul_mul_inv_eq_pow, TauCeti.mem_normalizer_zpowers_of_mul_mul_inv_eq_pow: if s * t * s⁻¹ = t ^ q with t of finite order, then q is prime to the order of t and s normalizes ⟨t⟩.

theorem IsOfFinOrder.dvd_orderOf_pow_iff {G : Type u_1} [Monoid G] {g : G} (hg : IsOfFinOrder g) {f : ℕ} (hf : f ∣ orderOf g) (k : ℕ) : f ∣ orderOf (g ^ k) ↔ ∀ p ∈ f.primeFactors, ¬p ^ ((orderOf g).factorization p - f.factorization p + 1) ∣ k

When a number divides the order of a power. Let g have finite order and let f divide that order. Then f divides the order of g ^ k exactly when, for every prime p of f, the exponent k is not divisible by p ^ (v_p (orderOf g) - v_p f + 1).

The exponent is the room orderOf g leaves at p after f has taken v_p f, plus one: the order of g ^ k is orderOf g / gcd (orderOf g) k, so k may absorb at most v_p (orderOf g) - v_p f powers of p; the first forbidden exponent is that room plus one.

theorem IsOfFinAddOrder.dvd_addOrderOf_nsmul_iff {G : Type u_1} [AddMonoid G] {g : G} (hg : IsOfFinAddOrder g) {f : ℕ} (hf : f ∣ addOrderOf g) (k : ℕ) : f ∣ addOrderOf (k • g) ↔ ∀ p ∈ f.primeFactors, ¬p ^ ((addOrderOf g).factorization p - f.factorization p + 1) ∣ k

When a number divides the additive order of a multiple. Let g have finite additive order and let f divide that order. Then f divides the additive order of k • g exactly when, for every prime p of f, the exponent k is not divisible by p ^ (v_p (addOrderOf g) - v_p f + 1).

theorem TauCeti.natCast_natCard_sub_one_eq_neg_one (R : Type u_1) [AddGroupWithOne R] [Finite R] : ↑(Nat.card R - 1) = -1

In a finite additive group with one of cardinality q, the cast of q - 1 is -1.

theorem TauCeti.pow_pow_totient_eq_self {M : Type u_1} [Monoid M] {q n : ℕ} (hq : q.Coprime n) {x : M} (hx : x ^ n = 1) : x ^ q ^ n.totient = x

Euler's theorem on an n-th root of unity: if x ^ n = 1 in a monoid and q is prime to n, then x ^ q ^ φ(n) = x, since q ^ φ(n) ≡ 1 [MOD n].

theorem TauCeti.mul_pow_eq_of_sq_eq_one {G : Type u_1} [CommMonoid G] {S u v w z : G} (hu : u ^ 2 = 1) (hv : v ^ 2 = 1) (hw : w ^ 2 = 1) (hz : z ^ 2 = 1) {A B C D E F : ℕ} (hF : F ≡ A + D [MOD 2]) (hE : E ≡ A [MOD 2]) (hBC : E ≡ B + C [MOD 2]) (hB : 1 ≡ B [MOD 2]) : S * (u * v) ^ A * (w * z) ^ B * w ^ C * u ^ D = S * z * (v * w) ^ E * u ^ F

Only parities matter for 2-torsion exponents. In a commutative monoid whose elements u, v, w, z square to 1, an identity between products of their powers holds as soon as the exponents agree modulo 2: here S * (u * v) ^ A * (w * z) ^ B * w ^ C * u ^ D regroups as S * z * (v * w) ^ E * u ^ F. This is the sign bookkeeping behind induction steps on products of quaternion symbols with binomial exponents.

theorem TauCeti.coprime_orderOf_of_mul_mul_inv_eq_pow {G : Type u_1} [Group G] {s t : G} {q : ℕ} (ht : IsOfFinOrder t) (h : s * t * s⁻¹ = t ^ q) : q.Coprime (orderOf t)

A conjugate power is a coprime power. If conjugation by s sends an element t of finite order to t ^ q, then q is prime to the order of t: conjugation preserves orders, and the order of t ^ q is orderOf t / gcd (orderOf t) q.

theorem TauCeti.mem_normalizer_zpowers_of_mul_mul_inv_eq_pow {G : Type u_1} [Group G] {s t : G} {q : ℕ} (ht : IsOfFinOrder t) (h : s * t * s⁻¹ = t ^ q) : s ∈ Subgroup.normalizer ↑(Subgroup.zpowers t)

A conjugate power normalizes the cyclic subgroup. If conjugation by s sends an element t of finite order to t ^ q, then s normalizes the cyclic subgroup generated by t. Since q is prime to the order of t, conjugation by s⁻¹ is a power map on it as well.