Canonical orders in a supplied quadratic number field

A square root of a nonsquare integer D in a number field of rational degree two identifies the field with the rational quadratic algebra of D. Evaluation transports the canonical integral order to the subalgebra generated by (D + √D)/2 in that field.

The construction returns an actual GlobalNumberFields.NumberFieldOrder. Its integral basis has vectors 1 and (D + √D)/2, its discriminant is D, and it is maximal exactly when D is fundamental.

References

• D. A. Cox, Primes of the Form x² + ny², §7.

noncomputable def TauCeti.QuadraticOrder.algEquivOfSqrt {K : Type u_1} [Field K] [NumberField K] (D : ℤ) [Fact ¬IsSquare D] (δ : K) (hδ : δ ^ 2 = ↑D) (hK : Module.finrank ℚ K = 2) : QuadraticAlgebra ℚ (↑D) 0 ≃ₐ[ℚ] K

Evaluation at a square root identifies the rational model with the given quadratic field.

@[simp]

theorem TauCeti.QuadraticOrder.algEquivOfSqrt_apply {K : Type u_1} [Field K] [NumberField K] (D : ℤ) [Fact ¬IsSquare D] (δ : K) (hδ : δ ^ 2 = ↑D) (hK : Module.finrank ℚ K = 2) (z : QuadraticAlgebra ℚ (↑D) 0) : (algEquivOfSqrt D δ hδ hK) z = z.re • 1 + z.im • δ

The field identification is evaluation at the chosen square root.

noncomputable def TauCeti.QuadraticOrder.numberFieldOrderOfSqrt {K : Type u_1} [Field K] [NumberField K] (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) [Fact ¬IsSquare D] (δ : K) (hδ : δ ^ 2 = ↑D) (hK : Module.finrank ℚ K = 2) : GlobalNumberFields.NumberFieldOrder K

The same canonical order, embedded in a supplied quadratic number field.

@[simp]

theorem TauCeti.QuadraticOrder.numberFieldOrderOfSqrt_toSubalgebra {K : Type u_1} [Field K] [NumberField K] (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) [Fact ¬IsSquare D] (δ : K) (hδ : δ ^ 2 = ↑D) (hK : Module.finrank ℚ K = 2) : (numberFieldOrderOfSqrt D hD δ hδ hK).toSubalgebra = Subalgebra.map (AlgHom.restrictScalars ℤ ↑(algEquivOfSqrt D δ hδ hK)) (toSubalgebra D hD)

The field order's carrier is the image of the canonical integral order.

noncomputable def TauCeti.QuadraticOrder.equivNumberFieldOrderOfSqrt {K : Type u_1} [Field K] [NumberField K] (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) [Fact ¬IsSquare D] (δ : K) (hδ : δ ^ 2 = ↑D) (hK : Module.finrank ℚ K = 2) : ↥(toSubalgebra D hD) ≃ₐ[ℤ] ↥(numberFieldOrderOfSqrt D hD δ hδ hK).toSubalgebra

Evaluation identifies the integral canonical order with its image in the supplied field.

noncomputable def TauCeti.QuadraticOrder.basisOfSqrt {K : Type u_1} [Field K] [NumberField K] (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) [Fact ¬IsSquare D] (δ : K) (hδ : δ ^ 2 = ↑D) (hK : Module.finrank ℚ K = 2) : Module.Basis (Fin 2) ℤ ↥(numberFieldOrderOfSqrt D hD δ hδ hK).toSubalgebra

The integral basis after embedding in the chosen quadratic number field.

theorem TauCeti.QuadraticOrder.discr_basisOfSqrt {K : Type u_1} [Field K] [NumberField K] (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) [Fact ¬IsSquare D] (δ : K) (hδ : δ ^ 2 = ↑D) (hK : Module.finrank ℚ K = 2) : Algebra.discr ℤ ⇑(basisOfSqrt D hD δ hδ hK) = D

Embedding preserves the discriminant of the canonical basis.

@[simp]

