Ramification in a compositum of prime-discriminant quadratic fields

Let D i be prime discriminants and let root i be chosen square roots of their radicands inside a number field. This file describes the ramification of the rational primes in their compositum M = ℚ(root i : i). The support result allows repeated factors and multiple even factors; the ramification-index results additionally assume distinct factors with at most one even factor.

Two facts are proved. Together they are the ramified-prime half of the multiquadratic splitting law, complementary to the quadratic-residue description in TauCeti/NumberTheory/Multiquadratic/Prime/Discriminant/Splitting.lean, which is stated for the primes dividing none of the D i.

• A rational prime ramifies in M if and only if it is the prime primeDiscriminantPrime (D i) belonging to one of the factors. This follows by specializing the general ramification theorem for multiquadratic fields and identifying the fundamental discriminant of each radicand with D i.
• At such a prime the ramification index is exactly 2, however large the compositum is: the inertia at a ramified prime of a prime-discriminant compositum is as small as it can be. The upper bound is a transverse cancellation — the compositum of all the other roots is unramified at primeDiscriminantPrime (D i) and has M as a quadratic extension — and the lower bound comes from the quadratic subfield ℚ(root i), where the prime is totally ramified.

The payoff is a criterion for relative unramifiedness, which is the shape the genus-field construction needs: if F is a subfield of M in which every primeDiscriminantPrime (D i) already has ramification index 2, then M is unramified over F at every finite place. The genus field of ℚ(√d) is the case F = ℚ(√d), whose ramified primes are precisely the primes of the prime-discriminant factorization of its discriminant.

The prime-discriminant construction of the genus field is classical; see D. A. Cox, Primes of the Form x² + ny², §6.A, and F. Lemmermeyer, Reciprocity Laws: from Euler to Eisenstein, §2.2.

Main results

• TauCeti.Multiquadratic.mem_ramifiedPrimes_iff_exists_eq_primeDiscriminantPrime: the ramified primes of a number field generated by the roots are the primes belonging to the factors.
• TauCeti.Multiquadratic.isUnramifiedIn_of_forall_ne_primeDiscriminantPrime and TauCeti.Multiquadratic.isUnramifiedIn_adjoin_range_ne_primeDiscriminantPrime: the two unramifiedness statements those give, for a prime outside the family and for the prime of an omitted factor in the compositum of the remaining ones.
• TauCeti.Multiquadratic.ramificationIdx_eq_two_of_liesOver_primeDiscriminantPrime: the ramification index at a ramified prime is 2.
• TauCeti.Multiquadratic.isUnramifiedIn_of_forall_ramificationIdx_eq_two: the relative unramifiedness criterion at a prime of a subfield that already carries the ramification.

theorem TauCeti.Multiquadratic.mem_ramifiedPrimes_iff_exists_eq_primeDiscriminantPrime {ι : Type u} {L : Type v} [Field L] [NumberField L] (D : ι → ℤ) (hD : ∀ (i : ι), IsPrimeDiscriminant (D i)) (root : ι → L) (hroot : ∀ (i : ι), root i ^ 2 = (algebraMap ℚ L) ↑(primeDiscriminantRadicand (D i))) (htop : IntermediateField.adjoin ℚ (Set.range root) = ⊤) {p : ℕ} (hp : Nat.Prime p) : p ∈ NumberField.ramifiedPrimes L ↔ ∃ (i : ι), p = primeDiscriminantPrime (D i)

The ramified primes of a field generated by prime-discriminant roots. Let D : ι → ℤ be any family of prime discriminants and let root i square to the radicand of D i. If the roots generate a number field L, a rational prime ramifies in L exactly when it is the prime primeDiscriminantPrime (D i) belonging to one of the factors. Repeated factors and multiple even prime discriminants are allowed: neither changes the support of ramification.

theorem TauCeti.Multiquadratic.isUnramifiedIn_of_forall_ne_primeDiscriminantPrime {ι : Type u} {L : Type v} [Field L] [NumberField L] (D : ι → ℤ) (root : ι → L) (hD : ∀ (i : ι), IsPrimeDiscriminant (D i)) (hroot : ∀ (i : ι), root i ^ 2 = (algebraMap ℚ L) ↑(primeDiscriminantRadicand (D i))) (htop : IntermediateField.adjoin ℚ (Set.range root) = ⊤) {p : ℕ} (hp : Nat.Prime p) (hne : ∀ (i : ι), p ≠ primeDiscriminantPrime (D i)) : Algebra.IsUnramifiedIn (NumberField.RingOfIntegers L) (Ideal.span {↑p})

A prime outside the family is unramified. If a rational prime is not the prime belonging to any of the prime-discriminant factors, it is unramified in the field they generate.

