Units congruent to one modulo a prime

For a prime p, the units of ZMod (p ^ (k + 1)) that reduce to 1 in ZMod p form the kernel of the reduction ZMod.unitsMap. That kernel has p ^ k elements, so raising to a power n coprime to p permutes it. In particular, for an odd prime p every unit congruent to one modulo p is a square modulo every power of p. This is the finite-level, group-order form of the Hensel argument for principal units.

Consequently, for n coprime to p and an integer a prime to p, reduction modulo p is a bijection from the n-th roots of a modulo p ^ k (k ≠ 0) to those modulo p. Surjectivity is Hensel's lemma TauCeti.HenselianLocalRing.exists_pow_eq_of_residue_pow_eq in the Henselian local ring ZMod (p ^ k), and injectivity holds because two n-th roots of a with the same reduction differ by a principal unit whose n-th power is 1.

Main results

• ZMod.card_ker_unitsMap_mul_totient: for n ∣ m with m ≠ 0, the kernel of (ZMod m)ˣ → (ZMod n)ˣ has φ m / φ n elements.
• ZMod.card_ker_unitsMap_prime_pow: the kernel of (ZMod (p ^ (k + 1)))ˣ → (ZMod p)ˣ has p ^ k elements.
• ZMod.existsUnique_pow_eq_of_unitsMap_eq_one: for n coprime to p, a unit congruent to one modulo p has a unique n-th root among the units congruent to one modulo p.
• ZMod.isSquare_of_unitsMap_eq_one: for an odd prime p, a unit of ZMod (p ^ (k + 1)) congruent to one modulo p is a square.
• ZMod.natCard_nthRoots_prime_pow_eq_natCard_nthRoots: for n coprime to p, a unit a has as many n-th roots modulo p ^ k as modulo p.

References

• Keith Conrad, Hensel's lemma, Example 2.8.

theorem ZMod.card_ker_unitsMap_mul_totient {m n : ℕ} [NeZero m] (h : n ∣ m) : Nat.card ↥(unitsMap h).ker * n.totient = m.totient

The kernel of the reduction (ZMod m)ˣ → (ZMod n)ˣ along n ∣ m has φ m / φ n elements, stated without division.

theorem ZMod.card_ker_unitsMap_prime_pow {p : ℕ} (hp : Nat.Prime p) (k : ℕ) (h : p ∣ p ^ (k + 1)) : Nat.card ↥(unitsMap h).ker = p ^ k

The units of ZMod (p ^ (k + 1)) congruent to one modulo the prime p form a subgroup with p ^ k elements.

theorem ZMod.existsUnique_pow_eq_of_unitsMap_eq_one {p k n : ℕ} (hp : Nat.Prime p) (hn : n.Coprime p) {h : p ∣ p ^ (k + 1)} {u : (ZMod (p ^ (k + 1)))ˣ} (hu : (unitsMap h) u = 1) : ∃! v : (ZMod (p ^ (k + 1)))ˣ, (unitsMap h) v = 1 ∧ v ^ n = u

n-th roots of units congruent to one modulo a prime. If n is coprime to the prime p, every unit of ZMod (p ^ (k + 1)) congruent to one modulo p has exactly one n-th root among the units congruent to one modulo p.

theorem ZMod.isSquare_of_unitsMap_eq_one {p k : ℕ} (hp : Nat.Prime p) (hp2 : p ≠ 2) {h : p ∣ p ^ (k + 1)} {u : (ZMod (p ^ (k + 1)))ˣ} (hu : (unitsMap h) u = 1) : IsSquare u

Units congruent to one modulo an odd prime are squares. For an odd prime p, every unit of ZMod (p ^ (k + 1)) whose reduction to ZMod p is 1 is a square of a unit.

theorem ZMod.natCard_nthRoots_prime_pow_eq_natCard_nthRoots {p n k : ℕ} [Fact (Nat.Prime p)] (hn : n.Coprime p) (hk : k ≠ 0) {a : ℤ} (ha : ↑a ≠ 0) : Nat.card { x : ZMod (p ^ k) // x ^ n = ↑a } = Nat.card { x : ZMod p // x ^ n = ↑a }

Hensel's lemma for n-th roots, as a count. For n coprime to the prime p, an integer a prime to p and k ≠ 0, reduction modulo p is a bijection from the n-th roots of a modulo p ^ k to those modulo p; so there are equally many.

Modulo 9, the units 4 and 7 are 2 ^ 2 and 4 ^ 2. The hypothesis that p is odd is needed: 5 is congruent to one modulo 2 but is not a square modulo 8.