The quadratic order of a binary integral lattice

The primitive norm discriminant Δ determines the embedded order ℤ[(Δ + √Δ)/2] in its rational quadratic algebra. This order is free of rank two and has trace-pairing discriminant Δ, with integral basis 1, (Δ + √Δ)/2.

For a nondegenerate lattice the rational algebra is étale. A nonsquare discriminant returns the actual number-field order, whose conductor is generated by its index in the maximal order. It is maximal precisely for fundamental discriminants. A square discriminant returns an integer congruence product order through the rational splitting equivalence.

References

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

noncomputable def TauCeti.IntegralLattice.binaryOrder {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hV : Module.finrank ℚ V = 2) : Subalgebra ℤ (QuadraticAlgebra ℚ (↑(L.binaryDiscriminant hV)) 0)

The canonical quadratic order of the primitive norm discriminant of the lattice.

theorem TauCeti.IntegralLattice.binaryOrder_def {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hV : Module.finrank ℚ V = 2) : L.binaryOrder hV = QuadraticOrder.toSubalgebra (L.binaryDiscriminant hV) ⋯

The lattice order is the quadratic order of its primitive discriminant.

theorem TauCeti.IntegralLattice.mem_binaryOrder_iff {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hV : Module.finrank ℚ V = 2) (x : QuadraticAlgebra ℚ (↑(L.binaryDiscriminant hV)) 0) : x ∈ L.binaryOrder hV ↔ ∃ (a : ℤ) (b : ℤ), x = ↑a + ↑b * QuadraticOrder.generator (L.binaryDiscriminant hV)

Members of the lattice order have integral coefficients in its two generators.

theorem TauCeti.IntegralLattice.binaryOrder_eq_adjoin {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hV : Module.finrank ℚ V = 2) : L.binaryOrder hV = ℤ[QuadraticOrder.generator (L.binaryDiscriminant hV)]

The lattice order is generated by its half-integral square root.

noncomputable def TauCeti.IntegralLattice.binaryOrderBasis {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hV : Module.finrank ℚ V = 2) : Module.Basis (Fin 2) ℤ ↥(L.binaryOrder hV)

The lattice order has an integral basis of size two.

instance TauCeti.IntegralLattice.instFiniteBinaryOrder {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hV : Module.finrank ℚ V = 2) : Module.Finite ℤ ↥(L.binaryOrder hV)

The lattice order is finite over the integers.

instance TauCeti.IntegralLattice.instFreeBinaryOrder {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hV : Module.finrank ℚ V = 2) : Module.Free ℤ ↥(L.binaryOrder hV)

The lattice order is free over the integers.

@[simp]

theorem TauCeti.IntegralLattice.coe_binaryOrderBasis_zero {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hV : Module.finrank ℚ V = 2) : ↑((L.binaryOrderBasis hV) 0) = 1

The first integral basis vector of the lattice order is one.

@[simp]

theorem TauCeti.IntegralLattice.coe_binaryOrderBasis_one {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hV : Module.finrank ℚ V = 2) : ↑((L.binaryOrderBasis hV) 1) = QuadraticOrder.generator (L.binaryDiscriminant hV)

The second integral basis vector is the half-integral square root generator.

theorem TauCeti.IntegralLattice.discr_binaryOrderBasis {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hV : Module.finrank ℚ V = 2) : Algebra.discr ℤ ⇑(L.binaryOrderBasis hV) = L.binaryDiscriminant hV

The primitive lattice discriminant is the actual trace-pairing order discriminant.

theorem TauCeti.IntegralLattice.etale_binaryQuadraticAlgebra {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hV : Module.finrank ℚ V = 2) [L.IsNondegenerate] : Algebra.Etale ℚ (QuadraticAlgebra ℚ (↑(L.binaryDiscriminant hV)) 0)

The nondegenerate lattice's rational quadratic algebra is étale.

noncomputable def TauCeti.IntegralLattice.binaryNumberFieldOrder {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hV : Module.finrank ℚ V = 2) [Fact ¬IsSquare (L.binaryDiscriminant hV)] : GlobalNumberFields.NumberFieldOrder (QuadraticAlgebra ℚ (↑(L.binaryDiscriminant hV)) 0)

A nonsquare primitive discriminant determines the actual number-field order.

@[simp]

theorem TauCeti.IntegralLattice.binaryNumberFieldOrder_toSubalgebra {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hV : Module.finrank ℚ V = 2) [Fact ¬IsSquare (L.binaryDiscriminant hV)] : (L.binaryNumberFieldOrder hV).toSubalgebra = L.binaryOrder hV

The nonsquare field order has the common lattice order as its embedded carrier.

@[simp]

theorem TauCeti.IntegralLattice.binaryNumberFieldOrder_discr {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hV : Module.finrank ℚ V = 2) [Fact ¬IsSquare (L.binaryDiscriminant hV)] : (L.binaryNumberFieldOrder hV).discr = L.binaryDiscriminant hV

The field order's discriminant equals the primitive lattice discriminant.

@[simp]

theorem TauCeti.IntegralLattice.binaryNumberFieldOrder_conductor {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hV : Module.finrank ℚ V = 2) [Fact ¬IsSquare (L.binaryDiscriminant hV)] : (L.binaryNumberFieldOrder hV).conductor = Ideal.span {↑(L.binaryNumberFieldOrder hV).index}

The conductor of the nonsquare lattice order is generated by its index in the maximal order.

@[simp]

theorem TauCeti.IntegralLattice.binaryNumberFieldOrder_eq_maximal_iff {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hV : Module.finrank ℚ V = 2) [Fact ¬IsSquare (L.binaryDiscriminant hV)] : L.binaryNumberFieldOrder hV = GlobalNumberFields.maximalNumberFieldOrder (QuadraticAlgebra ℚ (↑(L.binaryDiscriminant hV)) 0) ↔ (L.binaryDiscriminant hV).IsFundamentalDiscr

In the field branch, maximality is precisely fundamentalness of the primitive discriminant.

noncomputable def TauCeti.IntegralLattice.binaryOrderEquivProductOfSq {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hV : Module.finrank ℚ V = 2) [L.IsNondegenerate] (s : ℤ) (hSq : L.binaryDiscriminant hV = s ^ 2) : ↥(L.binaryOrder hV) ≃ₐ[ℤ] ↥(QuadraticOrder.productSubalgebra s)

A nonzero square primitive discriminant returns an explicit integer congruence product order, independently of the field-order interface.