A ramified prime of a quadratic field is totally ramified

Let K be a number field of degree 2 over ℚ and let p be a rational prime that ramifies in K. This file proves the classical description of that ramification: there is exactly one prime 𝔭 of 𝓞 K above p, it has ramification index 2 and inertia degree 1, and

p 𝓞 K = 𝔭 ^ 2.

The argument is the fundamental identity ∑_{𝔭 ∣ p} e(𝔭) f(𝔭) = [K : ℚ] (Ideal.sum_ramification_inertia_eq_finrank) with the right-hand side equal to 2: every summand is at least 1, so a single summand with e ≥ 2 exhausts the sum, forcing e = 2, f = 1 and no further primes above p. Turning the resulting e = 2 into the ideal identity p 𝓞 K = 𝔭 ^ 2 is the Dedekind factorization Ideal.map_algebraMap_eq_finsetProd_pow, whose product runs over the single prime 𝔭.

This file covers every ramified prime of a quadratic field. The splitting law of TauCeti.NumberTheory.NumberField.Quadratic.Splitting covers the odd primes p ∤ d not dividing the radicand; the unramified prime 2 (that is, d ≡ 1 mod 4, where 2 is split or inert) is described by neither file and remains open. It is the ramified case that genus theory needs: the 2-rank formula for ℚ(√d) rests on comparing the ramification of p in ℚ(√d) with its ramification in the genus field, and e(𝔭 ∣ p) = 2 is what makes the genus field unramified over ℚ(√d) at p.

Main results

All of the following assume Module.finrank ℚ K = 2. They live in the namespace NumberField, except for the two TauCeti.NumberField results whose names are written out in full:

• primesOver_eq_singleton_of_mem_ramifiedPrimes and ncard_primesOver_eq_one_of_mem_ramifiedPrimes: a ramified prime has a unique prime above it.
• ramificationIdx_eq_two_of_mem_ramifiedPrimes and inertiaDeg_eq_one_of_mem_ramifiedPrimes: that prime has e = 2 and f = 1.
• absNorm_eq_of_mem_ramifiedPrimes: its absolute norm is p.
• TauCeti.NumberField.eq_of_absNorm_eq_of_mem_ramifiedPrimes: every ideal of absolute norm p is that unique prime.
• map_span_eq_sq_of_mem_ramifiedPrimes: p 𝓞 K = 𝔭 ^ 2.
• TauCeti.NumberField.eq_map_span_of_absNorm_eq_sq_of_mem_ramifiedPrimes: every ideal of absolute norm p ^ 2 is the ideal p 𝓞 K; hence TauCeti.NumberField.isPrincipal_of_absNorm_eq_sq_of_mem_ramifiedPrimes: it is principal.
• map_eq_self_of_mem_ramifiedPrimes: any ring automorphism of 𝓞 K fixes 𝔭.
• mem_ramifiedPrimes_iff_ramificationIdx_eq_two: conversely, e = 2 characterises the ramified primes among the rational primes.

theorem NumberField.primesOver_eq_singleton_of_mem_ramifiedPrimes {K : Type u_1} [Field K] [NumberField K] {p : ℕ} (hK : Module.finrank ℚ K = 2) (hmem : p ∈ ramifiedPrimes K) (𝔭 : Ideal (RingOfIntegers K)) [𝔭.IsPrime] [𝔭.LiesOver (Ideal.span {↑p})] : (Ideal.span {↑p}).primesOver (RingOfIntegers K) = {𝔭}

A ramified prime of a quadratic field has a unique prime above it. If p ramifies in a number field K of degree 2, the primes of 𝓞 K above p are the single prime 𝔭.

theorem NumberField.ncard_primesOver_eq_one_of_mem_ramifiedPrimes {K : Type u_1} [Field K] [NumberField K] {p : ℕ} (hK : Module.finrank ℚ K = 2) (hmem : p ∈ ramifiedPrimes K) : ((Ideal.span {↑p}).primesOver (RingOfIntegers K)).ncard = 1

A ramified prime of a quadratic field has exactly one prime above it. The count form of primesOver_eq_singleton_of_mem_ramifiedPrimes: in the notation of the fundamental identity, g = 1.

theorem NumberField.ramificationIdx_eq_two_of_mem_ramifiedPrimes {K : Type u_1} [Field K] [NumberField K] {p : ℕ} (hK : Module.finrank ℚ K = 2) (hmem : p ∈ ramifiedPrimes K) (𝔭 : Ideal (RingOfIntegers K)) [𝔭.IsPrime] [𝔭.LiesOver (Ideal.span {↑p})] : 𝔭.ramificationIdx ℤ = 2

A ramified prime of a quadratic field is totally ramified. The prime 𝔭 above a ramified rational prime p has ramification index e(𝔭 ∣ p) = 2.

theorem NumberField.inertiaDeg_eq_one_of_mem_ramifiedPrimes {K : Type u_1} [Field K] [NumberField K] {p : ℕ} (hK : Module.finrank ℚ K = 2) (hmem : p ∈ ramifiedPrimes K) (𝔭 : Ideal (RingOfIntegers K)) [𝔭.IsPrime] [𝔭.LiesOver (Ideal.span {↑p})] : 𝔭.inertiaDeg ℤ = 1

The residue field does not grow at a ramified prime of a quadratic field. The prime 𝔭 above a ramified rational prime p has inertia degree f(𝔭 ∣ p) = 1.

