The order of the automorphism group of the E₈ root system

The automorphism group of the pinned root datum of type E₈ has order 240 · 126 · 23040 = 696729600.

The count runs along the chain of pointwise stabilizers of the Bourbaki simple roots α₁, …, α₈. Write H k for the subgroup fixing α₁, …, α_k, so that H 0 is the whole group and H 8 is trivial, an automorphism fixing a base being the identity. By orbit and stabilizer, |H k| = |H k · α_{k+1}| · |H (k + 1)|, and the orbit H k · α_{k+1} is the set of roots having the same pairings with α₁, …, α_k as α_{k+1}. The orbit sizes are 240, 126, 32, 6, 5, 4, 3, 2. In particular the group is transitive on the 240 roots, the stabilizer of α₁ is transitive on the 126 roots orthogonal to it, and the pointwise stabilizer of the orthogonal pair α₁, α₂ has order 32 · 6 · 5 · 4 · 3 · 2 = 2⁵ · 6! = 23040. These are the orders of the Weyl groups of types E₇ and D₆, the classical identifications of the two stabilizers, which the count does not need.

That every root β with the right pairings lies in the orbit is the content of the count. If two such roots β and γ pair to 1, then β - γ is a root orthogonal to α₁, …, α_k, and the reflection in it fixes α₁, …, α_k and exchanges β and γ. A finite computation checks that every such β other than α_{k+1} pairs to 1 with such a root γ whose pairing with α_{k+1} is strictly larger, so induction on that pairing reaches α_{k+1}.

Main results

• TauCeti.DynkinType.card_aut_e8SimplyConnectedRootDatum: the automorphism group of the pinned E₈ datum has order 696729600.
• TauCeti.DynkinType.card_weylGroup_e8SimplyConnectedRootDatum: so does its Weyl group.
• TauCeti.DynkinType.isPretransitive_aut_e8SimplyConnectedRootDatum: it acts transitively on the 240 roots.

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.

Orbits through reflections

The chain of stabilizers

The order

theorem TauCeti.DynkinType.card_aut_e8SimplyConnectedRootDatum : Nat.card (RootPairing.Aut e8SimplyConnectedRootDatum) = 696729600

The automorphism group of the pinned E₈ root datum has order 240 · 126 · 23040 = 696729600.

theorem TauCeti.DynkinType.card_weylGroup_e8SimplyConnectedRootDatum : Nat.card ↥(RootPairing.weylGroup e8SimplyConnectedRootDatum) = 696729600

The Weyl group of the pinned E₈ root datum has order 696729600: it is the whole automorphism group, the E₈ diagram having no nontrivial symmetry.

instance TauCeti.DynkinType.isPretransitive_aut_e8SimplyConnectedRootDatum : MulAction.IsPretransitive (RootPairing.Aut e8SimplyConnectedRootDatum) (Fin 240)

The automorphism group of the pinned E₈ root datum acts transitively on the 240 roots.