Ramification of primes in a quadratic field

For a quadratic number field K = ℚ(√d) (given by θ : 𝓞 K with minpoly ℤ θ = X² - d and Algebra.adjoin ℚ {θ} = ⊤, d squarefree), a rational prime p ramifies iff it divides the discriminant, which is fundamentalDiscriminant d. Concretely:

• p is unramified in 𝓞 K iff p ∤ fundamentalDiscriminant d;
• for p ∤ 2 (an odd prime up to sign), p is unramified iff p ∤ d — i.e. the ramified odd primes are exactly those dividing the radicand d.

This is the finite-prime half of the Layer-1 ramified-prime behaviour of the multiquadratic roadmap. It combines Mathlib's NumberField.not_dvd_discr_iff_isUnramifiedIn with the quadratic discriminant computation TauCeti.Multiquadratic.discr_eq_fundamentalDiscriminant.

The second half of the file counts the ramified primes. Writing fundamentalDiscriminant d as a product of prime discriminants (IsFundamentalDiscriminant.exists_finset_primeDiscriminant), each factor contributes exactly one ramified prime — the prime primeDiscriminantPrime lying under it — and distinct factors contribute distinct primes. So the number t of ramified primes of ℚ(√d) is the number of prime discriminants in that factorization: the t of the genus-theory 2-rank formula and of the degree 2 ^ t of the candidate genus field. The one-factor case is recorded separately: a single prime ramifies in the quadratic field of a prime discriminant, which is what the name "prime discriminant" refers to.

Main results

• TauCeti.Multiquadratic.isUnramifiedIn_iff_not_dvd_fundamentalDiscriminant.
• TauCeti.Multiquadratic.isUnramifiedIn_iff_not_dvd_of_not_dvd_two: odd primes.
• TauCeti.Multiquadratic.isUnramifiedIn_two_iff_mod_four_eq_one: the prime 2.
• TauCeti.Multiquadratic.mem_ramifiedPrimes_adjoin_iff_dvd_fundamentalDiscriminant: the ramified primes of the field generated by a square root, including the square radicand 1.
• TauCeti.Multiquadratic.ramifiedPrimes_eq_singleton: exactly one prime ramifies in the quadratic field of a prime discriminant.
• TauCeti.Multiquadratic.ramifiedPrimes_eq_image: the ramified primes of ℚ(√d) are the primes under the prime discriminants dividing its discriminant.
• TauCeti.Multiquadratic.ncard_ramifiedPrimes_eq_card: hence there are as many ramified primes as prime-discriminant factors.
• TauCeti.Multiquadratic.map_span_eq_sq_of_dvd_fundamentalDiscriminant: a prime dividing the discriminant is totally ramified, p 𝓞 K = 𝔭 ^ 2.
• TauCeti.Multiquadratic.map_span_primeDiscriminantPrime_eq_sq: the same for the single prime ramifying in the quadratic field of a prime discriminant.

theorem TauCeti.Multiquadratic.isUnramifiedIn_iff_not_dvd_fundamentalDiscriminant {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d) {p : ℤ} (hp : Prime p) : Algebra.IsUnramifiedIn (NumberField.RingOfIntegers K) (Ideal.span {p}) ↔ ¬p ∣ fundamentalDiscriminant d

Ramification via the discriminant. A rational prime p is unramified in 𝓞 K iff it does not divide fundamentalDiscriminant d (the field discriminant).

theorem TauCeti.Multiquadratic.isUnramifiedIn_iff_not_dvd_of_not_dvd_two {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d) {p : ℤ} (hp : Prime p) (hp2 : ¬p ∣ 2) : Algebra.IsUnramifiedIn (NumberField.RingOfIntegers K) (Ideal.span {p}) ↔ ¬p ∣ d

The ramified odd primes are the divisors of the radicand. For a prime p ∤ 2, p is unramified in 𝓞 K iff p ∤ d.

theorem TauCeti.Multiquadratic.isUnramifiedIn_two_iff_mod_four_eq_one {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d) : Algebra.IsUnramifiedIn (NumberField.RingOfIntegers K) (Ideal.span {2}) ↔ d % 4 = 1

2 ramifies iff d ≢ 1 (mod 4). The prime 2 is unramified in 𝓞 K iff d ≡ 1 (mod 4).

Counting the ramified primes

theorem TauCeti.Multiquadratic.mem_ramifiedPrimes_iff_dvd_fundamentalDiscriminant {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d) {p : ℕ} (hp : Nat.Prime p) : p ∈ NumberField.ramifiedPrimes K ↔ ↑p ∣ fundamentalDiscriminant d

The ramified primes of ℚ(√d). A natural prime lies in ramifiedPrimes K exactly when it divides fundamentalDiscriminant d.

theorem TauCeti.Multiquadratic.mem_ramifiedPrimes_adjoin_iff_dvd_fundamentalDiscriminant {M : Type u_2} [Field M] [NumberField M] {a : ℤ} (hsf : Squarefree a) {x : M} (hx : x ^ 2 = (algebraMap ℤ M) a) {p : ℕ} (hp : Nat.Prime p) : p ∈ NumberField.ramifiedPrimes ↥ℚ⟮x⟯ ↔ ↑p ∣ fundamentalDiscriminant a

The ramified primes of a subfield generated by a square root. For squarefree a and x ∈ M with x ^ 2 = a, a rational prime ramifies in ℚ(x) exactly when it divides fundamentalDiscriminant a. If a is a rational square, squarefreeness forces a = 1, and ℚ(x) = ℚ is unramified.