theorem TauCeti.QuadraticOrder.numberFieldOrderOfSqrt_discr {K : Type u_1} [Field K] [NumberField K] (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) [Fact ¬IsSquare D] (δ : K) (hδ : δ ^ 2 = ↑D) (hK : Module.finrank ℚ K = 2) : (numberFieldOrderOfSqrt D hD δ hδ hK).discr = D

The embedded canonical order has the original integral discriminant.

@[simp]

theorem TauCeti.QuadraticOrder.numberFieldOrderOfSqrt_eq_maximal_iff {K : Type u_1} [Field K] [NumberField K] (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) [Fact ¬IsSquare D] (δ : K) (hδ : δ ^ 2 = ↑D) (hK : Module.finrank ℚ K = 2) : numberFieldOrderOfSqrt D hD δ hδ hK = GlobalNumberFields.maximalNumberFieldOrder K ↔ D.IsFundamentalDiscr

The embedded canonical order is maximal exactly at fundamental discriminants.

theorem TauCeti.QuadraticOrder.algEquivOfSqrt_apply_generator {K : Type u_1} [Field K] [NumberField K] (D : ℤ) [Fact ¬IsSquare D] (δ : K) (hδ : δ ^ 2 = ↑D) (hK : Module.finrank ℚ K = 2) : (algEquivOfSqrt D δ hδ hK) (generator D) = (↑D + δ) / 2

Evaluation sends the canonical half-integral generator to (D + δ)/2.

theorem TauCeti.QuadraticOrder.mem_numberFieldOrderOfSqrt_iff {K : Type u_1} [Field K] [NumberField K] (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) [Fact ¬IsSquare D] (δ : K) (hδ : δ ^ 2 = ↑D) (hK : Module.finrank ℚ K = 2) (x : K) : x ∈ (numberFieldOrderOfSqrt D hD δ hδ hK).toSubalgebra ↔ ∃ (m : ℤ) (n : ℤ), x = m • 1 + n • ((↑D + δ) / 2)

Membership in the embedded order is an integral linear combination of its two generators.

@[simp]

theorem TauCeti.QuadraticOrder.coe_equivNumberFieldOrderOfSqrt_apply {K : Type u_1} [Field K] [NumberField K] (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) [Fact ¬IsSquare D] (δ : K) (hδ : δ ^ 2 = ↑D) (hK : Module.finrank ℚ K = 2) (z : ↥(toSubalgebra D hD)) : ↑((equivNumberFieldOrderOfSqrt D hD δ hδ hK) z) = (algEquivOfSqrt D δ hδ hK) ↑z

The order equivalence evaluates its embedded elements at the chosen square root.

@[simp]

theorem TauCeti.QuadraticOrder.coe_basisOfSqrt_zero {K : Type u_1} [Field K] [NumberField K] (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) [Fact ¬IsSquare D] (δ : K) (hδ : δ ^ 2 = ↑D) (hK : Module.finrank ℚ K = 2) : ↑((basisOfSqrt D hD δ hδ hK) 0) = 1

The embedded integral basis starts with one.

@[simp]

theorem TauCeti.QuadraticOrder.coe_basisOfSqrt_one {K : Type u_1} [Field K] [NumberField K] (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) [Fact ¬IsSquare D] (δ : K) (hδ : δ ^ 2 = ↑D) (hK : Module.finrank ℚ K = 2) : ↑((basisOfSqrt D hD δ hδ hK) 1) = (↑D + δ) / 2

The second embedded basis vector is the half-integral generator.

theorem TauCeti.QuadraticOrder.numberFieldOrderOfSqrt_toSubalgebra_eq_adjoin {K : Type u_1} [Field K] [NumberField K] (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) [Fact ¬IsSquare D] (δ : K) (hδ : δ ^ 2 = ↑D) (hK : Module.finrank ℚ K = 2) : (numberFieldOrderOfSqrt D hD δ hδ hK).toSubalgebra = ℤ[(↑D + δ) / 2]

The order in the supplied field is generated by (D + δ)/2.