Gram-matrix lattices on the standard rational coordinate space

An integral symmetric matrix G indexed by a finite type ι presents an integral lattice on ι → ℚ, namely ofGramMatrix (Pi.basisFun ℚ ι) G hG, whose carrier is the standard integral lattice ι → ℤ and whose form is ⟨x, y⟩ = ∑ᵢⱼ xᵢ Gᵢⱼ yⱼ. This is how a Cartan matrix presents a root lattice, the standard coordinate vectors playing the role of the simple roots.

This file expands the form, the carrier and the dual carrier of such a lattice in coordinates. The dual carrier is described by the row combinations of G: a vector is dual-integral exactly when G *ᵥ x is an integer vector, which is what makes the discriminant group of a lattice given by a Cartan matrix computable from that matrix alone.

Main declarations

• TauCeti.IntegralLattice.form_ofGramMatrix_basisFun_apply: the form in coordinates.
• TauCeti.IntegralLattice.form_ofGramMatrix_basisFun_right: pairing against a standard coordinate vector is the corresponding row combination of G.
• TauCeti.IntegralLattice.form_ofGramMatrix_basisFun_basisFun: the Gram matrix of the standard coordinate basis is G.
• TauCeti.IntegralLattice.mem_ofGramMatrix_basisFun_carrier_iff: the carrier is ℤⁿ.
• TauCeti.IntegralLattice.mem_ofGramMatrix_basisFun_dualCarrier_iff: the dual carrier consists of the vectors whose row combinations against G are integers.

References

• TauCetiRoadmap/IntegralLattices/README.md, Layer 5.

theorem TauCeti.IntegralLattice.form_ofGramMatrix_basisFun_apply {ι : Type u_1} [Fintype ι] (G : Matrix ι ι ℤ) (hG : G.IsSymm) (x y : ι → ℚ) : ((ofGramMatrix (Pi.basisFun ℚ ι) G hG).form x) y = ∑ i : ι, x i * ∑ j : ι, ↑(G i j) * y j

The form of the lattice presented by G on ι → ℚ, expanded in coordinates.

theorem TauCeti.IntegralLattice.form_ofGramMatrix_basisFun_right {ι : Type u_1} [Fintype ι] (G : Matrix ι ι ℤ) (hG : G.IsSymm) (x : ι → ℚ) (i : ι) : ((ofGramMatrix (Pi.basisFun ℚ ι) G hG).form x) ((Pi.basisFun ℚ ι) i) = ∑ j : ι, ↑(G i j) * x j

Pairing an arbitrary vector against the i-th standard coordinate vector collapses the double sum to the i-th row combination of the Gram matrix.

theorem TauCeti.IntegralLattice.form_ofGramMatrix_basisFun_basisFun {ι : Type u_1} [Fintype ι] (G : Matrix ι ι ℤ) (hG : G.IsSymm) (i j : ι) : ((ofGramMatrix (Pi.basisFun ℚ ι) G hG).form ((Pi.basisFun ℚ ι) i)) ((Pi.basisFun ℚ ι) j) = ↑(G i j)

The Gram matrix of a Gram-matrix lattice in its standard coordinate basis is the given matrix.

theorem TauCeti.IntegralLattice.mem_ofGramMatrix_basisFun_carrier_iff {ι : Type u_1} [Fintype ι] (G : Matrix ι ι ℤ) (hG : G.IsSymm) (x : ι → ℚ) : x ∈ (ofGramMatrix (Pi.basisFun ℚ ι) G hG).carrier ↔ ∀ (i : ι), ∃ (z : ℤ), ↑z = x i

A vector belongs to a Gram-matrix lattice exactly when all of its standard coordinates are integers.

@[simp]

theorem TauCeti.IntegralLattice.mem_ofGramMatrix_basisFun_dualCarrier_iff {ι : Type u_1} [Fintype ι] (G : Matrix ι ι ℤ) (hG : G.IsSymm) (x : ι → ℚ) : x ∈ (ofGramMatrix (Pi.basisFun ℚ ι) G hG).dualCarrier ↔ ∀ (i : ι), ∃ (z : ℤ), ↑z = ∑ j : ι, ↑(G i j) * x j

A vector belongs to the dual of a Gram-matrix lattice exactly when every row combination of the Gram matrix against it is an integer.