Integral symmetric lattices

An integral symmetric lattice in a rational vector space consists of a full finitely generated ℤ-submodule together with a symmetric ℚ-bilinear form whose values on the lattice are integers. The integrality condition is expressed using Mathlib's LinearMap.BilinForm.dualSubmodule: the carrier is contained in its dual submodule.

The form restricts to a canonical ℤ-bilinear form on the carrier. Conversely, a finite ℚ-basis and an integral symmetric Gram matrix construct an integral lattice.

References

• TauCetiRoadmap/IntegralLattices/README.md
• TauCetiRoadmap/IntegralLattices/Suggested.lean

Main definitions

• TauCeti.IntegralLattice: an integral symmetric lattice in a rational vector space.
• TauCeti.IntegralLattice.IsNondegenerate: the nondegeneracy mixin for an integral lattice.
• TauCeti.IntegralLattice.form_mem_one: the rational form takes integer values on lattice vectors.
• TauCeti.IntegralLattice.le_dualSubmodule_of_le_carrier: every submodule of the carrier is integral for the lattice form.
• TauCeti.IntegralLattice.rationalBasis: the ambient ℚ-basis extending a chosen ℤ-basis of the carrier.
• TauCeti.IntegralLattice.integralForm: the induced ℤ-bilinear form on the carrier.
• TauCeti.IntegralLattice.ofSubmodule: constructor from a full submodule, symmetric form, and integrality proof.
• TauCeti.IntegralLattice.ofBasis: the lattice spanned by a basis on which a given form is integral.
• TauCeti.IntegralLattice.ofBasis.basis: the canonical carrier basis induced by a rational basis.
• TauCeti.IntegralLattice.ofGramMatrix: the lattice and form determined by an integral symmetric Gram matrix.
• TauCeti.IntegralLattice.ofGramMatrix.basis: the canonical carrier basis induced by a rational basis.

structure TauCeti.IntegralLattice (V : Type u) [AddCommGroup V] [Module ℚ V] : Type u

An integral symmetric lattice in a rational vector space.

The field le_dual says exactly that the form takes integer values on pairs of vectors in carrier.

• carrier : Submodule ℤ V

  The full ℤ-submodule underlying the lattice.

• form : LinearMap.BilinForm ℚ V

  The rational symmetric bilinear form on the ambient vector space.

• isLattice : Submodule.IsLattice ℚ self.carrier

  The carrier is finitely generated and spans the ambient rational vector space.

• isSymm : self.form.IsSymm

  The rational bilinear form is symmetric.

• le_dual : self.carrier ≤ self.form.dualSubmodule self.carrier

  Every vector of the carrier lies in its dual submodule.

