Basics for quadratic number fields

Shared facts about a quadratic number field K presented by an algebraic integer θ : 𝓞 K whose minimal polynomial over ℤ is X² - d. These feed the prime-splitting law (Quadratic/Splitting.lean), the conjugation automorphism (Quadratic/Conjugation/Basic.lean), the ring-of-integers/discriminant computation (Quadratic/RingOfIntegers.lean), and the field-norm computation (Quadratic/Norm.lean).

Main results

• NumberField.minpoly_rat_quadratic: the minimal polynomial of θ over ℚ is X² - d.
• NumberField.finrank_rat_eq_two: K has degree 2 over ℚ.
• NumberField.finrank_rat_eq_two_of_minpoly_eq_X_sq_sub_X_add: the same for a field generated by a root of a monic quadratic X² - X + c, the half-integer presentation.
• NumberField.gen_sq: the integral generator squares to the radicand in 𝓞 K.
• TauCeti.NumberField.smul_gen_eq_or_eq_neg: every ℚ-automorphism sends θ to ±θ.
• NumberField.coe_gen_sq: the generator squares to the radicand, θ² = d in K.
• NumberField.coe_gen_sq_ratCast: the same over ℚ, θ² = (d : ℚ) in K.
• NumberField.gen_notMem_range: the generator is not rational, θ ∉ ℚ.
• NumberField.coe_gen_ne_zero: the generator is nonzero.
• NumberField.exists_eq_add_mul_gen: every element of K is b + aθ.
• NumberField.not_isSquare_radicand: the radicand is not a rational square.
• NumberField.exists_gen_of_sq_eq_intCast: an irrational square root of an integer presents a quadratic field.
• NumberField.exists_minpoly_eq_X_sq_sub_C_and_adjoin_eq_top: every number field of degree 2 over ℚ has such a presentation, with squarefree radicand.
• NumberField.trace_gen_eq_zero: the trace of the generator is 0.
• NumberField.discr_one_gen: the discriminant of {1, θ} over ℚ is 4d.
• NumberField.discr_one_halfGen: the discriminant of {1, (1+θ)/2} over ℚ is d.

The trace and discriminant computations reuse the generic quadratic-extension API NumberField.trace_eq_zero_of_sq_ratCast and TauCeti.Algebra.discr_one_elem_eq_of_sq_algebraMap from TauCeti.FieldTheory.Trace.

theorem NumberField.minpoly_rat_quadratic {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) : minpoly ℚ ↑θ = Polynomial.X ^ 2 - Polynomial.C ↑d

The minimal polynomial of θ over ℚ is X² - d, obtained from its minimal polynomial over ℤ by base change along ℤ → ℚ.

theorem NumberField.finrank_rat_eq_two {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) : Module.finrank ℚ K = 2

The quadratic field K = ℚ(θ) has degree 2 over ℚ: its power basis has dimension natDegree (X² - d) = 2.

theorem NumberField.finrank_rat_eq_two_of_minpoly_eq_X_sq_sub_X_add {K : Type u_1} [Field K] [NumberField K] {ω : RingOfIntegers K} {c : ℤ} (hmin : minpoly ℤ ω = Polynomial.X ^ 2 - Polynomial.X + Polynomial.C c) (hgen : ℚ[↑ω] = ⊤) : Module.finrank ℚ K = 2

The field generated over ℚ by an algebraic integer ω with minimal polynomial X² - X + c over ℤ — the half-integer presentation of a quadratic field — has degree 2 over ℚ.

@[simp]

theorem NumberField.gen_sq {K : Type u_1} [Field K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) : θ ^ 2 = (algebraMap ℤ (RingOfIntegers K)) d

The integral generator squares to the radicand: θ² = d in 𝓞 K.

@[simp]

theorem NumberField.coe_gen_sq {K : Type u_1} [Field K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) : ↑θ ^ 2 = (algebraMap ℤ K) d

The generator squares to the radicand in K: θ² = d.

theorem NumberField.coe_gen_sq_ratCast {K : Type u_1} [Field K] {θ : RingOfIntegers K} {d : ℤ} [CharZero K] (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) : ↑θ ^ 2 = (algebraMap ℚ K) ↑d