theorem NumberField.absNorm_eq_of_mem_ramifiedPrimes {K : Type u_1} [Field K] [NumberField K] {p : ℕ} (hK : Module.finrank ℚ K = 2) (hmem : p ∈ ramifiedPrimes K) (𝔭 : Ideal (RingOfIntegers K)) [𝔭.IsPrime] [𝔭.LiesOver (Ideal.span {↑p})] : Ideal.absNorm 𝔭 = p

The absolute norm of a ramified prime of a quadratic field is the rational prime below it. Since the residue degree is 1 (inertiaDeg_eq_one_of_mem_ramifiedPrimes), the residue field of 𝔭 is ℤ/p, so N(𝔭) = p.

theorem NumberField.map_span_eq_sq_of_mem_ramifiedPrimes {K : Type u_1} [Field K] [NumberField K] {p : ℕ} (hK : Module.finrank ℚ K = 2) (hmem : p ∈ ramifiedPrimes K) (𝔭 : Ideal (RingOfIntegers K)) [𝔭.IsPrime] [𝔭.LiesOver (Ideal.span {↑p})] : Ideal.map (algebraMap ℤ (RingOfIntegers K)) (Ideal.span {↑p}) = 𝔭 ^ 2

p 𝓞 K = 𝔭 ^ 2 at a ramified prime of a quadratic field. The ideal generated by a ramified rational prime p in the ring of integers of a quadratic field is the square of the unique prime above it.

theorem NumberField.map_eq_self_of_mem_ramifiedPrimes {K : Type u_1} [Field K] [NumberField K] {p : ℕ} (hK : Module.finrank ℚ K = 2) (hmem : p ∈ ramifiedPrimes K) (𝔭 : Ideal (RingOfIntegers K)) [𝔭.IsPrime] [𝔭.LiesOver (Ideal.span {↑p})] (σ : RingOfIntegers K ≃+* RingOfIntegers K) : Ideal.map σ 𝔭 = 𝔭

A ring automorphism fixes a ramified prime. In a degree-two number field, any ring automorphism σ of 𝓞 K fixes the unique prime 𝔭 above a ramified rational prime p: σ 𝔭 is again a prime of 𝓞 K lying over p, and a ramified prime has only one prime above it.

theorem NumberField.mem_ramifiedPrimes_iff_ramificationIdx_eq_two {K : Type u_1} [Field K] [NumberField K] {p : ℕ} (hK : Module.finrank ℚ K = 2) (hp : Nat.Prime p) (𝔭 : Ideal (RingOfIntegers K)) [𝔭.IsPrime] [𝔭.LiesOver (Ideal.span {↑p})] : p ∈ ramifiedPrimes K ↔ 𝔭.ramificationIdx ℤ = 2

Ramification index 2 characterises the ramified primes of a quadratic field. For a rational prime p and a prime 𝔭 of 𝓞 K above it, p ramifies in the quadratic field K iff e(𝔭 ∣ p) = 2.

theorem TauCeti.NumberField.ramificationIdxIn_eq_two_of_mem_ramifiedPrimes {K : Type u_1} [Field K] [NumberField K] {p : ℕ} (hK : Module.finrank ℚ K = 2) (hmem : p ∈ NumberField.ramifiedPrimes K) : (Ideal.span {↑p}).ramificationIdxIn (NumberField.RingOfIntegers K) = 2

A ramified prime of a quadratic field has ramification index 2, in the form ramificationIdxIn that names no prime above p: the quadratic field is Galois over ℚ, so the ramification index is the same at every prime above p.

theorem TauCeti.NumberField.eq_of_absNorm_eq_of_mem_ramifiedPrimes {K : Type u_1} [Field K] [NumberField K] {p : ℕ} (hK : Module.finrank ℚ K = 2) (hmem : p ∈ NumberField.ramifiedPrimes K) (𝔭 I : Ideal (NumberField.RingOfIntegers K)) [𝔭.IsPrime] [𝔭.LiesOver (Ideal.span {↑p})] (hI : Ideal.absNorm I = p) : I = 𝔭

An ideal of prime norm is the unique prime above a ramified rational prime. If p ramifies in a quadratic number field, every ideal of absolute norm p equals the caller's chosen prime 𝔭 above p.

theorem TauCeti.NumberField.eq_map_span_of_absNorm_eq_sq_of_mem_ramifiedPrimes {K : Type u_1} [Field K] [NumberField K] {p : ℕ} (hK : Module.finrank ℚ K = 2) (hmem : p ∈ NumberField.ramifiedPrimes K) (I : Ideal (NumberField.RingOfIntegers K)) (hI : Ideal.absNorm I = p ^ 2) : I = Ideal.map (algebraMap ℤ (NumberField.RingOfIntegers K)) (Ideal.span {↑p})

An ideal whose absolute norm is the square of a ramified rational prime is the ideal that prime generates. In a quadratic number field, such an ideal is the square of the unique prime 𝔭 above p, and 𝔭 ^ 2 = p 𝓞 K.

theorem TauCeti.NumberField.isPrincipal_of_absNorm_eq_sq_of_mem_ramifiedPrimes {K : Type u_1} [Field K] [NumberField K] {p : ℕ} (hK : Module.finrank ℚ K = 2) (hmem : p ∈ NumberField.ramifiedPrimes K) (I : Ideal (NumberField.RingOfIntegers K)) (hI : Ideal.absNorm I = p ^ 2) : Submodule.IsPrincipal I

An ideal whose absolute norm is the square of a ramified rational prime is principal. By eq_map_span_of_absNorm_eq_sq_of_mem_ramifiedPrimes it is the ideal p 𝓞 K, generated by p.