The prime-splitting law for a quadratic field

For a quadratic number field K = ℚ(√d) — given as K generated over ℚ by an algebraic integer θ whose minimal polynomial over ℤ is X² - d — and an odd prime p not dividing d, the prime p splits completely in K (there are [K:ℚ] = 2 primes of 𝓞 K above it) if and only if d is a quadratic residue mod p, i.e. legendreSym p d = 1.

The proof routes through Mathlib's number-field Kummer–Dedekind theorem (primesOverSpanEquivMonicFactorsMod): the primes above p biject with the monic irreducible factors of X² - d mod p, of which there are two exactly when d is a square mod p. The required conductor hypothesis p ∤ exponent θ follows because the conductor exponent divides the power-basis discriminant 4d, which is coprime to the odd prime p ∤ d.

This is the base case n = 1 of the multiquadratic prime-splitting law.

The splitting law is then read off at the level of ideals: a completely split rational prime is the absolute norm of a prime of 𝓞 K (Ideal.absNorm_eq_of_ncard_primesOver_eq_finrank). That is the shape in which the splitting law enters genus theory, where an ideal of norm p is what carries the prescribed values of the genus characters.

The prime 2 is handled separately, through the count of primes above 2 for a generator with minimal polynomial X² - X + c and odd conductor exponent (NumberField.ncard_primesOver_two_of_minpoly_eq_X_sq_sub_X_add, in TauCeti.NumberTheory.NumberField.Ideal.KummerDedekind). Such a generator always has odd conductor exponent, since X² - X + c is separable modulo 2 (not_two_dvd_exponent_of_minpoly_eq_X_sq_sub_X_add, in the same file). For c = (1 - d)/4 with d ≡ 1 (mod 4), the presentation of ℚ(√d) by (1 + √d)/2, 2 splits exactly when d ≡ 1 (mod 8) and is inert exactly when d ≡ 5 (mod 8). For K = ℚ(√d) presented by θ with θ² = d and d ≡ 1 (mod 4), the half-integer generator (1 + θ)/2 (halfGen) has minimal polynomial X² - X + (1 - d)/4 (minpoly_halfGen) and generates K over ℚ (adjoin_rat_halfGen_eq_top), and (1 - d)/4 is even exactly when d ≡ 1 (mod 8); the generator θ itself is useless here, since 2 divides its conductor exponent. No squarefreeness of d is needed.

Main results

• NumberField.ncard_primesOver_quadratic_iff: the quadratic splitting law at an odd prime.
• NumberField.exists_isPrime_and_absNorm_eq_of_legendreSym_eq_one: an odd prime p with legendreSym p d = 1 is the absolute norm of a prime ideal of 𝓞 K.
• NumberField.ncard_primesOver_two_eq_finrank_iff_of_minpoly_eq_X_sq_sub_X_add and NumberField.ncard_primesOver_two_eq_one_iff_of_minpoly_eq_X_sq_sub_X_add: for a generator with minimal polynomial X² - X + (1 - d)/4 and d ≡ 1 (mod 4), 2 splits iff d ≡ 1 (mod 8) and is inert iff d ≡ 5 (mod 8).
• NumberField.ncard_primesOver_two_of_mod_four_eq_one: the number of primes above 2 is if d % 8 = 1 then 2 else 1 for ℚ(√d) with d ≡ 1 (mod 4), presented by √d, with the corollaries NumberField.ncard_primesOver_two_eq_finrank_iff_of_mod_four_eq_one (2 splits iff d ≡ 1 (mod 8)) and NumberField.ncard_primesOver_two_eq_one_iff_of_mod_four_eq_one (2 is inert iff d ≡ 5 (mod 8)).

References

• J. Neukirch, Algebraic Number Theory, Chapter I, §8, Proposition (8.3).

theorem NumberField.ncard_primesOver_quadratic_iff {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) {p : ℕ} [Fact (Nat.Prime p)] (hodd : p ≠ 2) (hcop : ¬↑p ∣ d) : ((Ideal.span {↑p}).primesOver (RingOfIntegers K)).ncard = Module.finrank ℚ K ↔ legendreSym p d = 1

The quadratic splitting law. For K = ℚ(√d) (θ a square root of the integer d generating K) and an odd prime p ∤ d, p splits completely in K iff d is a quadratic residue mod p. This is the n = 1 case of the multiquadratic prime-splitting law.