The generator squares to the radicand viewed over ℚ: θ² = (d : ℚ) in K. This is coe_gen_sq transported along ℤ → ℚ → K, the form fed to the generic square-root-basis API.

theorem NumberField.gen_notMem_range {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) : ↑θ ∉ (algebraMap ℚ K).range

The generator is irrational: θ ∉ ℚ.

theorem NumberField.coe_gen_ne_zero {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) : ↑θ ≠ 0

The generator of a quadratic presentation is nonzero: it is irrational (gen_notMem_range), whereas 0 is rational.

theorem NumberField.exists_eq_add_mul_gen {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) (x : K) : ∃ (a : ℚ) (b : ℚ), x = (algebraMap ℚ K) b + (algebraMap ℚ K) a * ↑θ

Every element of a quadratic field is b + aθ for rationals a, b.

theorem NumberField.not_isSquare_radicand {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) : ¬IsSquare ↑d

The radicand of a quadratic presentation is not a rational square. Were d = q², the factorization (θ - q)(θ + q) = θ² - d = 0 would force θ = ±q ∈ ℚ.

theorem NumberField.exists_gen_of_sq_eq_intCast {K : Type u_1} [Field K] [NumberField K] [Algebra.IsQuadraticExtension ℚ K] {z : K} {n : ℤ} (hz2 : z ^ 2 = ↑n) (hzQ : z ∉ Set.range ⇑(algebraMap ℚ K)) : ∃ (θ : RingOfIntegers K), minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C n ∧ ℚ[↑θ] = ⊤

An irrational square root of an integer presents a quadratic field: if z : K is irrational and z² = n for an integer n, then z is an algebraic integer with minimal polynomial X² - n generating K over ℚ.

theorem NumberField.exists_minpoly_eq_X_sq_sub_C_and_adjoin_eq_top {K : Type u_1} [Field K] [NumberField K] (hK : Module.finrank ℚ K = 2) : ∃ (θ : RingOfIntegers K) (d : ℤ), minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d ∧ ℚ[↑θ] = ⊤ ∧ Squarefree d

Every quadratic number field has a quadratic presentation with squarefree radicand. If [K : ℚ] = 2 there is an algebraic integer θ : 𝓞 K generating K over ℚ whose minimal polynomial over ℤ is X² - d for a squarefree integer d. So any statement proved under the hypotheses minpoly ℤ θ = X ^ 2 - C d, Algebra.adjoin ℚ {(θ : K)} = ⊤ and Squarefree d whose conclusion does not mention θ or d holds for every quadratic field.

Take any irrational x ∈ K and write x² = b + ax; completing the square, y = 2x - a squares to the rational e = a² + 4b, which is nonzero because y is irrational. Representing the square class of e by a squarefree integer, e = d · c² with c : ℚ nonzero (Rat.exists_squarefree_int_mul_sq), the irrational y / c squares to d.

theorem NumberField.trace_gen_eq_zero {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) : (Algebra.trace ℚ K) ↑θ = 0

The trace of the generator vanishes: Tr(θ) = 0.

theorem NumberField.discr_one_gen {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) : Algebra.discr ℚ ![1, ↑θ] = ↑(4 * d)

The discriminant of the ℚ-family {1, θ} is 4d.

theorem NumberField.discr_one_halfGen {K : Type u_1} [Field K] [NumberField K] {θ : RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (hgen : ℚ[↑θ] = ⊤) : Algebra.discr ℚ ![1, (1 + ↑θ) / 2] = ↑d

The discriminant of the ℚ-family {1, (1+θ)/2} is d.

theorem TauCeti.NumberField.smul_gen_eq_or_eq_neg {K : Type u_1} [Field K] [NumberField K] {θ : NumberField.RingOfIntegers K} {d : ℤ} (hmin : minpoly ℤ θ = Polynomial.X ^ 2 - Polynomial.C d) (σ : Gal(K/ℚ)) : σ • θ = θ ∨ σ • θ = -θ

Every ℚ-automorphism of K sends θ to θ or to -θ, the two square roots of the radicand d.