Integral orders in rational quadratic algebras

For an integer D ≡ 0, 1 mod 4, the element (D + ω)/2 in QuadraticAlgebra ℚ D 0 satisfies an integral quadratic relation. Its generated subalgebra has the integral basis 1, (D + ω)/2, whose trace-pairing discriminant is D. The basis spans the rational quadratic algebra. This construction applies to both square and nonsquare parameters; it does not require an ambient field.

The embedding uses the integral model QuadraticAlgebra ℤ ((D - D²)/4) D and Mathlib's universal algebra homomorphism. The range description characterizes every order element by its two integral coefficients.

References

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

def TauCeti.QuadraticOrder.generator (D : ℤ) : QuadraticAlgebra ℚ (↑D) 0

The integral generator (D + √D)/2 in the rational quadratic algebra.

@[simp]

theorem TauCeti.QuadraticOrder.generator_re (D : ℤ) : (generator D).re = ↑D / 2

The rational coefficient of the half-integral generator.

@[simp]

theorem TauCeti.QuadraticOrder.generator_im (D : ℤ) : (generator D).im = 1 / 2

The square-root coefficient of the half-integral generator.

theorem TauCeti.QuadraticOrder.mul_im_eq_half_of_mutual_generators (D a : ℤ) (ha : 0 < a) (τ : QuadraticAlgebra ℚ (↑D) 0) (hτim : 0 < τ.im) (m n r s : ℤ) (hθrep : ↑a * τ = m • 1 + n • generator D) (hgenrep : generator D = r • 1 + s • (↑a * τ)) : ↑a * τ.im = 1 / 2

Mutual integral expressions for a positive-imaginary generator and a positive multiple of τ force the latter to have the canonical half-integral imaginary coefficient.

theorem TauCeti.QuadraticOrder.parameter_discr (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) : QuadraticAlgebra.discr ((D - D ^ 2) / 4) D = D

The integral parameter has quadratic discriminant D for a valid discriminant.

theorem TauCeti.QuadraticOrder.generator_mul_generator (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) : generator D * generator D = ((D - D ^ 2) / 4) • 1 + D • generator D

The half-integral generator satisfies the defining integral relation.

def TauCeti.QuadraticOrder.lift (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) : QuadraticAlgebra ℤ ((D - D ^ 2) / 4) D →ₐ[ℤ] QuadraticAlgebra ℚ (↑D) 0

Embedding the integral quadratic algebra generated by (D + √D)/2.

theorem TauCeti.QuadraticOrder.lift_apply (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) (z : QuadraticAlgebra ℤ ((D - D ^ 2) / 4) D) : (lift D hD) z = z.re • 1 + z.im • generator D

Evaluation of the integral-model embedding in its two coefficients.

@[simp]

theorem TauCeti.QuadraticOrder.lift_omega (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) : (lift D hD) QuadraticAlgebra.omega = generator D

The integral-model generator maps to the half-integral generator.

theorem TauCeti.QuadraticOrder.lift_injective (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) : Function.Injective ⇑(lift D hD)

The two integral generators are linearly independent.

def TauCeti.QuadraticOrder.toSubalgebra (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) : Subalgebra ℤ (QuadraticAlgebra ℚ (↑D) 0)

The actual integral order as a subalgebra of the quadratic algebra.

theorem TauCeti.QuadraticOrder.mem_toSubalgebra_iff (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) (z : QuadraticAlgebra ℚ (↑D) 0) : z ∈ toSubalgebra D hD ↔ ∃ (m : ℤ) (n : ℤ), z = m • 1 + n • generator D

Every element of the order has two integral coefficients in the basis 1, (D + √D)/2.

theorem TauCeti.QuadraticOrder.toSubalgebra_eq_adjoin (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) : toSubalgebra D hD = ℤ[generator D]

The order is generated by (D + √D)/2.

noncomputable def TauCeti.QuadraticOrder.equivToSubalgebra (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) : QuadraticAlgebra ℤ ((D - D ^ 2) / 4) D ≃ₐ[ℤ] ↥(toSubalgebra D hD)

The integral model is algebra-isomorphic to the embedded order.

@[simp]

theorem TauCeti.QuadraticOrder.coe_equivToSubalgebra_apply (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) (z : QuadraticAlgebra ℤ ((D - D ^ 2) / 4) D) : ↑((equivToSubalgebra D hD) z) = (lift D hD) z

The integral-model equivalence preserves its image in the quadratic algebra.

instance TauCeti.QuadraticOrder.instFinite (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) : Module.Finite ℤ ↥(toSubalgebra D hD)

The embedded order is finite over the integers.

theorem TauCeti.QuadraticOrder.isIntegral (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) (z : ↥(toSubalgebra D hD)) : IsIntegral ℤ ↑z

Every element of the embedded order is integral over the integers.

noncomputable def TauCeti.QuadraticOrder.basis (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) : Module.Basis (Fin 2) ℤ ↥(toSubalgebra D hD)

The integral basis 1, (D + √D)/2 of the order.

instance TauCeti.QuadraticOrder.instFree (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) : Module.Free ℤ ↥(toSubalgebra D hD)

The embedded order is free over the integers.

theorem TauCeti.QuadraticOrder.discr_basis (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) : Algebra.discr ℤ ⇑(basis D hD) = D

The trace-pairing discriminant of the order basis is D.

theorem TauCeti.QuadraticOrder.span_toSubalgebra_eq_top (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) : Submodule.span ℚ ↑(toSubalgebra D hD) = ⊤

The embedded order spans the rational quadratic algebra.

@[simp]

theorem TauCeti.QuadraticOrder.coe_basis_zero (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) : ↑((basis D hD) 0) = 1

The first order basis vector is one.

@[simp]

theorem TauCeti.QuadraticOrder.coe_basis_one (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) : ↑((basis D hD) 1) = generator D

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