Gram determinants of integral lattices

This file attaches an integral Gram matrix to every basis of an integral lattice. Its determinant is independent of the carrier basis: an integral change-of-basis matrix has determinant 1 or -1, and the Gram matrix changes by multiplication by that matrix and its transpose. The resulting basis-free signed determinant and its absolute value are the determinant and discriminant of the lattice. An integral-lattice isometry carries every carrier basis to one with the same Gram matrix, so it preserves both basis-free invariants.

The rational scalar extension of a Gram matrix is the matrix of the ambient rational bilinear form in the extended basis. Consequently the signed determinant is nonzero exactly when that form is nondegenerate. This is the determinant criterion needed before constructing the finite discriminant group.

Main definitions

• TauCeti.IntegralLattice.gramMatrix: the integral matrix of the restricted form in a carrier basis.
• TauCeti.IntegralLattice.gramDet: its signed determinant.
• TauCeti.IntegralLattice.determinant: the basis-independent signed determinant.
• TauCeti.IntegralLattice.discriminant: the nonnegative absolute determinant.
• TauCeti.IntegralLattice.determinantUnit: the signed determinant of a nondegenerate lattice as a nonzero rational number.

Main results

• TauCeti.IntegralLattice.gramDet_eq_gramDet: Gram determinants agree in any two bases.
• TauCeti.IntegralLattice.gramDet_ne_zero_iff: a Gram determinant is nonzero exactly when the ambient form is nondegenerate.
• TauCeti.IntegralLattice.nondegenerate_integralForm_iff: the integral form on the carrier is nondegenerate exactly when the ambient form is.
• TauCeti.IntegralLattice.gramMatrix_ofGramMatrix: the Gram matrix of ofGramMatrix in its canonical basis is G.
• TauCeti.IntegralLattice.determinant_ofGramMatrix: the signed determinant of ofGramMatrix is the determinant of G.
• TauCeti.IntegralLattice.isNondegenerate_ofGramMatrix: a nonsingular Gram matrix produces a nondegenerate integral lattice.
• TauCeti.IntegralLattice.discriminant_ofGramMatrix: the discriminant of ofGramMatrix is the absolute determinant of G.
• TauCeti.IntegralLattice.Isometry.determinant_eq and Isometry.discriminant_eq: isometry invariance of the basis-free invariants.
• TauCeti.IntegralLattice.Isometry.ofGramMatrixEq: lattices with bases of equal Gram matrices are isometric.

References

• W. Ebeling, Lattices and Codes, Chapter 1.
• TauCetiRoadmap/IntegralLattices/README.md, Layer 1.

