Primes above a rational prime in an integral quadratic algebra

Let ℤ[ω] = QuadraticAlgebra ℤ a b, so ω² = a + b ω: the quadratic orders ℤ[√d] and ℤ[(1 + √d)/2] are of this shape. Here f = X² - b X - a denotes the minimal polynomial of ω and p a rational prime. This file describes the ideals of ℤ[ω] above p by explicit generators, following the Dedekind–Kummer recipe:

• if r is a root of f modulo p, then 𝔭_r = (p, ω - r) is the kernel of the evaluation ℤ[ω] → ℤ/p sending ω ↦ r. It is a maximal ideal with residue field of size p (isMaximal_span_natCast_omega_sub, card_quotient_span_natCast_omega_sub), and x ∈ 𝔭_r ↔ p ∣ x.re + x.im r;
• the second root is b - r, and the product formula (p, ω - r) (p, ω - (b - r)) = (p) holds exactly when p does not divide both f'(r) = 2r - b and f(r) / p (span_natCast_omega_sub_mul_span_natCast_omega_sub_eq_iff). This is the quadratic case of Dedekind's criterion, stated as an identity of ideals of the order ℤ[ω] itself, maximal or not. In the maximal order of a quadratic field it holds at every prime; in ℤ[√d] with d ≡ 1 (mod 4), an order of conductor 2, it fails at p = 2 (span_two_omega_sub_one_sq_ne_span_two);
• every prime of ℤ[ω] containing p is 𝔭_r or 𝔭_(b - r) (eq_or_eq_of_natCast_mem), whether or not the criterion holds; the two coincide exactly when p ∣ 2r - b, that is, when p divides the discriminant b² + 4a of f (span_natCast_omega_sub_eq_span_natCast_omega_sub_iff);
• if f has no root modulo p, then (p) itself is maximal, so p is inert (isMaximal_span_natCast_iff), and conversely;
• together, the primes of ℤ[ω] above p are exactly (p) when f has no root modulo p, and the ideals 𝔭_r otherwise (isPrime_and_natCast_mem_iff).

For a monogenic order inside a number field, Mathlib's Kummer–Dedekind theorem (KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk) describes the primes of the ring of integers above a prime not dividing the conductor, and TauCeti.NumberField.IntegralPrimitiveElement.not_dvd_index_iff decides when that hypothesis holds. The statements here need neither a Dedekind domain nor an ambient field.

References

• D. A. Cox, Primes of the Form x² + ny², §5.B and §7.D.
• J. Neukirch, Algebraic Number Theory, Chapter I, Proposition 8.3.

@[simp]

theorem QuadraticAlgebra.mem_span_natCast_omega_sub_iff {a b : ℤ} {p : ℕ} {r : ℤ} (hr : ↑p ∣ r ^ 2 - b * r - a) {x : QuadraticAlgebra ℤ a b} : x ∈ Ideal.span {↑p, omega - ↑r} ↔ ↑p ∣ x.re + x.im * r

Membership in (p, ω - r). For a root r of X² - b X - a modulo p, an element x of ℤ[ω] lies in (p, ω - r) exactly when p ∣ x.re + x.im r, that is, when x vanishes under ω ↦ r modulo p.

@[simp]

theorem QuadraticAlgebra.card_quotient_span_natCast_omega_sub {a b : ℤ} {p : ℕ} {r : ℤ} (hr : ↑p ∣ r ^ 2 - b * r - a) : Nat.card (QuadraticAlgebra ℤ a b ⧸ Ideal.span {↑p, omega - ↑r}) = p

The norm of (p, ω - r) is p. For a root r of X² - b X - a modulo p, the residue ring of (p, ω - r) is ℤ/p, so its Nat.card is p. For p ≠ 0 this says that it has exactly p elements; for p = 0 the residue ring is ℤ, which is infinite.

theorem QuadraticAlgebra.span_natCast_omega_sub_eq_iff {a b : ℤ} {p : ℕ} {r : ℤ} (hr : ↑p ∣ r ^ 2 - b * r - a) {s : ℤ} : Ideal.span {↑p, omega - ↑s} = Ideal.span {↑p, omega - ↑r} ↔ ↑p ∣ r - s

Two roots give the same ideal iff they agree modulo p. For a root r of X² - b X - a modulo p, the ideals (p, ω - s) and (p, ω - r) coincide exactly when s ≡ r (mod p). When p is prime these ideals are the primes above p (isMaximal_span_natCast_omega_sub).

theorem QuadraticAlgebra.isMaximal_span_natCast_omega_sub {a b : ℤ} {p : ℕ} {r : ℤ} [Fact (Nat.Prime p)] (hr : ↑p ∣ r ^ 2 - b * r - a) : (Ideal.span {↑p, omega - ↑r}).IsMaximal

The prime (p, ω - r). For a root r of X² - b X - a modulo p, the ideal (p, ω - r) of ℤ[ω] is maximal.

