The d-th power criterion in a finite cyclic group

Let G be a finite cyclic commutative group of order N and let d be any natural number, not assumed to divide N. Write g = gcd(N, d). The d-th powers of G are exactly the elements killed by the (N / g)-th power map, and they form the unique subgroup of order N / g. In particular a is a d-th power exactly when a ^ (N / g) = 1. For d = 0 the exponent is N / N = 1 and the criterion reads a = 1; for d dividing N it is the familiar a ^ (N / d) = 1, which for the units modulo an odd prime and d = 2 is Euler's criterion.

This is the group theory behind the n-th power residue criteria: applied to the cyclic unit group of a finite field it decides which elements are n-th powers, and the kernel of the d-th power map (of order g, Mathlib's IsCyclic.card_powMonoidHom_ker) counts their roots.

The inclusion of the image in the kernel holds in any group of order N, indeed for any x with x ^ N = 1 in a monoid; it is TauCeti.pow_pow_div_gcd_eq_one in TauCeti.GroupTheory.OrderOfElement.Basic. That the d-th powers are the gcd(N, d)-th powers holds in any commutative group of order N, indeed of exponent dividing N; it is TauCeti.range_powMonoidHom_gcd in TauCeti.Algebra.Group.PowMonoidHom.

Main results

• IsCyclic.range_powMonoidHom_eq_ker: in a finite cyclic group the image of the d-th power map is the kernel of the (N / gcd(N, d))-th power map.
• IsCyclic.mem_range_powMonoidHom_iff: a is a d-th power iff a ^ (N / gcd(N, d)) = 1.

Each result has an additive version, stated for nsmulAddMonoidHom in an additive cyclic group (IsAddCyclic.range_nsmulAddMonoidHom_eq_ker, IsAddCyclic.mem_range_nsmulAddMonoidHom_iff).

That the d-th powers form the unique subgroup of order N / gcd(N, d) is already Mathlib's IsCyclic.subgroup_eq_iff_card_eq combined with IsCyclic.card_powMonoidHom_range; an example below applies it.

References

• Victor Shoup, A Computational Introduction to Number Theory and Algebra (2nd ed.), Theorem 6.32 (iii) and (vi), and Example 7.61.

theorem IsCyclic.range_powMonoidHom_eq_ker {G : Type u_1} [CommGroup G] [IsCyclic G] [Finite G] (d : ℕ) : (powMonoidHom d).range = (powMonoidHom (Nat.card G / (Nat.card G).gcd d)).ker

The d-th power criterion in a finite cyclic group, as an equality of subgroups: the image of the d-th power map of a finite cyclic group of order N is the kernel of the (N / gcd(N, d))-th power map.

theorem IsAddCyclic.range_nsmulAddMonoidHom_eq_ker {G : Type u_1} [AddCommGroup G] [IsAddCyclic G] [Finite G] (d : ℕ) : (nsmulAddMonoidHom d).range = (nsmulAddMonoidHom (Nat.card G / (Nat.card G).gcd d)).ker

The d-th multiple criterion in a finite additive cyclic group, as an equality of subgroups: the image of multiplication by d on a finite additive cyclic group of order N is the kernel of multiplication by N / gcd(N, d).

theorem IsCyclic.mem_range_powMonoidHom_iff {G : Type u_1} [CommGroup G] [IsCyclic G] [Finite G] (d : ℕ) (x : G) : x ∈ (powMonoidHom d).range ↔ x ^ (Nat.card G / (Nat.card G).gcd d) = 1

The d-th power criterion in a finite cyclic group. In a finite cyclic group of order N, an element x is a d-th power exactly when x ^ (N / gcd(N, d)) = 1. The natural number d is arbitrary: when d ∣ N the exponent is N / d, and when d = 0 the criterion reads x = 1.

theorem IsAddCyclic.mem_range_nsmulAddMonoidHom_iff {G : Type u_1} [AddCommGroup G] [IsAddCyclic G] [Finite G] (d : ℕ) (x : G) : x ∈ (nsmulAddMonoidHom d).range ↔ (Nat.card G / (Nat.card G).gcd d) • x = 0

The d-th multiple criterion in a finite additive cyclic group. In a finite additive cyclic group of order N, an element x is a d-th multiple exactly when (N / gcd(N, d)) • x = 0.

Examples