The AdjoinRoot (X² - 3) model of ℚ(√3)

The concrete number field AdjoinRoot (X² - 3) serving as the canonical model of the real quadratic field ℚ(√3), together with its integral generator. This presentation datum is shared by the class-number and 2-rank computations for this field, so it lives here rather than in either of them.

Unlike the imaginary quadratic models, where X² - d with d < 0 has no rational root for sign reasons, irreducibility here is the irrationality of √3: a rational square root of 3 would make 3 a square in ℤ (Rat.isSquare_intCast_iff), contradicting its primality.

Main results

• TauCeti.NumberField.not_isSquare_three_rat: 3 is not a square in ℚ.
• TauCeti.NumberField.exists_minpoly_eq_X_sq_sub_three_and_adjoin_eq_top: the model has an integral generator with minimal polynomial X² - 3 generating the field over ℚ.

theorem TauCeti.NumberField.not_isSquare_three_rat : ¬IsSquare ↑3

3 is not a square in ℚ, the arithmetic input that makes ℚ(√3) a quadratic field: a rational square root of 3 would make 3 a square in ℤ (Rat.isSquare_intCast_iff), contradicting its primality.

instance TauCeti.NumberField.irreducible_X_sq_sub_three : Fact (Irreducible (Polynomial.X ^ 2 - Polynomial.C 3))

X² - 3 is irreducible over ℚ, so AdjoinRoot (X² - 3) is a field.

theorem TauCeti.NumberField.exists_minpoly_eq_X_sq_sub_three_and_adjoin_eq_top : ∃ (θ : NumberField.RingOfIntegers (AdjoinRoot (Polynomial.X ^ 2 - Polynomial.C 3))), minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C 3 ∧ ℚ[↑θ] = ⊤

The concrete model AdjoinRoot (X² - 3) of ℚ(√3) carries an integral generator with minimal polynomial X² - 3 generating the field over ℚ: the presentation data shared by the class-number and 2-rank computations for this field.