theorem TauCeti.Multiquadratic.isUnramifiedIn_adjoin_range_ne_primeDiscriminantPrime {ι : Type u} {L : Type v} [Field L] [NumberField L] (D : ι → ℤ) (root : ι → L) (hD : ∀ (i : ι), IsPrimeDiscriminant (D i)) (hinj : Function.Injective D) (heven : ∀ (i j : ι), IsEvenPrimeDiscriminant (D i) → IsEvenPrimeDiscriminant (D j) → D i = D j) (hroot : ∀ (i : ι), root i ^ 2 = (algebraMap ℚ L) ↑(primeDiscriminantRadicand (D i))) (i : ι) : Algebra.IsUnramifiedIn (NumberField.RingOfIntegers ↥(IntermediateField.adjoin ℚ (Set.range fun (j : { j : ι // j ≠ i }) => root ↑j))) (Ideal.span {↑(primeDiscriminantPrime (D i))})

The transverse subcompositum is unramified at the omitted prime. The prime belonging to the factor D i is unramified in the compositum of the roots attached to all the other factors, because that compositum's ramified primes belong to those other factors, and the prime of a factor determines it.

theorem TauCeti.Multiquadratic.ramificationIdx_eq_two_of_liesOver_primeDiscriminantPrime {ι : Type u} [Finite ι] {L : Type v} [Field L] [NumberField L] (D : ι → ℤ) (root : ι → L) (hD : ∀ (i : ι), IsPrimeDiscriminant (D i)) (hinj : Function.Injective D) (heven : ∀ (i j : ι), IsEvenPrimeDiscriminant (D i) → IsEvenPrimeDiscriminant (D j) → D i = D j) (hroot : ∀ (i : ι), root i ^ 2 = (algebraMap ℚ L) ↑(primeDiscriminantRadicand (D i))) (htop : IntermediateField.adjoin ℚ (Set.range root) = ⊤) (i : ι) (𝔓 : Ideal (NumberField.RingOfIntegers L)) [𝔓.IsPrime] [𝔓.LiesOver (Ideal.span {↑(primeDiscriminantPrime (D i))})] : 𝔓.ramificationIdx ℤ = 2

The ramification index at a ramified prime of a prime-discriminant compositum is 2. However many factors the compositum has, a prime belonging to one of them has ramification index exactly two: the inertia subgroup at a ramified prime is as small as it can be.

The upper bound is transverse cancellation. The compositum U of the other roots is unramified at the prime (isUnramifiedIn_adjoin_range_ne_primeDiscriminantPrime), so the absolute ramification index equals the relative one over U, which is at most [L : U] = 2. The lower bound is the total ramification of the quadratic subfield ℚ(root i).

theorem TauCeti.Multiquadratic.isUnramifiedIn_of_forall_ramificationIdx_eq_two {ι : Type u} [Finite ι] {L : Type v} [Field L] [NumberField L] (D : ι → ℤ) (root : ι → L) (hD : ∀ (i : ι), IsPrimeDiscriminant (D i)) (hinj : Function.Injective D) (heven : ∀ (i j : ι), IsEvenPrimeDiscriminant (D i) → IsEvenPrimeDiscriminant (D j) → D i = D j) (hroot : ∀ (i : ι), root i ^ 2 = (algebraMap ℚ L) ↑(primeDiscriminantRadicand (D i))) (htop : IntermediateField.adjoin ℚ (Set.range root) = ⊤) (F : IntermediateField ℚ L) (𝔮 : Ideal (NumberField.RingOfIntegers ↥F)) [𝔮.IsPrime] (hF : ∀ (i : ι), 𝔮.LiesOver (Ideal.span {↑(primeDiscriminantPrime (D i))}) → 𝔮.ramificationIdx ℤ = 2) : Algebra.IsUnramifiedIn (NumberField.RingOfIntegers L) 𝔮

Unramifiedness over a subfield carrying the ramification. Let F be a subfield of the prime-discriminant compositum L and let 𝔮 be a prime of 𝓞 F whose ramification index over ℤ is already 2 whenever it lies over one of the primes primeDiscriminantPrime (D i). Then 𝔮 is unramified in 𝓞 L.

Indeed, a prime of 𝓞 L above 𝔮 has absolute ramification index 2 as well, by ramificationIdx_eq_two_of_liesOver_primeDiscriminantPrime, so nothing is left to ramify in the tower; and if 𝔮 lies over none of those primes, the rational prime below it is already unramified in L.

This is the finite-place half of the genus-field property. For the genus field of ℚ(√d) the subfield F is the embedded copy of ℚ(√d), whose ramified primes are exactly the primes of the prime-discriminant factorization of its discriminant, each with ramification index 2.