instance TauCeti.IntegralLattice.instIsLatticeIntRatCarrier {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : Submodule.IsLattice ℚ L.carrier

The carrier of an integral lattice is a Mathlib lattice.

@[instance_reducible]

instance TauCeti.IntegralLattice.instCoeSortType {V : Type u} [AddCommGroup V] [Module ℚ V] : CoeSort (IntegralLattice V) (Type u)

An integral lattice coerces to the type of its vectors.

Equations

• TauCeti.IntegralLattice.instCoeSortType = { coe := fun (L : TauCeti.IntegralLattice V) => ↥L.carrier }

@[instance_reducible]

instance TauCeti.IntegralLattice.instCoeFunForallForallRat {V : Type u} [AddCommGroup V] [Module ℚ V] : CoeFun (IntegralLattice V) fun (x : IntegralLattice V) => V → V → ℚ

An integral lattice coerces to its rational bilinear form.

Equations

• TauCeti.IntegralLattice.instCoeFunForallForallRat = { coe := fun (L : TauCeti.IntegralLattice V) (x y : V) => (L.form x) y }

@[simp]

theorem TauCeti.IntegralLattice.coe_form_apply {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x y : V) : (fun (x y : V) => (L.form x) y) x y = (L.form x) y

@[simp]

theorem TauCeti.IntegralLattice.form_flip {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.form.flip = L.form

The flipped rational bilinear form of an integral lattice equals the form itself.

theorem TauCeti.IntegralLattice.form_mem_one {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x y : ↥L.carrier) : (L.form ↑x) ↑y ∈ 1

The value of the rational form on lattice vectors is integral.

theorem TauCeti.IntegralLattice.le_dualSubmodule_of_le_carrier {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {N : Submodule ℤ V} (hN : N ≤ L.carrier) : N ≤ L.form.dualSubmodule N

Every ambient submodule contained in the carrier is integral for the lattice form.

noncomputable def TauCeti.IntegralLattice.rationalBasis {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : Module.Basis (Module.Free.ChooseBasisIndex ℤ ↥L.carrier) ℚ V

The chosen ℤ-basis of an integral lattice extends to a ℚ-basis of the ambient space.

Equations

• L.rationalBasis = Module.Basis.extendOfIsLattice ℚ (Module.Free.chooseBasis ℤ ↥L.carrier)

@[simp]

theorem TauCeti.IntegralLattice.rationalBasis_apply {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (i : Module.Free.ChooseBasisIndex ℤ ↥L.carrier) : L.rationalBasis i = ↑((Module.Free.chooseBasis ℤ ↥L.carrier) i)

theorem TauCeti.IntegralLattice.finiteDimensional {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : FiniteDimensional ℚ V

The ambient rational vector space of an integral lattice is finite-dimensional.

theorem TauCeti.IntegralLattice.finrank_carrier {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : Module.finrank ℤ ↥L.carrier = Module.finrank ℚ V

The ℤ-finrank of the carrier of an integral lattice equals the ℚ-finrank of the ambient space.

theorem TauCeti.IntegralLattice.ext {V : Type u} [AddCommGroup V] [Module ℚ V] {L M : IntegralLattice V} (hcarrier : L.carrier = M.carrier) (hform : L.form = M.form) : L = M

Two integral lattices are equal if their carriers and rational forms are equal.

theorem TauCeti.IntegralLattice.ext_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {L M : IntegralLattice V} : L = M ↔ L.carrier = M.carrier ∧ L.form = M.form

class TauCeti.IntegralLattice.IsNondegenerate {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : Prop

An integral lattice is nondegenerate when its ambient rational bilinear form is nondegenerate. This is a mixin rather than a field of IntegralLattice, so degenerate lattices remain objects of the same type.

• nondegenerate : L.form.Nondegenerate

  The rational bilinear form has trivial kernel.

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

The ambient form of a nondegenerate integral lattice is nondegenerate.

noncomputable def TauCeti.IntegralLattice.integralForm {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : LinearMap.BilinForm ℤ ↥L.carrier

The integral bilinear form induced on the carrier.

This is the integral-valued restriction of L.form, obtained from Mathlib's canonical pairing between a submodule and its dual submodule.

Equations

• L.integralForm = L.form.dualSubmoduleToDual L.carrier ∘ₗ Submodule.inclusion ⋯

@[simp]

theorem TauCeti.IntegralLattice.integralForm_cast {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x y : ↥L.carrier) : ↑((L.integralForm x) y) = (L.form ↑x) ↑y

The integral form recovers the rational form after coercion to ℚ.

theorem TauCeti.IntegralLattice.isSymm_integralForm {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.integralForm.IsSymm

The induced integral form is symmetric.

def TauCeti.IntegralLattice.ofSubmodule {V : Type u} [AddCommGroup V] [Module ℚ V] (S : Submodule ℤ V) [hS : Submodule.IsLattice ℚ S] (B : LinearMap.BilinForm ℚ V) (hB : B.IsSymm) (hle : S ≤ B.dualSubmodule S) : IntegralLattice V

Construct an integral lattice from a full submodule, a symmetric rational bilinear form, and an integrality proof.

Equations

• TauCeti.IntegralLattice.ofSubmodule S B hB hle = { carrier := S, form := B, isLattice := hS, isSymm := hB, le_dual := hle }

@[simp]

theorem TauCeti.IntegralLattice.ofSubmodule_carrier {V : Type u} [AddCommGroup V] [Module ℚ V] (S : Submodule ℤ V) [hS : Submodule.IsLattice ℚ S] (B : LinearMap.BilinForm ℚ V) (hB : B.IsSymm) (hle : S ≤ B.dualSubmodule S) : (ofSubmodule S B hB hle).carrier = S

@[simp]

theorem TauCeti.IntegralLattice.ofSubmodule_form {V : Type u} [AddCommGroup V] [Module ℚ V] (S : Submodule ℤ V) [hS : Submodule.IsLattice ℚ S] (B : LinearMap.BilinForm ℚ V) (hB : B.IsSymm) (hle : S ≤ B.dualSubmodule S) : (ofSubmodule S B hB hle).form = B

theorem TauCeti.IntegralLattice.isLattice_span_basis {V : Type u} [AddCommGroup V] [Module ℚ V] {ι : Type u_1} [Finite ι] (b : Module.Basis ι ℚ V) : Submodule.IsLattice ℚ (Submodule.span ℤ (Set.range ⇑b))

The ℤ-span of a finite rational basis is a Mathlib lattice.

noncomputable def TauCeti.IntegralLattice.ofBasis {V : Type u} [AddCommGroup V] [Module ℚ V] {ι : Type u_1} [Finite ι] (b : Module.Basis ι ℚ V) (B : LinearMap.BilinForm ℚ V) (hB : B.IsSymm) (hint : ∀ (i j : ι), (B (b i)) (b j) ∈ 1) : IntegralLattice V

A symmetric rational form that is integral on basis vectors defines an integral lattice.

The carrier is the ℤ-span of the basis. Bilinearity propagates the integral-value hypothesis from basis vectors to their integral span.

Equations

• TauCeti.IntegralLattice.ofBasis b B hB hint = { carrier := Submodule.span ℤ (Set.range ⇑b), form := B, isLattice := ⋯, isSymm := hB, le_dual := ⋯ }

@[simp]

theorem TauCeti.IntegralLattice.ofBasis_carrier {V : Type u} [AddCommGroup V] [Module ℚ V] {ι : Type u_1} [Finite ι] (b : Module.Basis ι ℚ V) (B : LinearMap.BilinForm ℚ V) (hB : B.IsSymm) (hint : ∀ (i j : ι), (B (b i)) (b j) ∈ 1) : (ofBasis b B hB hint).carrier = Submodule.span ℤ (Set.range ⇑b)

@[simp]

theorem TauCeti.IntegralLattice.ofBasis_form {V : Type u} [AddCommGroup V] [Module ℚ V] {ι : Type u_1} [Finite ι] (b : Module.Basis ι ℚ V) (B : LinearMap.BilinForm ℚ V) (hB : B.IsSymm) (hint : ∀ (i j : ι), (B (b i)) (b j) ∈ 1) : (ofBasis b B hB hint).form = B

noncomputable def TauCeti.IntegralLattice.ofBasis.basis {V : Type u} [AddCommGroup V] [Module ℚ V] {ι : Type u_1} [Finite ι] (b : Module.Basis ι ℚ V) (B : LinearMap.BilinForm ℚ V) (hB : B.IsSymm) (hint : ∀ (i j : ι), (B (b i)) (b j) ∈ 1) : Module.Basis ι ℤ ↥(ofBasis b B hB hint).carrier

The canonical carrier basis of ofBasis b B hB hint induced by b.

Equations

• TauCeti.IntegralLattice.ofBasis.basis b B hB hint = Module.Basis.restrictScalars ℤ b

@[simp]

theorem TauCeti.IntegralLattice.ofBasis.coe_basis {V : Type u} [AddCommGroup V] [Module ℚ V] {ι : Type u_1} [Finite ι] (b : Module.Basis ι ℚ V) (B : LinearMap.BilinForm ℚ V) (hB : B.IsSymm) (hint : ∀ (i j : ι), (B (b i)) (b j) ∈ 1) (i : ι) : ↑((basis b B hB hint) i) = b i

noncomputable def TauCeti.IntegralLattice.ofGramMatrix {V : Type u} [AddCommGroup V] [Module ℚ V] {ι : Type u_1} [Fintype ι] (b : Module.Basis ι ℚ V) (G : Matrix ι ι ℤ) (hG : G.IsSymm) : IntegralLattice V

Construct an integral lattice from a finite rational basis and an integral symmetric Gram matrix.

Equations

• TauCeti.IntegralLattice.ofGramMatrix b G hG = TauCeti.IntegralLattice.ofBasis b ((Matrix.toBilin b) (G.map ⇑(algebraMap ℤ ℚ))) ⋯ ⋯

@[simp]

theorem TauCeti.IntegralLattice.ofGramMatrix_carrier {V : Type u} [AddCommGroup V] [Module ℚ V] {ι : Type u_1} [Fintype ι] (b : Module.Basis ι ℚ V) (G : Matrix ι ι ℤ) (hG : G.IsSymm) : (ofGramMatrix b G hG).carrier = Submodule.span ℤ (Set.range ⇑b)

@[simp]

theorem TauCeti.IntegralLattice.ofGramMatrix_form {V : Type u} [AddCommGroup V] [Module ℚ V] {ι : Type u_1} [Fintype ι] (b : Module.Basis ι ℚ V) (G : Matrix ι ι ℤ) (hG : G.IsSymm) : (ofGramMatrix b G hG).form = (Matrix.toBilin b) (G.map ⇑(algebraMap ℤ ℚ))

noncomputable def TauCeti.IntegralLattice.ofGramMatrix.basis {V : Type u} [AddCommGroup V] [Module ℚ V] {ι : Type u_1} [Fintype ι] (b : Module.Basis ι ℚ V) (G : Matrix ι ι ℤ) (hG : G.IsSymm) : Module.Basis ι ℤ ↥(ofGramMatrix b G hG).carrier

The canonical carrier basis of ofGramMatrix b G hG induced by b.

Equations

• TauCeti.IntegralLattice.ofGramMatrix.basis b G hG = Module.Basis.restrictScalars ℤ b

@[simp]

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

@[simp]

theorem TauCeti.IntegralLattice.integralForm_ofGramMatrix_apply {V : Type u} [AddCommGroup V] [Module ℚ V] {ι : Type u_1} [Fintype ι] (b : Module.Basis ι ℚ V) (G : Matrix ι ι ℤ) (hG : G.IsSymm) (i j : ι) : ((ofGramMatrix b G hG).integralForm ((ofGramMatrix.basis b G hG) i)) ((ofGramMatrix.basis b G hG) j) = G i j

Evaluating the induced integral form of ofGramMatrix on embedded basis vectors recovers the corresponding entry of the Gram matrix.