theorem TauCeti.Multiquadratic.ramifiedPrimes_eq_singleton {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {D : ℤ} (hD : IsPrimeDiscriminant D) (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C (primeDiscriminantRadicand D)) (hgen : ℚ[↑θ] = ⊤) : NumberField.ramifiedPrimes K = {primeDiscriminantPrime D}

Exactly one rational prime ramifies in the quadratic field of a prime discriminant. If D is a prime discriminant and K = ℚ(√(primeDiscriminantRadicand D)), then the ramified primes of K are the single prime primeDiscriminantPrime D lying under D. This is the defining property of a prime discriminant, and the base case of the count below.

theorem TauCeti.Multiquadratic.ramifiedPrimes_eq_image {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {d : ℤ} {s : Finset ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d) (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (hprod : ∏ P ∈ s, P = fundamentalDiscriminant d) : NumberField.ramifiedPrimes K = ↑(Finset.image primeDiscriminantPrime s)

The ramified primes of ℚ(√d) are the primes under the prime discriminants dividing its discriminant. If s is a finite set of prime discriminants with product fundamentalDiscriminant d, then the ramified primes of K = ℚ(√d) are exactly the primes primeDiscriminantPrime P for P ∈ s: a prime divides the product iff it divides some factor, and a prime discriminant has just one prime divisor.

theorem TauCeti.Multiquadratic.ncard_ramifiedPrimes_eq_card {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {d : ℤ} {s : Finset ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d) (hs : ∀ P ∈ s, IsPrimeDiscriminant P) (heven : ∀ P ∈ s, ∀ Q ∈ s, IsEvenPrimeDiscriminant P → IsEvenPrimeDiscriminant Q → P = Q) (hprod : ∏ P ∈ s, P = fundamentalDiscriminant d) : (NumberField.ramifiedPrimes K).ncard = s.card

The number of ramified primes of ℚ(√d) is the number of prime discriminants dividing its discriminant. This is the t of genus theory: the exponent in the degree 2 ^ t of the candidate genus field, and the t of the 2-rank formula t - 1. Distinct prime-discriminant factors give distinct ramified primes because only the three even prime discriminants share a prime, and s contains at most one of them.

theorem TauCeti.Multiquadratic.exists_finset_primeDiscriminant_ncard_ramifiedPrimes {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d) : ∃ (s : Finset ℤ), (∀ P ∈ s, IsPrimeDiscriminant P) ∧ ∏ P ∈ s, P = fundamentalDiscriminant d ∧ (NumberField.ramifiedPrimes K).ncard = s.card

The ramified primes of ℚ(√d), counted by a prime-discriminant factorization of the discriminant. Packages ncard_ramifiedPrimes_eq_card with the existence of the factorization, so a caller need only supply d squarefree together with a quadratic presentation of K.

Total ramification

A ramified prime of a quadratic field is totally ramified: it has a single prime above it, with ramification index 2. This is NumberField.map_span_eq_sq_of_mem_ramifiedPrimes, read here through the discriminant criterion above.

theorem TauCeti.Multiquadratic.ramificationIdx_eq_two_of_dvd_fundamentalDiscriminant {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {d : ℤ} {p : ℕ} {𝔭 : Ideal (NumberField.RingOfIntegers K)} [𝔭.IsPrime] [𝔭.LiesOver (Ideal.span {↑p})] (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d) (hp : Nat.Prime p) (hdvd : ↑p ∣ fundamentalDiscriminant d) : 𝔭.ramificationIdx ℤ = 2

A prime dividing the discriminant of ℚ(√d) is totally ramified. If the rational prime p divides fundamentalDiscriminant d and 𝔭 is a prime of 𝓞 K above p, then e(𝔭 ∣ p) = 2.

theorem TauCeti.Multiquadratic.map_span_eq_sq_of_dvd_fundamentalDiscriminant {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {d : ℤ} {p : ℕ} {𝔭 : Ideal (NumberField.RingOfIntegers K)} [𝔭.IsPrime] [𝔭.LiesOver (Ideal.span {↑p})] (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d) (hp : Nat.Prime p) (hdvd : ↑p ∣ fundamentalDiscriminant d) : Ideal.map (algebraMap ℤ (NumberField.RingOfIntegers K)) (Ideal.span {↑p}) = 𝔭 ^ 2

p 𝓞 K = 𝔭 ^ 2 at a prime dividing the discriminant of ℚ(√d).

theorem TauCeti.Multiquadratic.map_span_primeDiscriminantPrime_eq_sq {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {D : ℤ} (hD : IsPrimeDiscriminant D) (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C (primeDiscriminantRadicand D)) (hgen : ℚ[↑θ] = ⊤) {𝔮 : Ideal (NumberField.RingOfIntegers K)} [𝔮.IsPrime] [𝔮.LiesOver (Ideal.span {↑(primeDiscriminantPrime D)})] : Ideal.map (algebraMap ℤ (NumberField.RingOfIntegers K)) (Ideal.span {↑(primeDiscriminantPrime D)}) = 𝔮 ^ 2

The quadratic field of a prime discriminant is totally ramified at its one ramified prime. For a prime discriminant D and K = ℚ(√(primeDiscriminantRadicand D)), the prime primeDiscriminantPrime D generates the square of the unique prime of 𝓞 K above it. This is the local picture at the generators of the candidate genus field.