Quadratic fields attached to prime discriminants

A prime discriminant D determines the quadratic field generated by a square root of primeDiscriminantRadicand D. This file identifies the number-field discriminant of that field with D itself.

The main theorem is stated first for an arbitrary presentation of the quadratic field, and then for the intermediate field generated by a root. The latter is the form needed to compute the discriminant of the prime-discriminant compositum: Mathlib's NumberField.natAbs_discr_eq_natAbs_discr_pow_mul_natAbs_discr_pow combines linearly disjoint number fields whose mapped different ideals are coprime. Coprime field discriminants establish that hypothesis via NumberField.isCoprime_differentIdeal_of_isCoprime_discr; iterating the formula over the prime-discriminant factors of a quadratic discriminant is the finite-place input to the genus-field construction.

The identification of prime discriminants with quadratic-field discriminants is classical; see D. A. Cox, Primes of the Form x² + ny², and F. Lemmermeyer, Reciprocity Laws.

Main results

• TauCeti.Multiquadratic.discr_eq_primeDiscriminant_of_sq: a number field generated by a square root of the radicand of D has discriminant D.
• TauCeti.Multiquadratic.discr_adjoin_singleton_eq_primeDiscriminant: the same result for the intermediate field generated by the root.
• TauCeti.Multiquadratic.isCoprime_discr_adjoin_singleton_of_primeDiscriminant: distinct prime-discriminant quadratic fields have coprime discriminants when at most one is even.

theorem TauCeti.Multiquadratic.discr_eq_primeDiscriminant_of_sq {K : Type u_1} [Field K] [NumberField K] {D : ℤ} (hD : IsPrimeDiscriminant D) {x : K} (hx : x ^ 2 = (algebraMap ℤ K) (primeDiscriminantRadicand D)) (hgen : ℚ[x] = ⊤) : NumberField.discr K = D

A number field generated by a square root of the radicand of a prime discriminant D has field discriminant D.

The root need not be supplied as an algebraic integer: its square is an integer, so integrality is automatic.

theorem TauCeti.Multiquadratic.discr_adjoin_singleton_eq_primeDiscriminant {L : Type u_1} [Field L] [CharZero L] {D : ℤ} (hD : IsPrimeDiscriminant D) {x : L} (hx : x ^ 2 = (algebraMap ℤ L) (primeDiscriminantRadicand D)) : have hxint := ⋯; NumberField.discr ↥ℚ⟮x⟯ = D

The quadratic intermediate field generated by a square root of the radicand of a prime discriminant D has field discriminant D. This is the form used when adjoining the prime-discriminant roots one at a time in their compositum.

theorem TauCeti.Multiquadratic.isCoprime_discr_adjoin_singleton_of_primeDiscriminant {L : Type u_1} [Field L] [CharZero L] {D E : ℤ} (hD : IsPrimeDiscriminant D) (hE : IsPrimeDiscriminant E) (hne : D ≠ E) (heven : ¬(IsEvenPrimeDiscriminant D ∧ IsEvenPrimeDiscriminant E)) {x y : L} (hx : x ^ 2 = (algebraMap ℤ L) (primeDiscriminantRadicand D)) (hy : y ^ 2 = (algebraMap ℤ L) (primeDiscriminantRadicand E)) : have hxint := ⋯; have hyint := ⋯; IsCoprime (NumberField.discr ↥ℚ⟮x⟯) (NumberField.discr ↥ℚ⟮y⟯)

Quadratic fields attached to distinct prime discriminants have coprime field discriminants, provided the two discriminants are not both even. The prime-discriminant factorization of a quadratic discriminant has exactly this property, so this is the coprimality input to Mathlib's discriminant formula for a compositum.