The integral roots of type E8

This file enumerates the 240 roots of type E8 in the lattices used by the pinned simply connected root datum, which is built from these tables in TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.E8.Datum; that the enumeration below misses no root is proved in TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.E8.Lattice. Coroots are expressed in the simple-coroot basis and roots in the fundamental-weight basis. Both tables are indexed by the same Fin 240: the first eight entries of the root table are the Bourbaki simple roots and the first eight entries of the coroot table are the corresponding simple coroots. The remaining positive entries are ordered by height, and the last 120 entries are the negatives of the first 120.

The enumeration is the root-data input for Layer 6 of the root-systems roadmap. It follows Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate VII.

def TauCeti.DynkinType.e8PositiveCoroot : Fin 120 ↪ Fin 8 → ℤ

The 120 positive E8 coroots in the simple-coroot basis. The first eight entries are the Bourbaki simple coroots and the rest are ordered by height.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.DynkinType.card_filter_e8PositiveCoroot_last_eq_zero : {i : Fin 120 | e8PositiveCoroot i 7 = 0}.card = 63

There are 63 positive E₈ coroots in the principal E₇ subsystem, characterized by having zero final simple-coroot coordinate.

theorem TauCeti.DynkinType.e8PositiveCoroot_nonneg (i : Fin 120) (j : Fin 8) : 0 ≤ e8PositiveCoroot i j

Every positive E8 coroot has nonnegative simple-coroot coordinates.

def TauCeti.DynkinType.e8Coroot : Fin 240 ↪ Fin 8 → ℤ

The 240 E8 coroots in the simple-coroot basis, with the positive coroots followed by their negatives.

Equations

• TauCeti.DynkinType.e8Coroot = Fin.Embedding.append TauCeti.DynkinType.e8PositiveCoroot_range_disjoint✝

def TauCeti.DynkinType.e8Root : Fin 240 ↪ Fin 8 → ℤ

The 240 E8 roots in the fundamental-weight basis.

Equations

• TauCeti.DynkinType.e8Root = { toFun := fun (i : Fin 240) => Matrix.vecMul (TauCeti.DynkinType.e8Coroot i) (CartanMatrix.E 8), inj' := TauCeti.DynkinType.e8Root._proof_1✝ }

theorem TauCeti.DynkinType.e8Root_apply (i : Fin 240) : e8Root i = Matrix.vecMul (e8Coroot i) (CartanMatrix.E 8)

The E8 roots are obtained from the coroot coordinates using the Cartan matrix.

theorem TauCeti.DynkinType.e8Root_eq_mulVec (i : Fin 240) : e8Root i = (CartanMatrix.E 8).mulVec (e8Coroot i)

The E8 roots are the images of the coroots under the Cartan matrix, read on the left or, equivalently, on the right, the matrix being symmetric.

@[simp]

theorem TauCeti.DynkinType.e8Coroot_castAdd (i : Fin 120) : e8Coroot (Fin.castAdd 120 i) = e8PositiveCoroot i

The first half of the coroot table is the positive coroot enumeration.

@[simp]

theorem TauCeti.DynkinType.e8Coroot_addNat (i : Fin 120) : e8Coroot (i.addNat 120) = -e8PositiveCoroot i

The negative half of the coroot table is the negation of the positive half.

@[simp]

theorem TauCeti.DynkinType.e8Root_addNat (i : Fin 120) : e8Root (i.addNat 120) = -e8Root (Fin.castAdd 120 i)

The negative half of the root table is the negation of the positive half.

@[simp]

theorem TauCeti.DynkinType.e8Root_dotProduct_coroot (i : Fin 240) : e8Root i ⬝ᵥ e8Coroot i = 2

Every listed E8 root pairs to two with its corresponding coroot.

def TauCeti.DynkinType.e8SimpleIndex (i : Fin 8) : Fin 240

The index of the i-th Bourbaki simple root in the pinned E₈ enumeration.

Equations

• TauCeti.DynkinType.e8SimpleIndex i = Fin.castAdd 232 i

@[simp]

theorem TauCeti.DynkinType.e8SimpleIndex_val (i : Fin 8) : ↑(e8SimpleIndex i) = ↑i

theorem TauCeti.DynkinType.e8SimpleIndex_injective : Function.Injective e8SimpleIndex

@[simp]

theorem TauCeti.DynkinType.root_e8SimpleIndex (i : Fin 8) : e8Root (e8SimpleIndex i) = CartanMatrix.E 8 i

The simple roots of the pinned E₈ datum are the rows of the Bourbaki Cartan matrix.

@[simp]

theorem TauCeti.DynkinType.coroot_e8SimpleIndex (i : Fin 8) : e8Coroot (e8SimpleIndex i) = Pi.single i 1

The simple coroots of the pinned E₈ datum are the standard basis vectors.

theorem TauCeti.DynkinType.e8Coroot_apply_last_positive : e8Coroot 119 = ![2, 3, 4, 6, 5, 4, 3, 2]

The last positive E8 coroot has Bourbaki marks (2, 3, 4, 6, 5, 4, 3, 2).