noncomputable def TauCeti.IntegralLattice.gramMatrix {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {ι : Type v} (e : Module.Basis ι ℤ ↥L.carrier) : Matrix ι ι ℤ

The integral Gram matrix of a carrier basis.

Equations

• L.gramMatrix e = (LinearMap.BilinForm.toMatrixAux ⇑e) L.integralForm

@[simp]

theorem TauCeti.IntegralLattice.gramMatrix_apply {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {ι : Type v} (e : Module.Basis ι ℤ ↥L.carrier) (i j : ι) : L.gramMatrix e i j = (L.integralForm (e i)) (e j)

A Gram-matrix entry is the value of the integral form on the corresponding basis vectors.

theorem TauCeti.IntegralLattice.gramMatrix_eq_toMatrix {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {ι : Type v} [Fintype ι] [DecidableEq ι] (e : Module.Basis ι ℤ ↥L.carrier) : L.gramMatrix e = (LinearMap.BilinForm.toMatrix e) L.integralForm

The Gram matrix is Mathlib's matrix of the restricted integral bilinear form.

theorem TauCeti.IntegralLattice.intCast_gramMatrix_apply {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {ι : Type v} (e : Module.Basis ι ℤ ↥L.carrier) (i j : ι) : ↑(L.gramMatrix e i j) = (L.form ↑(e i)) ↑(e j)

Casting a Gram-matrix entry to ℚ recovers the ambient rational form.

theorem TauCeti.IntegralLattice.isSymm_gramMatrix {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {ι : Type v} (e : Module.Basis ι ℤ ↥L.carrier) : (L.gramMatrix e).IsSymm

The Gram matrix of a symmetric integral lattice is symmetric.

theorem TauCeti.IntegralLattice.map_gramMatrix {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {ι : Type v} [Fintype ι] [DecidableEq ι] (e : Module.Basis ι ℤ ↥L.carrier) : (L.gramMatrix e).map ⇑(algebraMap ℤ ℚ) = (LinearMap.BilinForm.toMatrix (Module.Basis.extendOfIsLattice ℚ e)) L.form

Extending the carrier basis and the entries of its Gram matrix to ℚ gives the matrix of the ambient rational form.

noncomputable def TauCeti.IntegralLattice.gramDet {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {ι : Type v} [Fintype ι] [DecidableEq ι] (e : Module.Basis ι ℤ ↥L.carrier) : ℤ

The signed determinant of the Gram matrix in a carrier basis.

Equations

• L.gramDet e = (L.gramMatrix e).det

theorem TauCeti.IntegralLattice.gramDet_def {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {ι : Type v} [Fintype ι] [DecidableEq ι] (e : Module.Basis ι ℤ ↥L.carrier) : L.gramDet e = (L.gramMatrix e).det

Unfolding the signed Gram determinant to the matrix determinant.

theorem TauCeti.IntegralLattice.intCast_gramDet {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {ι : Type v} [Fintype ι] [DecidableEq ι] (e : Module.Basis ι ℤ ↥L.carrier) : ↑(L.gramDet e) = ((LinearMap.BilinForm.toMatrix (Module.Basis.extendOfIsLattice ℚ e)) L.form).det

Casting the signed Gram determinant to ℚ gives the determinant of the ambient rational form in the extended basis.

theorem TauCeti.IntegralLattice.gramMatrix_reindex {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {ι : Type v} {κ : Type w} (e : Module.Basis ι ℤ ↥L.carrier) (σ : ι ≃ κ) : L.gramMatrix (e.reindex σ) = (L.gramMatrix e).submatrix ⇑σ.symm ⇑σ.symm

Reindexing a carrier basis simultaneously reindexes the rows and columns of its Gram matrix.

theorem TauCeti.IntegralLattice.gramDet_reindex {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {ι : Type v} {κ : Type w} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (e : Module.Basis ι ℤ ↥L.carrier) (σ : ι ≃ κ) : L.gramDet (e.reindex σ) = L.gramDet e

Reindexing a carrier basis does not change its signed Gram determinant.

theorem TauCeti.IntegralLattice.gramDet_eq_gramDet {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {ι : Type v} {κ : Type w} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (e : Module.Basis ι ℤ ↥L.carrier) (f : Module.Basis κ ℤ ↥L.carrier) : L.gramDet e = L.gramDet f

The signed Gram determinant is independent of the carrier basis. This permits both the index type and the basis to change.

@[simp]

theorem TauCeti.IntegralLattice.gramDet_ne_zero_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {ι : Type v} [Fintype ι] [DecidableEq ι] (e : Module.Basis ι ℤ ↥L.carrier) : L.gramDet e ≠ 0 ↔ L.form.Nondegenerate

A Gram determinant is nonzero exactly when the ambient rational form is nondegenerate.

@[simp]

theorem TauCeti.IntegralLattice.gramMatrix_ofGramMatrix {V : Type u} [AddCommGroup V] [Module ℚ V] {ι : Type v} [Fintype ι] (b : Module.Basis ι ℚ V) (G : Matrix ι ι ℤ) (hG : G.IsSymm) : (ofGramMatrix b G hG).gramMatrix (ofGramMatrix.basis b G hG) = G

The Gram matrix of ofGramMatrix b G hG in its canonical carrier basis is G.

@[simp]

theorem TauCeti.IntegralLattice.gramDet_ofGramMatrix {V : Type u} [AddCommGroup V] [Module ℚ V] {ι : Type v} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℚ V) (G : Matrix ι ι ℤ) (hG : G.IsSymm) : (ofGramMatrix b G hG).gramDet (ofGramMatrix.basis b G hG) = G.det

The signed Gram determinant of ofGramMatrix b G hG in its canonical carrier basis is the determinant of G.

noncomputable def TauCeti.IntegralLattice.determinant {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : ℤ

The basis-independent signed determinant of an integral lattice.

Equations

• L.determinant = L.gramDet (Module.Free.chooseBasis ℤ ↥L.carrier)

theorem TauCeti.IntegralLattice.determinant_eq_gramDet {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {ι : Type v} [Fintype ι] [DecidableEq ι] (e : Module.Basis ι ℤ ↥L.carrier) : L.determinant = L.gramDet e

The signed determinant agrees with the determinant of the Gram matrix in every carrier basis.

@[simp]

theorem TauCeti.IntegralLattice.determinant_ofGramMatrix {V : Type u} [AddCommGroup V] [Module ℚ V] {ι : Type v} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℚ V) (G : Matrix ι ι ℤ) (hG : G.IsSymm) : (ofGramMatrix b G hG).determinant = G.det

The basis-independent signed determinant of ofGramMatrix b G hG is the determinant of G.

@[simp]

theorem TauCeti.IntegralLattice.determinant_ne_zero_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.determinant ≠ 0 ↔ L.form.Nondegenerate

The basis-independent determinant is nonzero exactly when the ambient rational form is nondegenerate.

noncomputable def TauCeti.IntegralLattice.determinantUnit {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] : ℚˣ

The signed Gram determinant of a nondegenerate integral lattice, regarded as a nonzero rational number.

Equations

• L.determinantUnit = Units.mk0 ↑L.determinant ⋯

@[simp]

theorem TauCeti.IntegralLattice.coe_determinantUnit {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] : ↑L.determinantUnit = ↑L.determinant

The value underlying determinantUnit is the integral Gram determinant cast to ℚ.

theorem TauCeti.IntegralLattice.nondegenerate_integralForm_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.integralForm.Nondegenerate ↔ L.form.Nondegenerate

The integral form on the carrier is nondegenerate exactly when the ambient rational form is.

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

An integral lattice constructed from a nonsingular Gram matrix is nondegenerate.

noncomputable def TauCeti.IntegralLattice.discriminant {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : ℕ

The nonnegative discriminant of an integral lattice is the absolute value of its signed determinant.

Equations

• L.discriminant = L.determinant.natAbs

theorem TauCeti.IntegralLattice.discriminant_def {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.discriminant = L.determinant.natAbs

Unfolding the discriminant to the absolute value of the signed determinant.

theorem TauCeti.IntegralLattice.discriminant_eq_natAbs_gramDet {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {ι : Type v} [Fintype ι] [DecidableEq ι] (e : Module.Basis ι ℤ ↥L.carrier) : L.discriminant = (L.gramDet e).natAbs

The discriminant is the absolute value of the Gram determinant in every carrier basis.

@[simp]

theorem TauCeti.IntegralLattice.discriminant_ofGramMatrix {V : Type u} [AddCommGroup V] [Module ℚ V] {ι : Type v} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℚ V) (G : Matrix ι ι ℤ) (hG : G.IsSymm) : (ofGramMatrix b G hG).discriminant = G.det.natAbs

The discriminant of ofGramMatrix b G hG is the absolute value of the determinant of G.

@[simp]

theorem TauCeti.IntegralLattice.discriminant_pos_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : 0 < L.discriminant ↔ L.form.Nondegenerate

The discriminant is positive exactly when the ambient rational form is nondegenerate.

theorem TauCeti.IntegralLattice.Isometry.gramMatrix_carrierBasisEquiv {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type w} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) {ι : Type v} (b : Module.Basis ι ℤ ↥L.carrier) : M.gramMatrix ((e.carrierBasisEquiv ι) b) = L.gramMatrix b

Transporting a carrier basis along an isometry preserves its Gram matrix entrywise.

theorem TauCeti.IntegralLattice.Isometry.gramDet_carrierBasisEquiv {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type w} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) {ι : Type v} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℤ ↥L.carrier) : M.gramDet ((e.carrierBasisEquiv ι) b) = L.gramDet b

Transporting a carrier basis along an isometry preserves its signed Gram determinant.

theorem TauCeti.IntegralLattice.Isometry.determinant_eq {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type w} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : L.determinant = M.determinant

The basis-independent signed determinant is invariant under integral-lattice isometry.

theorem TauCeti.IntegralLattice.Isometry.discriminant_eq {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type w} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : L.discriminant = M.discriminant

The nonnegative discriminant is invariant under integral-lattice isometry.

noncomputable def TauCeti.IntegralLattice.Isometry.ofGramMatrixEq {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type w} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} {ι : Type v} (b : Module.Basis ι ℤ ↥L.carrier) (b' : Module.Basis ι ℤ ↥M.carrier) (h : L.gramMatrix b = M.gramMatrix b') : L.Isometry M

Lattices with bases of equal Gram matrices are isometric. The isometry carries the i-th vector of the first basis to the i-th vector of the second; this is the converse of TauCeti.IntegralLattice.Isometry.gramMatrix_carrierBasisEquiv.

Equations

• TauCeti.IntegralLattice.Isometry.ofGramMatrixEq b b' h = TauCeti.IntegralLattice.Isometry.ofCarrierEquiv (b.equiv b' (Equiv.refl ι)) ⋯

@[simp]

theorem TauCeti.IntegralLattice.Isometry.ofGramMatrixEq_apply_basis {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type w} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} {ι : Type v} (b : Module.Basis ι ℤ ↥L.carrier) (b' : Module.Basis ι ℤ ↥M.carrier) (h : L.gramMatrix b = M.gramMatrix b') (i : ι) : (ofGramMatrixEq b b' h) ↑(b i) = ↑(b' i)

The isometry ofGramMatrixEq b b' h carries each vector of b to the corresponding vector of b'.