The isometry group of the E₈ lattice is its Weyl group, of order 696729600

Every isometry of the integral E₈ lattice typeE₈RootLattice is a product of reflections in its 240 roots: TauCeti.IntegralLattice.weylGroup_typeE₈RootLattice_eq_top says that the Weyl group of the lattice is its whole isometry group O(E₈). In particular -1 is a product of root reflections.

The proof passes through the pinned E₈ root datum TauCeti.DynkinType.e8SimplyConnectedRootDatum. Since the E₈ lattice is unimodular, the map sending a lattice vector to its pairings with the simple roots identifies the lattice with the weight lattice of the datum, carrying the enumerated lattice roots TauCeti.IntegralLattice.typeE₈RootVector to the roots of the datum. Transport along this identification is a group isomorphism TauCeti.IntegralLattice.typeE₈IsometryEquivAut from O(E₈) onto the automorphism group of the datum, sending the reflection in a lattice root to the reflection of the datum in the same root. Its surjectivity and the equality of the two Weyl groups with the full groups both come from the rigidity of the E₈ diagram: every automorphism of a root system of type E₈ lies in its Weyl group (TauCeti.weylGroup_eq_top_of_hasCartanType_E8).

The same isomorphism transports the order of the automorphism group of the datum, TauCeti.DynkinType.card_aut_e8SimplyConnectedRootDatum, and its transitivity on the roots, so |O(E₈)| = |W(E₈)| = 240 · 126 · 23040 = 696729600.

Main definitions

• TauCeti.IntegralLattice.typeE₈IsometryEquivAut: the isomorphism from the isometry group of the E₈ lattice onto the automorphism group of the pinned E₈ root datum.

Main results

• TauCeti.IntegralLattice.typeE₈RootVector_typeE₈IsometryEquivAut_indexEquiv: the isomorphism permutes the root indices as the isometry permutes the lattice roots.
• TauCeti.IntegralLattice.typeE₈IsometryEquivAut_rootReflection: it sends root reflections to root reflections.
• TauCeti.IntegralLattice.weylGroup_typeE₈RootLattice_eq_top: the root reflections generate the isometry group of the E₈ lattice.
• TauCeti.IntegralLattice.neg_mem_weylGroup_typeE₈RootLattice: -1 lies in the Weyl group of the E₈ lattice.
• TauCeti.IntegralLattice.exists_carrierEquiv_typeE₈RootVector_eq: the isometry group acts transitively on the 240 roots.
• TauCeti.IntegralLattice.card_isometry_typeE₈RootLattice and TauCeti.IntegralLattice.card_weylGroup_typeE₈RootLattice: |O(E₈)| = |W(E₈)| = 696729600.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Ch. VI, §4.10 and Plate VII.
• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, Chapter 4, §8.1.
• W. Ebeling, Lattices and Codes, Chapter 1, §1.4.

The weight lattice of the pinned datum

Isometries as automorphisms of the datum

noncomputable def TauCeti.IntegralLattice.typeE₈IsometryEquivAut : typeE₈RootLattice.Isometry typeE₈RootLattice ≃* RootPairing.Aut DynkinType.e8SimplyConnectedRootDatum

The isometry group of the E₈ lattice is the automorphism group of the pinned E₈ root datum. An isometry acts on the weight lattice of the datum through the identification of the lattice with the weight lattice by pairing with the simple roots.

@[simp]

theorem TauCeti.IntegralLattice.typeE₈RootVector_typeE₈IsometryEquivAut_indexEquiv (g : typeE₈RootLattice.Isometry typeE₈RootLattice) (i : Fin 240) : typeE₈RootVector ((↑(typeE₈IsometryEquivAut g)).indexEquiv i) = g.carrierEquiv (typeE₈RootVector i)

The isomorphism permutes the root indices as the isometry permutes the lattice roots. This characterizes it, since an automorphism of a root system is determined by its permutation of the roots.

@[simp]

theorem TauCeti.IntegralLattice.typeE₈IsometryEquivAut_rootReflection (i : Fin 240) : typeE₈IsometryEquivAut (rootReflection (typeE₈RootVector i) ⋯) = RootPairing.Equiv.reflection DynkinType.e8SimplyConnectedRootDatum i

The isomorphism sends the reflection in a lattice root to the reflection of the datum in the same root.

The isometry group is generated by root reflections

@[simp]

theorem TauCeti.IntegralLattice.weylGroup_typeE₈RootLattice_eq_top : typeE₈RootLattice.weylGroup = ⊤

The reflections in the 240 roots generate the isometry group of the E₈ lattice: its Weyl group is the whole of O(E₈).

theorem TauCeti.IntegralLattice.neg_mem_weylGroup_typeE₈RootLattice : Isometry.neg typeE₈RootLattice ∈ typeE₈RootLattice.weylGroup

-1 is a product of reflections in roots of the E₈ lattice.

The order of the isometry group

theorem TauCeti.IntegralLattice.exists_carrierEquiv_typeE₈RootVector_eq (i j : Fin 240) : ∃ (g : typeE₈RootLattice.Isometry typeE₈RootLattice), g.carrierEquiv (typeE₈RootVector i) = typeE₈RootVector j

The isometry group of the E₈ lattice acts transitively on its 240 roots.

theorem TauCeti.IntegralLattice.card_isometry_typeE₈RootLattice : Nat.card (typeE₈RootLattice.Isometry typeE₈RootLattice) = 696729600

The isometry group of the E₈ lattice has order 240 · 126 · 23040 = 696729600.

theorem TauCeti.IntegralLattice.card_weylGroup_typeE₈RootLattice : Nat.card ↥typeE₈RootLattice.weylGroup = 696729600

The Weyl group of the E₈ lattice has order 696729600.