The roots and kissing number of the integral E₈ lattice

The norm-two shell of typeE₈RootLattice consists of exactly 240 vectors, and its kissing number is 240. The equivalence typeE₈RootEquiv identifies this actual lattice shell with the indices of the existing Bourbaki root enumeration. It supplies both explicit vectors and exhaustion, so computations on the roots can use finite indices without replacing the lattice by a separate coordinate model.

The enumeration DynkinType.e8Coroot is expressed in the simple-coroot basis. In the simply laced type E₈ these are also simple-root coordinates, and the integral Cartan norm agrees with the rational norm of the lattice. We reuse DynkinType.exists_e8Coroot_eq for completeness rather than recounting the Euclidean roots.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate VII.
• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, Chapter 4, §8.

noncomputable def TauCeti.IntegralLattice.typeE₈RootVector (i : Fin 240) : ↥typeE₈RootLattice.carrier

The i-th root of the integral E₈ lattice, in the existing Bourbaki enumeration.

@[simp]

theorem TauCeti.IntegralLattice.typeE₈RootVector_apply (i : Fin 240) (j : Fin 8) : ↑(typeE₈RootVector i) j = ↑(DynkinType.e8Coroot i j)

The coordinates of a root vector are those of the existing simple-coroot enumeration.

@[simp]

theorem TauCeti.IntegralLattice.norm_typeE₈RootVector (i : Fin 240) : typeE₈RootLattice.norm ↑(typeE₈RootVector i) = 2

Every enumerated E₈ root has norm two.

@[simp]

theorem TauCeti.IntegralLattice.integralNorm_typeE₈RootVector (i : Fin 240) : typeE₈RootLattice.integralNorm (typeE₈RootVector i) = 2

Every enumerated E₈ root has integral norm two, so it defines a root reflection.

@[simp]

theorem TauCeti.IntegralLattice.typeE₈RootVector_e8SimpleIndex (i : Fin 8) : ↑(typeE₈RootVector (DynkinType.e8SimpleIndex i)) = typeE₈SimpleRoot i

The Bourbaki simple-root indices give the simple roots of the integral lattice.

theorem TauCeti.IntegralLattice.typeE₈RootVector_injective : Function.Injective typeE₈RootVector

Distinct root indices give distinct lattice vectors.

theorem TauCeti.IntegralLattice.norm_typeE₈RootLattice_eq_two_iff (x : ↥typeE₈RootLattice.carrier) : typeE₈RootLattice.norm ↑x = 2 ↔ ∃ (i : Fin 240), typeE₈RootVector i = x

A lattice vector has norm two exactly when it is one of the enumerated E₈ roots.

noncomputable def TauCeti.IntegralLattice.typeE₈RootEquiv : Fin 240 ≃ ↑(typeE₈RootLattice.vectorsOfNorm 2)

The 240 root indices enumerate the actual norm-two shell of the integral E₈ lattice.

@[simp]

theorem TauCeti.IntegralLattice.typeE₈RootEquiv_apply (i : Fin 240) : ↑(typeE₈RootEquiv i) = typeE₈RootVector i

The shell equivalence sends each index to its enumerated root vector.

@[simp]

theorem TauCeti.IntegralLattice.representationNumber_typeE₈RootLattice_two : typeE₈RootLattice.representationNumber 2 = 240

The integral E₈ lattice has exactly 240 vectors of norm two.

@[simp]

theorem TauCeti.IntegralLattice.kissingNumber_typeE₈RootLattice : typeE₈RootLattice.kissingNumber = 240

The kissing number of the integral E₈ lattice is 240.