Documentation

TauCeti.NumberTheory.QuadraticOrder.Field

Nonsquare quadratic orders #

For a nonsquare integer D ≡ 0, 1 mod 4, the rational quadratic algebra is a number field. The subalgebra ℤ[(D + √D)/2] constructed in QuadraticOrder/Basic is therefore an actual GlobalNumberFields.NumberFieldOrder, of discriminant D.

This order is maximal exactly when D is a fundamental discriminant. For a fundamental D, the supplier's discriminant/index formula and Stickelberger's congruence force index one. If D is not fundamental, a proper square factor D = p²e with e ≡ 0, 1 mod 4 supplies the integral element (e + √D/p)/2 outside the order.

References #

source
noncomputable def TauCeti.QuadraticOrder.numberFieldOrder (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) [Fact ¬IsSquare D] :
GlobalNumberFields.NumberFieldOrder (QuadraticAlgebra ℚ (↑D) 0)

The integral quadratic order in the nonsquare number field.

Instances For
    source
    @[simp]
    theorem TauCeti.QuadraticOrder.numberFieldOrder_toSubalgebra (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) [Fact ¬IsSquare D] :
    (numberFieldOrder D hD).toSubalgebra = toSubalgebra D hD

    The field order has the subalgebra constructed in the rational quadratic algebra.

    source
    @[simp]
    theorem TauCeti.QuadraticOrder.numberFieldOrder_discr (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) [Fact ¬IsSquare D] :
    (numberFieldOrder D hD).discr = D

    The discriminant of the field order is its defining integer.

    source
    @[simp]
    theorem TauCeti.QuadraticOrder.numberFieldOrder_eq_maximal_iff (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) [Fact ¬IsSquare D] :
    numberFieldOrder D hD = GlobalNumberFields.maximalNumberFieldOrder (QuadraticAlgebra ℚ (↑D) 0) ↔ D.IsFundamentalDiscr

    The quadratic field order is maximal exactly when its discriminant is fundamental.

    source
    theorem TauCeti.QuadraticOrder.toSubalgebra_eq_integralClosure_iff (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) [Fact ¬IsSquare D] :
    toSubalgebra D hD = integralClosure ℤ (QuadraticAlgebra ℚ (↑D) 0) ↔ D.IsFundamentalDiscr

    The order ℤ[(D + √D)/2] is the ring of integers exactly when D is fundamental. The subalgebra TauCeti.QuadraticOrder.toSubalgebra D of the model ℚ(√D) is the integral closure of ℤ if and only if D is a fundamental discriminant.