The squarefree radicand of a quadratic field

A quadratic number field K has a presentation K = ℚ(θ) with θ² = d for a squarefree integer d (NumberField.exists_minpoly_eq_X_sq_sub_C_and_adjoin_eq_top). This file shows that the radicand d is an isomorphism invariant: it classifies quadratic fields up to ℚ-algebra isomorphism, and the rational quadratic algebra QuadraticAlgebra ℚ d 0 is the corresponding model. For an imaginary quadratic field the radicand is negative (NumberField.exists_minpoly_eq_X_sq_sub_C_and_adjoin_eq_top_of_isTotallyComplex), so imaginary quadratic fields up to isomorphism are in bijection with the negative squarefree integers, and statements about imaginary quadratic fields up to isomorphism may be read off their radicands.

The comparison of models reuses the classification of the models themselves, QuadraticAlgebra.Rat.nonempty_algEquiv_iff: for squarefree integers d and e, ℚ(√d) ≃ₐ[ℚ] ℚ(√e) exactly when d = e. A presented field is identified with its model by TauCeti.QuadraticOrder.algEquivOfSqrt, evaluation at the chosen square root.

Main results

• NumberField.nonempty_algEquiv_quadraticAlgebra: a quadratic field presented by a square root of d is isomorphic to QuadraticAlgebra ℚ d 0.
• NumberField.nonempty_algEquiv_iff_of_squarefree: two quadratic fields presented by squarefree radicands d and e are isomorphic exactly when d = e.
• NumberField.eq_of_sq_eq_intCast_of_squarefree: the squarefree radicand is the only squarefree integer other than 1 with a square root in K.
• NumberField.existsUnique_squarefree_algEquiv: every quadratic field is isomorphic to QuadraticAlgebra ℚ d 0 for exactly one squarefree integer d.
• NumberField.existsUnique_neg_squarefree_algEquiv: every imaginary quadratic field is isomorphic to QuadraticAlgebra ℚ d 0 for exactly one negative squarefree integer d.

theorem NumberField.nonempty_algEquiv_quadraticAlgebra {K : Type u_1} [Field K] [NumberField K] {d : ℤ} (hK : Module.finrank ℚ K = 2) {θ : RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) : Nonempty (K ≃ₐ[ℚ] QuadraticAlgebra ℚ (↑d) 0)

A presented quadratic field is isomorphic to its model. If [K : ℚ] = 2 and θ ∈ 𝓞 K has minimal polynomial X² - d, then K ≃ₐ[ℚ] QuadraticAlgebra ℚ d 0. The isomorphism is the inverse of evaluation at θ, TauCeti.QuadraticOrder.algEquivOfSqrt; no generation hypothesis is needed, since an irrational element of a quadratic field generates it.

theorem NumberField.nonempty_algEquiv_iff_of_squarefree {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] {d e : ℤ} (hK : Module.finrank ℚ K = 2) (hL : Module.finrank ℚ L = 2) {θ : RingOfIntegers K} {η : RingOfIntegers L} (hθ : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hη : minpoly ℤ η = Polynomial.X ^ 2 - Polynomial.C e) (hd : Squarefree d) (he : Squarefree e) : Nonempty (K ≃ₐ[ℚ] L) ↔ d = e

The squarefree radicand is an isomorphism invariant. Two quadratic fields presented by square roots of squarefree integers d and e are ℚ-isomorphic exactly when d = e. Taking L = K and the identity shows that the squarefree radicand of a quadratic field does not depend on the presentation.

theorem NumberField.eq_of_sq_eq_intCast_of_squarefree {K : Type u_1} [Field K] [NumberField K] {d : ℤ} (hK : Module.finrank ℚ K = 2) {θ : RingOfIntegers K} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hd : Squarefree d) {z : K} {n : ℤ} (hz : z ^ 2 = ↑n) (hn : Squarefree n) (hn1 : n ≠ 1) : n = d

The radicand is the only squarefree square class in K. If K is presented by a square root of the squarefree integer d, and z ∈ K squares to a squarefree integer n ≠ 1, then n = d. Such a z is irrational, so it presents K with radicand n, and the radicand does not depend on the presentation.

theorem NumberField.existsUnique_squarefree_algEquiv {K : Type u_1} [Field K] [NumberField K] (hK : Module.finrank ℚ K = 2) : ∃! d : ℤ, Squarefree d ∧ Nonempty (K ≃ₐ[ℚ] QuadraticAlgebra ℚ (↑d) 0)

The squarefree model of a quadratic field. Every number field of degree 2 over ℚ is isomorphic to QuadraticAlgebra ℚ d 0 for exactly one squarefree integer d.

theorem NumberField.existsUnique_neg_squarefree_algEquiv {K : Type u_1} [Field K] [NumberField K] [IsTotallyComplex K] (hK : Module.finrank ℚ K = 2) : ∃! d : ℤ, d < 0 ∧ Squarefree d ∧ Nonempty (K ≃ₐ[ℚ] QuadraticAlgebra ℚ (↑d) 0)

The radicand classification of imaginary quadratic fields. Every totally complex number field of degree 2 over ℚ is isomorphic to QuadraticAlgebra ℚ d 0 for exactly one negative squarefree integer d.