The integral roots of type E7

This file enumerates the 126 roots of type E7 in the lattices used by the pinned simply connected root datum constructed in TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.E7.Datum. Coroots are expressed in the simple-coroot basis and roots in the fundamental-weight basis. The first seven entries are the Bourbaki simple roots; the remaining positive roots are ordered by height, followed by their negatives. Completeness of the table among the norm-two vectors is proved in TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.E7.Lattice.

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 VI.

def TauCeti.DynkinType.e7PositiveCoroot (i : Fin 63) : Fin 7 → ℤ

The 63 positive E7 coroots in the simple-coroot basis, ordered by height.

Equations

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

def TauCeti.DynkinType.e7Coroot : Fin 126 ↪ Fin 7 → ℤ

The 126 E7 coroots in the simple-coroot basis, with positive roots followed by negatives.

Equations

• TauCeti.DynkinType.e7Coroot = Fin.Embedding.append TauCeti.DynkinType.e7Coroot_disjoint✝

theorem TauCeti.DynkinType.e7Coroot_apply (i : Fin 126) : e7Coroot i = if hi : ↑i < 63 then e7PositiveCoroot ⟨↑i, hi⟩ else -e7PositiveCoroot ⟨↑i - 63, ⋯⟩

Evaluate an E7 coroot through the exposed table of positive coroots.

def TauCeti.DynkinType.e7Root : Fin 126 ↪ Fin 7 → ℤ

The 126 E7 roots in the fundamental-weight basis.

Equations

• TauCeti.DynkinType.e7Root = { toFun := fun (i : Fin 126) => Matrix.vecMul (TauCeti.DynkinType.e7Coroot i) (CartanMatrix.E 7), inj' := TauCeti.DynkinType.e7Root._proof_1✝ }

theorem TauCeti.DynkinType.e7Root_apply (i : Fin 126) : e7Root i = Matrix.vecMul (e7Coroot i) (CartanMatrix.E 7)

Each E7 root is the E7 Cartan matrix applied to the corresponding coroot.

theorem TauCeti.DynkinType.e7Root_eq_mulVec (i : Fin 126) : e7Root i = (CartanMatrix.E 7).mulVec (e7Coroot i)

The E7 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.e7Coroot_addNat (i : Fin 63) : e7Coroot (i.addNat 63) = -e7Coroot (Fin.castAdd 63 i)

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

@[simp]

theorem TauCeti.DynkinType.e7Root_addNat (i : Fin 63) : e7Root (i.addNat 63) = -e7Root (Fin.castAdd 63 i)

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

@[simp]

theorem TauCeti.DynkinType.e7Root_dotProduct_coroot (i : Fin 126) : e7Root i ⬝ᵥ e7Coroot i = 2

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

def TauCeti.DynkinType.e7SimpleIndex (i : Fin 7) : Fin 126

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

Equations

• TauCeti.DynkinType.e7SimpleIndex i = Fin.castAdd 119 i

@[simp]

theorem TauCeti.DynkinType.e7SimpleIndex_val (i : Fin 7) : ↑(e7SimpleIndex i) = ↑i

theorem TauCeti.DynkinType.e7SimpleIndex_injective : Function.Injective e7SimpleIndex

@[simp]

theorem TauCeti.DynkinType.coroot_e7SimpleIndex (i : Fin 7) : e7Coroot (e7SimpleIndex i) = Pi.single i 1

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

@[simp]

theorem TauCeti.DynkinType.root_e7SimpleIndex (i : Fin 7) : e7Root (e7SimpleIndex i) = CartanMatrix.E 7 i

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

theorem TauCeti.DynkinType.e7Coroot_nonneg (i : Fin 63) (j : Fin 7) : 0 ≤ e7Coroot (Fin.castAdd 63 i) j

Every positive E7 coroot has nonnegative simple-coroot coordinates.

@[simp]

theorem TauCeti.DynkinType.e7Coroot_apply_62 : e7Coroot 62 = ![2, 2, 3, 4, 3, 2, 1]

The last positive entry of the coroot table has the Bourbaki marks (2, 2, 3, 4, 3, 2, 1).

@[simp]

theorem TauCeti.DynkinType.e7Root_apply_62 : e7Root 62 = ![1, 0, 0, 0, 0, 0, 0]

The last positive entry of the root table has fundamental-weight coordinates (1, 0, 0, 0, 0, 0, 0).

theorem TauCeti.DynkinType.e7Coroot_le_apply_62 (i : Fin 126) (j : Fin 7) : e7Coroot i j ≤ e7Coroot 62 j

The last positive entry is the highest E7 coroot: it dominates every entry of the table in each simple-coroot coordinate.