theorem QuadraticAlgebra.span_natCast_omega_sub_mul_span_natCast_omega_sub_eq_iff {a b : ℤ} {p : ℕ} {r : ℤ} [Fact (Nat.Prime p)] (hr : ↑p ∣ r ^ 2 - b * r - a) : Ideal.span {↑p, omega - ↑r} * Ideal.span {↑p, omega - ↑(b - r)} = Ideal.span {↑p} ↔ ¬(↑p ∣ 2 * r - b ∧ ↑p ^ 2 ∣ r ^ 2 - b * r - a)

Dedekind's criterion for a quadratic order. Let r be a root of X² - b X - a modulo p, so that b - r is the second root. Then p factors as (p) = (p, ω - r) (p, ω - (b - r)) in ℤ[ω] if and only if p does not divide both the derivative 2r - b and the quotient (r² - b r - a)/p, that is, unless p ∣ 2r - b and p² ∣ r² - b r - a.

theorem QuadraticAlgebra.span_natCast_omega_sub_sq_eq_iff {a b : ℤ} {p : ℕ} {r : ℤ} [Fact (Nat.Prime p)] (hr : ↑p ∣ r ^ 2 - b * r - a) (hs : ↑p ∣ 2 * r - b) : Ideal.span {↑p, omega - ↑r} ^ 2 = Ideal.span {↑p} ↔ ¬↑p ^ 2 ∣ r ^ 2 - b * r - a

The ramified case of Dedekind's criterion. If r is a double root of X² - b X - a modulo p (that is, p ∣ 2r - b), then (p) = (p, ω - r)² exactly when p² ∤ r² - b r - a.

theorem QuadraticAlgebra.span_two_omega_sub_one_sq_ne_span_two {d : ℤ} (hd4 : d % 4 = 1) : Ideal.span {2, omega - 1} ^ 2 ≠ Ideal.span {2}

Dedekind's criterion fails at the conductor. For d ≡ 1 (mod 4), the order ℤ[√d] has conductor 2 in ℤ[(1 + √d)/2], and Dedekind's criterion fails at 2: the maximal ideal (2, √d - 1) above 2 satisfies (2, √d - 1)² ≠ (2).

theorem QuadraticAlgebra.eq_or_eq_of_natCast_mem {a b : ℤ} {p : ℕ} {r : ℤ} [Fact (Nat.Prime p)] (hr : ↑p ∣ r ^ 2 - b * r - a) {P : Ideal (QuadraticAlgebra ℤ a b)} [P.IsPrime] (hP : ↑p ∈ P) : P = Ideal.span {↑p, omega - ↑r} ∨ P = Ideal.span {↑p, omega - ↑(b - r)}

The primes above a split or ramified p. If r is a root of X² - b X - a modulo p, every prime ideal of ℤ[ω] containing p is (p, ω - r) or (p, ω - (b - r)). This needs no Dedekind criterion, so it also holds at primes dividing the conductor of a nonmaximal order.

theorem QuadraticAlgebra.isMaximal_span_natCast_iff {a b : ℤ} {p : ℕ} [Fact (Nat.Prime p)] : (Ideal.span {↑p}).IsMaximal ↔ ∀ (r : ℤ), ¬↑p ∣ r ^ 2 - b * r - a

The inert case. The ideal (p) of ℤ[ω] is maximal, that is, p is inert, exactly when X² - b X - a has no root modulo p.

theorem QuadraticAlgebra.span_natCast_omega_sub_eq_span_natCast_omega_sub_iff {a b : ℤ} {p : ℕ} {r : ℤ} [Fact (Nat.Prime p)] (hr : ↑p ∣ r ^ 2 - b * r - a) : Ideal.span {↑p, omega - ↑r} = Ideal.span {↑p, omega - ↑(b - r)} ↔ ↑p ∣ b ^ 2 + 4 * a

When the two primes above p coincide. For a root r of X² - b X - a modulo p, the ideals (p, ω - r) and (p, ω - (b - r)) coincide exactly when p divides the discriminant b² + 4a of X² - b X - a.

theorem QuadraticAlgebra.isPrime_and_natCast_mem_iff {a b : ℤ} {p : ℕ} [Fact (Nat.Prime p)] {P : Ideal (QuadraticAlgebra ℤ a b)} : P.IsPrime ∧ ↑p ∈ P ↔ (P = Ideal.span {↑p} ∧ ∀ (r : ℤ), ¬↑p ∣ r ^ 2 - b * r - a) ∨ ∃ (r : ℤ), ↑p ∣ r ^ 2 - b * r - a ∧ P = Ideal.span {↑p, omega - ↑r}

The primes above p. A prime ideal P of ℤ[ω] contains the rational prime p exactly when either X² - b X - a has no root modulo p and P = (p), or P = (p, ω - r) for a root r of X² - b X - a modulo p. This lists every prime of ℤ[ω] above p, including at primes dividing the conductor of a nonmaximal order.