The quadratic base of the candidate genus field, as a quadratic field

For a squarefree integer d, candidateGenusFieldBase hd is the copy of ℚ(√d) cut out inside candidateGenusField hd by the chosen square root candidateGenusFieldBaseRoot hd of d. The quadratic-field API of TauCeti.NumberTheory.NumberField.Quadratic and of Multiquadratic/Quadratic/* — the ring of integers, the discriminant, the ramified primes, the conjugation — is phrased for a number field K presented by an algebraic integer θ : 𝓞 K with

minpoly ℤ θ = X ^ 2 - d and Algebra.adjoin ℚ {(θ : K)} = ⊤.

This file supplies that presentation for the embedded base, so those results become available for it. The generator is candidateGenusFieldBaseGen, the chosen root packaged as an algebraic integer; its minimal polynomial is X ^ 2 - d as soon as d is not a rational square (NumberField.minpoly_integralSqrt), and it generates the base over ℚ because the base is by definition the simple extension it generates.

Main definitions

• TauCeti.Multiquadratic.candidateGenusFieldBaseSqrt: the chosen square root of d, viewed as an element of the embedded base rather than of the whole candidate genus field.
• TauCeti.Multiquadratic.candidateGenusFieldBaseGen: the same element as an algebraic integer.

Main results

• TauCeti.Multiquadratic.minpoly_candidateGenusFieldBaseGen: its minimal polynomial over ℤ is X ^ 2 - d, for d not a rational square.
• TauCeti.Multiquadratic.adjoin_candidateGenusFieldBaseSqrt_eq_top: the chosen root generates the base as an intermediate field.
• TauCeti.Multiquadratic.adjoin_candidateGenusFieldBaseGen_eq_top: it generates the base over ℚ.

noncomputable def TauCeti.Multiquadratic.candidateGenusFieldBaseSqrt {d : ℤ} (hd : Squarefree d) : ↥(candidateGenusFieldBase hd)

The chosen square root of d, viewed inside the embedded base ℚ(√d) of the candidate genus field rather than inside the candidate genus field itself.

@[simp]

theorem TauCeti.Multiquadratic.candidateGenusFieldBaseSqrt_val {d : ℤ} (hd : Squarefree d) : ↑(candidateGenusFieldBaseSqrt hd) = candidateGenusFieldBaseRoot hd

@[simp]

theorem TauCeti.Multiquadratic.candidateGenusFieldBaseSqrt_sq {d : ℤ} (hd : Squarefree d) : candidateGenusFieldBaseSqrt hd ^ 2 = (algebraMap ℤ ↥(candidateGenusFieldBase hd)) d

noncomputable def TauCeti.Multiquadratic.candidateGenusFieldBaseGen {d : ℤ} (hd : Squarefree d) : NumberField.RingOfIntegers ↥(candidateGenusFieldBase hd)

The chosen square root of d, as an algebraic integer of the embedded base. This is the θ of the quadratic-field presentation minpoly ℤ θ = X ^ 2 - d, Algebra.adjoin ℚ {θ} = ⊤.

@[simp]

theorem TauCeti.Multiquadratic.coe_candidateGenusFieldBaseGen {d : ℤ} (hd : Squarefree d) : ↑(candidateGenusFieldBaseGen hd) = candidateGenusFieldBaseSqrt hd

theorem TauCeti.Multiquadratic.minpoly_candidateGenusFieldBaseGen {d : ℤ} (hd : Squarefree d) (hnsq : ¬IsSquare ↑d) : minpoly ℤ (candidateGenusFieldBaseGen hd) = Polynomial.X ^ 2 - Polynomial.C d

The minimal polynomial of the base generator is X ^ 2 - d, for d not a rational square. Together with adjoin_candidateGenusFieldBaseGen_eq_top this presents candidateGenusFieldBase hd as the quadratic field ℚ(√d) in the form the quadratic-field API expects.

theorem TauCeti.Multiquadratic.adjoin_candidateGenusFieldBaseSqrt_eq_top {d : ℤ} (hd : Squarefree d) : ℚ⟮candidateGenusFieldBaseSqrt hd⟯ = ⊤

The chosen square root of d generates the embedded base as an intermediate field: the base is by definition the simple extension it generates, read one level down.

theorem TauCeti.Multiquadratic.adjoin_candidateGenusFieldBaseGen_eq_top {d : ℤ} (hd : Squarefree d) : ℚ[↑(candidateGenusFieldBaseGen hd)] = ⊤

The base generator generates the base over ℚ. The embedded base is by definition the simple extension generated by the chosen square root of d; being integral, that root generates the base already as a ℚ-algebra.