Cardinality of an integral lattice's discriminant group

For a nondegenerate integral lattice L, the order of its discriminant group is the absolute value of any Gram determinant:

#(Lᵛ / L) = |det Gram(L)|.

The proof uses Mathlib's quotient-cardinality theorem for full-rank free ℤ-submodules. Given a carrier basis b, the corresponding bilinear dual basis is a basis of Lᵛ, while b itself gives a basis of the copy of L inside Lᵛ. The change-of-basis matrix between them is the Gram matrix of b: the coefficient of b j along the dual vector indexed by i is B(b j, b i), which equals B(b i, b j) by symmetry.

Main results

• TauCeti.IntegralLattice.dualCarrierBasis_toMatrix_carrierInDualBasis: the associated change-of-basis matrix is the Gram matrix.
• TauCeti.IntegralLattice.natCard_discriminantGroup_eq_natAbs_gramDet: the basis-relative cardinality formula.
• TauCeti.IntegralLattice.natCard_discriminantGroup: the discriminant-group cardinality is the lattice discriminant.
• TauCeti.IntegralLattice.natCard_discriminantGroup_ofGramMatrix: the formula for a lattice constructed from a nonsingular integral symmetric matrix.

References

• W. Ebeling, Lattices and Codes, Chapter 1.
• TauCetiRoadmap/IntegralLattices/README.md (Layer 2).
• TauCetiRoadmap/IntegralLattices/Suggested.lean.

theorem TauCeti.IntegralLattice.dualCarrierBasis_toMatrix_carrierInDualBasis {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] {ι : Type v} [Finite ι] (b : Module.Basis ι ℤ ↥L.carrier) : (L.dualCarrierBasis b).toMatrix (Subtype.val ∘ ⇑(L.carrierInDualBasis b)) = L.gramMatrix b

The change-of-basis matrix from the dual basis to the embedded carrier basis is the Gram matrix.

theorem TauCeti.IntegralLattice.dualCarrierBasis_det_carrierInDualBasis {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] {ι : Type v} [Fintype ι] (b : Module.Basis ι ℤ ↥L.carrier) : (L.dualCarrierBasis b).det (Subtype.val ∘ ⇑(L.carrierInDualBasis b)) = L.gramDet b

The determinant of the carrier basis inside the dual basis is the signed Gram determinant.

theorem TauCeti.IntegralLattice.natCard_discriminantGroup_eq_natAbs_gramDet {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] {ι : Type v} [Fintype ι] (b : Module.Basis ι ℤ ↥L.carrier) : Nat.card L.DiscriminantGroup = (L.gramDet b).natAbs

The discriminant group has cardinality equal to the absolute value of the Gram determinant in any carrier basis.

theorem TauCeti.IntegralLattice.natCard_discriminantGroup {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] : Nat.card L.DiscriminantGroup = L.discriminant

The order of the discriminant group is the lattice discriminant.

@[simp]

theorem TauCeti.IntegralLattice.natCard_discriminantGroup_ofGramMatrix {V : Type u} [AddCommGroup V] [Module ℚ V] {ι : Type v} [Fintype ι] (b : Module.Basis ι ℚ V) (G : Matrix ι ι ℤ) (hG : G.IsSymm) (hdet : G.det ≠ 0) : Nat.card (ofGramMatrix b G hG).DiscriminantGroup = G.det.natAbs

The discriminant group of a lattice constructed from a nonsingular integral symmetric matrix has cardinality equal to the absolute value of that matrix's determinant.