Counting solutions of the congruences x² + 1 ≡ 0 and x² - x + 1 ≡ 0

For an odd prime p and an integer a prime to p, reduction modulo p is a bijection from the square roots of a modulo p ^ k (k ≥ 1) to those modulo p, by Hensel's lemma ZMod.natCard_nthRoots_prime_pow_eq_natCard_nthRoots. So their number is 1 + (a | p) at every level p ^ k.

Combined with the Chinese remainder theorem this counts the solutions of x² + 1 ≡ 0 (mod N) and of x² - x + 1 ≡ 0 (mod N). Away from 2, the first congruence asks for a square root of -1; completing the square, 4 (x² - x + 1) = (2 x - 1)² + 3, the second asks away from 2 for a square root of -3, and (-3 | p) = (p | 3). The primes 2 and 3, where the discriminants -4 and -3 are not prime to p, are computed directly: x² + 1 ≡ 0 has one solution modulo 2 and none modulo 4, and x² - x + 1 ≡ 0 has none modulo 2, one modulo 3 and none modulo 9. The resulting counts are

• #{x mod N | x² + 1 = 0} = 0 if 4 ∣ N, and ∏_{p ∣ N} (1 + χ₄(p)) otherwise;
• #{x mod N | x² - x + 1 = 0} = 0 if 9 ∣ N, and ∏_{p ∣ N} (1 + (p | 3)) otherwise,

where χ₄ is the character of ℤ/4ℤ, so that χ₄(p) = (-1 | p) for odd p and χ₄(2) = 0. They hold also for N = 0, as neither polynomial has an integer root. These are the numbers of elliptic points of order two and three of Γ₀(N).

Main results

• TauCeti.ZMod.natCard_sqrts_prime_pow_eq_legendreSym_add_one: the count 1 + (a | p) of square roots of a unit a modulo p ^ k.
• TauCeti.ZMod.natCard_sq_add_one_eq_zero: the number of roots of x² + 1 modulo N.
• TauCeti.ZMod.natCard_sq_sub_self_add_one_eq_zero: the number of roots of x² - x + 1 modulo N.

References

• F. Diamond and J. Shurman, A First Course in Modular Forms, Corollary 3.7.2.
• G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Proposition 1.43.
• K. Ireland and M. Rosen, A Classical Introduction to Modern Number Theory, Chapter 4, §2.

Square roots modulo odd prime powers

theorem TauCeti.ZMod.natCard_sqrts_prime_pow_eq_legendreSym_add_one {p : ℕ} [Fact (Nat.Prime p)] (hp : p ≠ 2) {k : ℕ} (hk : k ≠ 0) {a : ℤ} (ha : ↑a ≠ 0) : ↑(Nat.card { x : ZMod (p ^ k) // x ^ 2 = ↑a }) = legendreSym p a + 1

Square roots modulo odd prime powers. For an odd prime p, an integer a prime to p and k ≠ 0, the number of square roots of a modulo p ^ k is 1 + (a | p).

The congruence x² + 1 ≡ 0

theorem TauCeti.ZMod.natCard_sq_add_one_eq_zero_prime_pow {p : ℕ} [Fact (Nat.Prime p)] (hp : p ≠ 2) {k : ℕ} (hk : k ≠ 0) : ↑(Nat.card { x : ZMod (p ^ k) // x ^ 2 + 1 = 0 }) = 1 + ZMod.χ₄ ↑p

Modulo an odd prime power p ^ k, k ≠ 0, the polynomial x² + 1 has 1 + χ₄(p) roots.

theorem TauCeti.ZMod.natCard_sq_add_one_eq_zero (N : ℕ) : ↑(Nat.card { x : ZMod N // x ^ 2 + 1 = 0 }) = if 4 ∣ N then 0 else ∏ p ∈ N.primeFactors, (1 + ZMod.χ₄ ↑p)

Square roots of -1 modulo N. The polynomial x² + 1 has no roots modulo N if 4 ∣ N, and otherwise ∏_{p ∣ N} (1 + χ₄(p)) roots, where χ₄(p) = (-1 | p) for odd p and χ₄(2) = 0.

The congruence x² - x + 1 ≡ 0

theorem TauCeti.ZMod.natCard_sq_sub_self_add_one_eq_zero_prime_pow {p : ℕ} [Fact (Nat.Prime p)] (hp3 : p ≠ 3) {k : ℕ} (hk : k ≠ 0) : ↑(Nat.card { x : ZMod (p ^ k) // x ^ 2 - x + 1 = 0 }) = 1 + legendreSym 3 ↑p

Modulo a power p ^ k, k ≠ 0, of a prime p ≠ 3, the polynomial x² - x + 1 has 1 + (p | 3) roots. At p = 2 there are none, as (2 | 3) = -1.

theorem TauCeti.ZMod.natCard_sq_sub_self_add_one_eq_zero (N : ℕ) : ↑(Nat.card { x : ZMod N // x ^ 2 - x + 1 = 0 }) = if 9 ∣ N then 0 else ∏ p ∈ N.primeFactors, (1 + legendreSym 3 ↑p)

Roots of x² - x + 1 modulo N. The polynomial x² - x + 1 has no roots modulo N if 9 ∣ N, and otherwise ∏_{p ∣ N} (1 + (p | 3)) roots. The factor 1 + (p | 3) is 0 at p = 2, 1 at p = 3, and 1 + (-3 | p) at every other prime.