The simply connected root datum of type E₆

This file constructs the pinned integral root datum of type E₆ on the character and cocharacter lattices Fin 6 → ℤ. The character lattice is written in the fundamental-weight basis and the cocharacter lattice in the simple-coroot basis, so that the i-th simple root is the i-th row of the Bourbaki-numbered Cartan matrix CartanMatrix.E 6 and the i-th simple coroot is the i-th standard basis vector.

The coordinates

A coroot is stored by its coordinates in the simple coroots, and the corresponding root by its pairings against the simple coroots. Because E₆ is simply laced, a root and its coroot have the same simple-root coordinates, so a single stored vector determines both: if a coroot has coordinates c, then the root has coordinates ⟨β, αⱼ^∨⟩ = ∑ i, cᵢ ⟨αᵢ, αⱼ^∨⟩, that is, the Cartan-matrix image of c. That relation is TauCeti.DynkinType.e6Root_eq_mulVec, and it is what makes every later step structural rather than a second table: the root reflections are the image of the coroot reflections under a linear map, and the pairing is symmetric because CartanMatrix.E 6 is.

The seventy-two roots — the count fixed by TauCeti.DynkinType.numRoots — are ordered with the six simple roots first, in Bourbaki order, then the remaining thirty positive roots by height and then lexicographically in their simple-root coordinates, and finally the thirty-six negative roots in the matching order. The last positive root is therefore the highest root, whose simple-root coordinates are the Bourbaki marks (1, 2, 2, 3, 2, 1).

Only the coroots are asked to span their lattice, and only that half is recorded, in TauCeti.DynkinType.corootSpan_e6SimplyConnectedRootDatum_eq_top. The roots span the root lattice, which sits inside the weight lattice with index 3 — the determinant of CartanMatrix.E 6 — so the datum carries no RootPairing.IsRootSystem instance. That asymmetry is what "simply connected" means here.

Main definitions

• TauCeti.DynkinType.e6Coroot and TauCeti.DynkinType.e6Root: the coroot coordinate embedding and the root embedding derived from it by the Cartan-matrix map.
• TauCeti.DynkinType.e6SimplyConnectedRootDatum: the pinned root datum of type E₆.
• TauCeti.DynkinType.e6SimpleIndex: the first six root indices, the Bourbaki-numbered simple roots.
• TauCeti.DynkinType.e6SimplyConnectedBase: the base they form.

Main results

• TauCeti.DynkinType.e6Root_eq_mulVec: the root coordinates are the Cartan-matrix image of the coroot coordinates.
• TauCeti.DynkinType.root_e6SimpleIndex and TauCeti.DynkinType.coroot_e6SimpleIndex: the i-th simple root is the i-th row of CartanMatrix.E 6 and the i-th simple coroot is Pi.single i 1, which is what pins the two lattices as the weight and coroot lattices.
• TauCeti.DynkinType.hasCartanType_e6SimplyConnectedRootDatum: the pinned base has Cartan type E6.
• TauCeti.DynkinType.corootSpan_e6SimplyConnectedRootDatum_eq_top: the coroots span the cocharacter lattice, the simply connected condition.

References

The coordinates and the node numbering follow Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate V, and Humphreys, Introduction to Lie Algebras and Representation Theory, section 12.1. This is the E₆ branch of the target "a named datum per valid type" in Layer 6 of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md.

The coordinate data

def TauCeti.DynkinType.e6Coroot : Fin 72 ↪ Fin 6 → ℤ

The coroots of type E₆ in the simple-coroot basis. The first six are the standard basis vectors, the first thirty-six are the positive coroots, and the last thirty-six are their negatives.

Equations

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

def TauCeti.DynkinType.e6Root : Fin 72 ↪ Fin 6 → ℤ

The roots of type E₆ in the fundamental-weight basis, ordered compatibly with TauCeti.DynkinType.e6Coroot. They are derived from the coroot coordinates by the Cartan-matrix map, and the first six are the rows of CartanMatrix.E 6.

Equations

