The discriminant of a quadratic field is its fundamental discriminant

For a quadratic number field K = ℚ(√d) — presented by an algebraic integer θ : 𝓞 K with minpoly ℤ θ = X² - d and Algebra.adjoin ℚ {θ} = ⊤ — with d squarefree, the field discriminant equals the fundamental discriminant of d:

NumberField.discr K = fundamentalDiscriminant d (= d for d ≡ 1 mod 4, else 4d).

This ties the ring-of-integers discriminant computations (NumberField.discr_eq_four_mul_of_mod_four_ne_one and NumberField.discr_eq_of_squarefree_of_mod_four_eq_one) to the integer-level TauCeti.Multiquadratic.fundamentalDiscriminant.

The same rewriting turns the two shapes of the quadratic norm form into the single statement A² - D * B² = 4 * N(z) with D = fundamentalDiscriminant d, which is the form genus theory consumes.

Main results

• TauCeti.Multiquadratic.discr_eq_fundamentalDiscriminant.
• TauCeti.Multiquadratic.discr_adjoin_singleton_eq_fundamentalDiscriminant: the same formula for the intermediate field generated by a square root in a characteristic-zero ambient field.
• TauCeti.Multiquadratic.exists_sq_sub_fundamentalDiscriminant_mul_sq_eq_four_mul_norm: the norm form of a quadratic field, written with its fundamental discriminant.

theorem TauCeti.Multiquadratic.discr_eq_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) : NumberField.discr K = fundamentalDiscriminant d

The discriminant of a quadratic field ℚ(√d) (squarefree d) is the fundamental discriminant of d.

theorem TauCeti.Multiquadratic.exists_sq_sub_fundamentalDiscriminant_mul_sq_eq_four_mul_norm {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (hsf : Squarefree d) (z : NumberField.RingOfIntegers K) : ∃ (A : ℤ) (B : ℤ), A ^ 2 - fundamentalDiscriminant d * B ^ 2 = 4 * (Algebra.norm ℤ) z

The norm form of a quadratic field, written with its fundamental discriminant. For a quadratic field K = ℚ(√d) with d squarefree, every algebraic integer z of K satisfies A² - D * B² = 4 * N(z) for some integers A, B, where D = fundamentalDiscriminant d. This is NumberField.exists_sq_sub_mul_sq_eq_four_mul_norm when d ≡ 1 (mod 4), and rescales NumberField.exists_sq_sub_mul_sq_eq_norm_of_mod_four_ne_one by 2 otherwise.

theorem TauCeti.Multiquadratic.discr_adjoin_singleton_eq_fundamentalDiscriminant {L : Type u_2} [Field L] [CharZero L] {d : ℤ} (hsf : Squarefree d) {x : L} (hx : x ^ 2 = (algebraMap ℤ L) d) (hnsq : ¬IsSquare ↑d) : have hxint := ⋯; NumberField.discr ↥ℚ⟮x⟯ = fundamentalDiscriminant d

Discriminant of a quadratic intermediate field. If x is a square root of a squarefree integer d which is not a rational square, then the intermediate field ℚ(x) has discriminant fundamentalDiscriminant d.

The ambient field need only have characteristic zero: x is automatically integral, so the statement supplies the resulting NumberField instance on ℚ(x) and the caller need not assume one on L.