theorem NumberField.exists_isPrime_and_absNorm_eq_of_legendreSym_eq_one {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) {p : ℕ} [Fact (Nat.Prime p)] (hodd : p ≠ 2) (hleg : legendreSym p d = 1) : ∃ (𝔭 : Ideal (RingOfIntegers K)), 𝔭.IsPrime ∧ 𝔭.LiesOver (Ideal.span {↑p}) ∧ Ideal.absNorm 𝔭 = p

A split prime is an ideal norm. For K = ℚ(√d) and an odd prime p for which d is a quadratic residue mod p — that is, one which splits in K by ncard_primesOver_quadratic_iff — there is a prime ideal of 𝓞 K of absolute norm p. This is the form in which the splitting law feeds genus theory: the genus characters are computed on ideals through their absolute norms.

The prime 2 for d ≡ 1 (mod 4)

theorem NumberField.ncard_primesOver_two_eq_finrank_iff_of_minpoly_eq_X_sq_sub_X_add {K : Type u_1} [Field K] [NumberField K] {ω : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ ω = Polynomial.X ^ 2 - Polynomial.X + Polynomial.C ((1 - d) / 4)) (hgen : ℚ[↑ω] = ⊤) (hd4 : d % 4 = 1) : ((Ideal.span {2}).primesOver (RingOfIntegers K)).ncard = Module.finrank ℚ K ↔ d % 8 = 1

The splitting law at 2 for a generator with minimal polynomial X² - X + (1 - d)/4. Let K be generated over ℚ by an algebraic integer ω with minimal polynomial X² - X + (1 - d)/4 over ℤ, where d ≡ 1 (mod 4) — the presentation of ℚ(√d) by ω = (1 + √d)/2. Then 2 splits completely in K if and only if d ≡ 1 (mod 8).

theorem NumberField.ncard_primesOver_two_eq_one_iff_of_minpoly_eq_X_sq_sub_X_add {K : Type u_1} [Field K] [NumberField K] {ω : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ ω = Polynomial.X ^ 2 - Polynomial.X + Polynomial.C ((1 - d) / 4)) (hgen : ℚ[↑ω] = ⊤) (hd4 : d % 4 = 1) : ((Ideal.span {2}).primesOver (RingOfIntegers K)).ncard = 1 ↔ d % 8 = 5

The inert case at 2 for a generator with minimal polynomial X² - X + (1 - d)/4. Let K be generated over ℚ by an algebraic integer ω with minimal polynomial X² - X + (1 - d)/4 over ℤ, where d ≡ 1 (mod 4). Then 2 is inert in K (there is a single prime above it) if and only if d ≡ 5 (mod 8).

theorem NumberField.ncard_primesOver_two_of_mod_four_eq_one {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hd4 : d % 4 = 1) : ((Ideal.span {2}).primesOver (RingOfIntegers K)).ncard = if d % 8 = 1 then 2 else 1

The number of primes above 2 for d ≡ 1 (mod 4). For K = ℚ(√d) with d ≡ 1 (mod 4), there are two primes of 𝓞 K above 2 when d ≡ 1 (mod 8) and one when d ≡ 5 (mod 8): the half-integer generator (1 + √d)/2 has minimal polynomial X² - X + (1 - d)/4 and odd conductor exponent, and (1 - d)/4 is even exactly when d ≡ 1 (mod 8).

theorem NumberField.ncard_primesOver_two_eq_finrank_iff_of_mod_four_eq_one {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hd4 : d % 4 = 1) : ((Ideal.span {2}).primesOver (RingOfIntegers K)).ncard = Module.finrank ℚ K ↔ d % 8 = 1

The splitting law at 2 for d ≡ 1 (mod 4). For K = ℚ(√d) with d ≡ 1 (mod 4), the prime 2 splits completely in K if and only if d ≡ 1 (mod 8).

theorem NumberField.ncard_primesOver_two_eq_one_iff_of_mod_four_eq_one {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hd4 : d % 4 = 1) : ((Ideal.span {2}).primesOver (RingOfIntegers K)).ncard = 1 ↔ d % 8 = 5

The inert case at 2 for d ≡ 1 (mod 4). For K = ℚ(√d) with d ≡ 1 (mod 4), the prime 2 is inert in K (there is a single prime above it) if and only if d ≡ 5 (mod 8).