• TauCeti.DynkinType.e6Root = { toFun := fun (i : Fin 72) => (CartanMatrix.E 6).mulVec (TauCeti.DynkinType.e6Coroot i), inj' := TauCeti.DynkinType.e6Root._proof_1✝ }

The three blocks of root indices

def TauCeti.DynkinType.e6SimpleIndex (i : Fin 6) : Fin 72

The i-th simple root of type E₆ sits at root index i, the Bourbaki node i + 1.

Equations

• TauCeti.DynkinType.e6SimpleIndex i = Fin.castAdd 66 i

def TauCeti.DynkinType.e6PositiveIndex (i : Fin 36) : Fin 72

The i-th positive root of type E₆ sits at root index i.

Equations

• TauCeti.DynkinType.e6PositiveIndex i = Fin.castAdd 36 i

def TauCeti.DynkinType.e6NegativeIndex (i : Fin 36) : Fin 72

The negative of the i-th positive root of type E₆ sits at root index i + 36.

Equations

• TauCeti.DynkinType.e6NegativeIndex i = i.addNat 36

@[simp]

theorem TauCeti.DynkinType.e6SimpleIndex_val (i : Fin 6) : ↑(e6SimpleIndex i) = ↑i

@[simp]

theorem TauCeti.DynkinType.e6PositiveIndex_val (i : Fin 36) : ↑(e6PositiveIndex i) = ↑i

@[simp]

theorem TauCeti.DynkinType.e6NegativeIndex_val (i : Fin 36) : ↑(e6NegativeIndex i) = ↑i + 36

theorem TauCeti.DynkinType.e6SimpleIndex_injective : Function.Injective e6SimpleIndex

The Cartan matrix as the bridge between the two embeddings

theorem TauCeti.DynkinType.e6Root_eq_mulVec (j : Fin 72) : e6Root j = (CartanMatrix.E 6).mulVec (e6Coroot j)

The root coordinates are the Cartan-matrix image of the coroot coordinates. Writing a coroot as β^∨ = ∑ i, cᵢ αᵢ^∨ in the simple coroots, the pairings of β against the simple coroots are ⟨β, αⱼ^∨⟩ = ∑ i, cᵢ ⟨αᵢ, αⱼ^∨⟩, which is the j-th entry of the Cartan-matrix image of c because CartanMatrix.E 6 is symmetric.

This is deliberately not a simp lemma: unfolding a root into the Cartan-matrix image of its coroot is a change of representation, not a normal form, and it would take the left-hand sides of the lemmas below out of normal form.

@[simp]

theorem TauCeti.DynkinType.coroot_e6SimpleIndex (i : Fin 6) : e6Coroot (e6SimpleIndex i) = Pi.single i 1

The simple coroots are the standard basis. This is what pins the cocharacter lattice as the coroot lattice, so that the datum is the simply connected one.

@[simp]

theorem TauCeti.DynkinType.root_e6SimpleIndex (i : Fin 6) : e6Root (e6SimpleIndex i) = CartanMatrix.E 6 i

The simple roots are the rows of the Cartan matrix. In the fundamental-weight basis the i-th simple root of the pinned type E₆ datum is the i-th row of CartanMatrix.E 6, which is what pins the character lattice as the weight lattice.

theorem TauCeti.DynkinType.e6Root_dotProduct_e6Coroot_comm (i j : Fin 72) : e6Root i ⬝ᵥ e6Coroot j = e6Root j ⬝ᵥ e6Coroot i

The pairing of the pinned tables is symmetric. This is the simply-laced feature of E₆: the pairing is the symmetric bilinear form attached to CartanMatrix.E 6, read on the shared simple-root coordinates of a root and its coroot.

@[simp]

theorem TauCeti.DynkinType.e6Coroot_e6NegativeIndex (i : Fin 36) : e6Coroot (e6NegativeIndex i) = -e6Coroot (e6PositiveIndex i)

The second half of the table lists the negatives of the coroots in the first half.

@[simp]

theorem TauCeti.DynkinType.e6Root_e6NegativeIndex (i : Fin 36) : e6Root (e6NegativeIndex i) = -e6Root (e6PositiveIndex i)

The second half of the table lists the negatives of the roots in the first half.

@[simp]

theorem TauCeti.DynkinType.e6Root_dotProduct_e6Coroot_self (i : Fin 72) : e6Root i ⬝ᵥ e6Coroot i = 2

Each root pairs with its own coroot to 2.

The reflections

The pinned datum

def TauCeti.DynkinType.e6SimplyConnectedRootDatum : RootDatum (Fin 72) (Fin 6 → ℤ) (Fin 6 → ℤ)

The pinned simply connected root datum of type E₆.

Both lattices are Fin 6 → ℤ: the character lattice in the fundamental-weight basis and the cocharacter lattice in the simple-coroot basis. Root indices 0 through 5 are the Bourbaki simple roots; see TauCeti.DynkinType.root_e6SimpleIndex.

Equations

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

@[simp]

theorem TauCeti.DynkinType.e6SimplyConnectedRootDatum_root : e6SimplyConnectedRootDatum.root = e6Root

The root embedding of the pinned E₆ datum is the explicit table e6Root.

@[simp]

theorem TauCeti.DynkinType.e6SimplyConnectedRootDatum_coroot : e6SimplyConnectedRootDatum.coroot = e6Coroot

The coroot embedding of the pinned E₆ datum is the explicit table e6Coroot.

@[simp]

theorem TauCeti.DynkinType.e6SimplyConnectedRootDatum_toLinearMap (x y : Fin 6 → ℤ) : (e6SimplyConnectedRootDatum.toLinearMap x) y = x ⬝ᵥ y

The perfect pairing of the pinned E₆ datum is the dot product of coordinate vectors, the fundamental-weight and simple-coroot bases being dual to one another.

@[simp]

theorem TauCeti.DynkinType.e6SimplyConnectedRootDatum_pairing (i j : Fin 72) : RootPairing.pairing e6SimplyConnectedRootDatum i j = e6Root i ⬝ᵥ e6Coroot j

Pairing a pinned E₆ root with a coroot computes as their coordinate dot product.

theorem TauCeti.DynkinType.corootSpan_e6SimplyConnectedRootDatum_eq_top : RootPairing.corootSpan e6SimplyConnectedRootDatum ℤ = ⊤

The coroots of the pinned type E₆ datum span the cocharacter lattice. This is the simply connected lattice condition required by the pinned Chevalley--Demazure construction. Its counterpart for the roots is deliberately absent: they span the root lattice, which sits inside the weight lattice with index 3 (Bourbaki, Plate V).

The pinned base

def TauCeti.DynkinType.e6SimplyConnectedBase : RootPairing.Base e6SimplyConnectedRootDatum

The Bourbaki-numbered base of the pinned simply connected root datum of type E₆. Its support is the set of the first six root indices, carrying the simple roots in Bourbaki order.

Equations

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

@[simp]

theorem TauCeti.DynkinType.mem_e6SimplyConnectedBase_support {k : Fin 72} : k ∈ e6SimplyConnectedBase.support ↔ ↑k < 6

Membership in the pinned base support is exactly membership among the first six root indices.

theorem TauCeti.DynkinType.pairing_e6SimpleIndex (i j : Fin 6) : RootPairing.pairing e6SimplyConnectedRootDatum (e6SimpleIndex i) (e6SimpleIndex j) = CartanMatrix.E 6 i j

The Cartan integers at the first six root indices are Mathlib's Bourbaki-numbered E₆ matrix. This pins the node order independently of the existential relabelling in TauCeti.HasCartanType.

theorem TauCeti.DynkinType.hasCartanType_e6SimplyConnectedRootDatum : HasCartanType e6SimplyConnectedRootDatum e6SimplyConnectedBase E6

The pinned datum of type E₆ has Cartan type E6. Its Bourbaki-numbered base realizes the standard Cartan matrix CartanMatrix.E 6, with the node numbering of TauCeti.DynkinType.