Ranks of positive definite even unimodular lattices

An even unimodular positive definite integral lattice exists in rank n precisely when eight divides n. The obstruction is Milgram's signature congruence (TauCeti.IntegralLattice.eight_dvd_finrank_of_isEven_isUnimodular_isPosDef). For existence, the Gram matrix of k orthogonal copies of the E₈ root lattice is the Kronecker product of the identity matrix of size k with the E₈ Cartan matrix. This construction includes the rank-zero lattice.

The coordinates on Fin (8 * k) are reindexed by finProdFinEquiv, so the E₈ blocks are explicitly indexed by Fin k × Fin 8. The resulting lattice is a concrete witness on Fin n → ℚ.

Main results

• TauCeti.IntegralLattice.e8PowLattice: the lattice E₈^k of k orthogonal E₈ blocks, with its block Gram matrix and standard integral carrier; it is even, unimodular and positive definite.
• TauCeti.IntegralLattice.span_vectorsOfNorm_two_e8PowLattice: the roots of E₈^k span it.
• TauCeti.IntegralLattice.exists_isEven_isUnimodular_isPosDef_iff: a positive definite even unimodular lattice on Fin n → ℚ exists exactly when 8 ∣ n.
• TauCeti.IntegralLattice.eight_dvd_finrank_of_isEven_isUnimodular_isPosDef: the rank of any positive definite even unimodular integral lattice is divisible by eight.

References

• J. Milnor and D. Husemoller, Symmetric Bilinear Forms, Appendix 4.
• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, Chapter 4.

def TauCeti.IntegralLattice.e8PowIndexEquiv (k : ℕ) : Fin (8 * k) ≃ Fin k × Fin 8

The coordinate equivalence identifying Fin (8 * k) with k blocks of eight coordinates.

noncomputable def TauCeti.IntegralLattice.e8PowLattice (k : ℕ) : IntegralLattice (Fin (8 * k) → ℚ)

The lattice E₈^k: k orthogonal copies of the E₈ root lattice, as an integral lattice of rank 8 * k on Fin (8 * k) → ℚ. Its Gram matrix is 1 ⊗ₖ E₈ up to reindexing.

theorem TauCeti.IntegralLattice.isEven_e8PowLattice (k : ℕ) : (e8PowLattice k).IsEven

The lattice E₈^k is even.

theorem TauCeti.IntegralLattice.isUnimodular_e8PowLattice (k : ℕ) : (e8PowLattice k).IsUnimodular

The lattice E₈^k is unimodular.

theorem TauCeti.IntegralLattice.isPosDef_e8PowLattice (k : ℕ) : (e8PowLattice k).IsPosDef

The lattice E₈^k is positive definite.

@[simp]

theorem TauCeti.IntegralLattice.finrank_e8PowLattice (k : ℕ) : Module.finrank ℤ ↥(e8PowLattice k).carrier = 8 * k

The rank of E₈^k is 8k.

@[simp]

theorem TauCeti.IntegralLattice.form_e8PowLattice_basisFun (k : ℕ) (a b : Fin k) (i j : Fin 8) : ((e8PowLattice k).form (Pi.single ((e8PowIndexEquiv k).symm (a, i)) 1)) (Pi.single ((e8PowIndexEquiv k).symm (b, j)) 1) = if a = b then ↑(CartanMatrix.E 8 i j) else 0

The Gram matrix of E₈^k on the basis indexed by Fin k × Fin 8 is block diagonal, with each diagonal block the E₈ Cartan matrix.

theorem TauCeti.IntegralLattice.e8PowLattice_carrier (k : ℕ) : (e8PowLattice k).carrier = Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℚ (Fin (8 * k))))

The carrier of E₈^k is the integral span of its standard basis.

@[simp]

theorem TauCeti.IntegralLattice.mem_e8PowLattice_carrier_iff (k : ℕ) (x : Fin (8 * k) → ℚ) : x ∈ (e8PowLattice k).carrier ↔ ∀ (i : Fin (8 * k)), ∃ (z : ℤ), ↑z = x i

A vector belongs to E₈^k exactly when all its standard coordinates are integers.

theorem TauCeti.IntegralLattice.span_vectorsOfNorm_two_e8PowLattice (k : ℕ) : Submodule.span ℤ ((e8PowLattice k).vectorsOfNorm 2) = ⊤

The roots of E₈^k span it. The standard basis vectors are the simple roots of the E₈ blocks, of norm two, and they span the carrier.

theorem TauCeti.IntegralLattice.exists_isEven_isUnimodular_isPosDef_iff (n : ℕ) : (∃ (L : IntegralLattice (Fin n → ℚ)), L.IsEven ∧ L.IsUnimodular ∧ L.IsPosDef) ↔ 8 ∣ n

Positive definite even unimodular lattices exist exactly in ranks divisible by eight. The witness at rank 8 * k is e8PowLattice k.