Discriminants of prime-discriminant composita

Let D i be distinct prime discriminants, at most one of which is even, and let root i be chosen square roots of their radicands in a number field. This file computes the absolute value of the discriminant of their compositum:

|disc ℚ(root i : i)| = ∏ i, |D i| ^ 2 ^ (n - 1).

The proof adjoins one root at a time. Distinct prime discriminants in the family are coprime, so Mathlib's discriminant formula for the compositum of linearly disjoint number fields applies at each step. This formula is the finite-place input to the genus-field construction: a rational prime belonging to one prime-discriminant factor cannot ramify in the compositum of all the other factors.

The discriminant formula for a compositum is NumberField.natAbs_discr_eq_natAbs_discr_pow_mul_natAbs_discr_pow from Mathlib. The prime-discriminant description of genus fields is classical; see D. A. Cox, Primes of the Form x² + ny², and F. Lemmermeyer, Reciprocity Laws.

Main result

• TauCeti.Multiquadratic.natAbs_discr_adjoin_range_primeDiscriminantRadicands: the absolute discriminant of a compositum of distinct prime-discriminant quadratic fields.

theorem TauCeti.Multiquadratic.natAbs_discr_adjoin_range_primeDiscriminantRadicands {ι : Type u} [Fintype ι] {L : Type v} [Field L] [NumberField L] (D : ι → ℤ) (hD : ∀ (i : ι), IsPrimeDiscriminant (D i)) (hinj : Function.Injective D) (heven : ∀ (i j : ι), IsEvenPrimeDiscriminant (D i) → IsEvenPrimeDiscriminant (D j) → D i = D j) (root : ι → L) (hroot : ∀ (i : ι), root i ^ 2 = (algebraMap ℚ L) ↑(primeDiscriminantRadicand (D i))) : (NumberField.discr ↥(IntermediateField.adjoin ℚ (Set.range root))).natAbs = ∏ i : ι, (D i).natAbs ^ 2 ^ (Fintype.card ι - 1)

Discriminant of a prime-discriminant compositum. Let D : ι → ℤ be an injective family of prime discriminants containing at most one even member, and let root i square to the radicand attached to D i. If n = |\u03b9|, then the compositum of these roots has absolute discriminant ∏ i, |D i| ^ 2 ^ (n - 1).

For the empty family both sides are one. For a singleton this recovers that the quadratic field attached to a prime discriminant D has discriminant D.