A 27-dimensional representation of the type-E6 Serre presentation

This file constructs a 27-dimensional representation of the type-E₆ Serre presentation. The coordinate basis is indexed by the Weyl orbit of the first fundamental weight enumerated by TauCeti.DynkinType.e6MinusculeWeight.

For a simple root i, the raising matrix sends the basis vector of weight μ to the basis vector of weight μ + αᵢ when ⟨μ, αᵢ∨⟩ = -1, and to zero otherwise. The lowering matrix is defined dually. The Cartan generator acts diagonally by the simple-coroot coordinate of the weight. These integral matrices satisfy the Serre relations for the transposed type-E₆ Cartan matrix. Identifying this presentation with the split semisimple Lie algebra of type E₆, and hence interpreting these matrices as a representation of that algebra, remains downstream.

This is the representation-theoretic input for the full-weight type-E₆ Chevalley--Demazure carrier required by Layer 9 of the ReductiveGroups roadmap. The weights span the full character lattice by TauCeti.DynkinType.span_range_e6MinusculeWeight_eq_top; constructing the associated Kostant carrier and its group scheme remains downstream.

Main declarations

• TauCeti.E6Minuscule.raisingMatrix, loweringMatrix, and cartanGeneratorMatrix: the integral Chevalley generators on the minuscule weight basis.
• TauCeti.E6Minuscule.weightTable: the minuscule weight table the construction reads, with weightTable_cartanMatrix, weightTable_weight and weightTable_reflection evaluating its three data fields.
• TauCeti.E6Minuscule.isSerreSystem: the generators satisfy the type-E₆ Serre relations.
• TauCeti.E6Minuscule.serreRepresentation: the induced homomorphism from the integral type-E₆ Serre presentation.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate V.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §§13.4 and 27.
• J. C. Jantzen, Representations of Algebraic Groups, II.2.

The weight table

def TauCeti.E6Minuscule.weightTable : MinusculeWeightTable (Fin 6) (Fin 27)

The twenty-seven minuscule weights of type E₆, as a minuscule weight table. The Cartan matrix is transposed, which is the convention placing the coroot index first.

Equations

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

@[simp]

theorem TauCeti.E6Minuscule.weightTable_cartanMatrix : weightTable.cartanMatrix = (CartanMatrix.E 6).transpose

The Cartan matrix of the type-E₆ minuscule weight table is the transposed E₆ Cartan matrix.

@[simp]

theorem TauCeti.E6Minuscule.weightTable_weight : weightTable.weight = DynkinType.e6MinusculeWeight

The weights of the type-E₆ minuscule weight table are the minuscule weights.

@[simp]

theorem TauCeti.E6Minuscule.weightTable_reflection (i : Fin 6) : weightTable.reflection i = ⇑(DynkinType.e6MinusculeReflection i)

The simple reflections of the type-E₆ minuscule weight table are the minuscule reflections.

@[simp]

theorem TauCeti.E6Minuscule.e6MinusculeWeight_reflection_apply_self (i : Fin 6) (a : Fin 27) : DynkinType.e6MinusculeWeight ((DynkinType.e6MinusculeReflection i) a) i = -DynkinType.e6MinusculeWeight a i

Reflection in a simple root negates the corresponding simple-coroot coordinate of a minuscule weight.

The Chevalley generators

def TauCeti.E6Minuscule.raisingMatrix (i : Fin 6) : Matrix (Fin 27) (Fin 27) ℤ

The raising matrix of the i-th simple root on the integral minuscule weight basis.

Equations

• TauCeti.E6Minuscule.raisingMatrix i = TauCeti.E6Minuscule.weightTable.raisingMatrix i

def TauCeti.E6Minuscule.loweringMatrix (i : Fin 6) : Matrix (Fin 27) (Fin 27) ℤ

The lowering matrix of the i-th simple root on the integral minuscule weight basis.

Equations

• TauCeti.E6Minuscule.loweringMatrix i = TauCeti.E6Minuscule.weightTable.loweringMatrix i

def TauCeti.E6Minuscule.cartanGeneratorMatrix (i : Fin 6) : Matrix (Fin 27) (Fin 27) ℤ

The diagonal matrix of the i-th simple coroot on the integral minuscule weight basis.

Equations

• TauCeti.E6Minuscule.cartanGeneratorMatrix i = TauCeti.E6Minuscule.weightTable.cartanGeneratorMatrix i

@[simp]

theorem TauCeti.E6Minuscule.raisingMatrix_apply (i : Fin 6) (a b : Fin 27) : raisingMatrix i a b = if DynkinType.e6MinusculeWeight b i = -1 ∧ a = (DynkinType.e6MinusculeReflection i) b then 1 else 0

The entry formula for a simple raising matrix.

@[simp]

theorem TauCeti.E6Minuscule.loweringMatrix_apply (i : Fin 6) (a b : Fin 27) : loweringMatrix i a b = if DynkinType.e6MinusculeWeight b i = 1 ∧ a = (DynkinType.e6MinusculeReflection i) b then 1 else 0

The entry formula for a simple lowering matrix.

@[simp]

theorem TauCeti.E6Minuscule.cartanGeneratorMatrix_apply (i : Fin 6) (a b : Fin 27) : cartanGeneratorMatrix i a b = if a = b then DynkinType.e6MinusculeWeight b i else 0

The entry formula for a simple Cartan generator matrix.

@[simp]

theorem TauCeti.E6Minuscule.raisingMatrix_pow_two (i : Fin 6) : raisingMatrix i ^ 2 = 0

Every raising matrix of the minuscule weight table squares to zero.

@[simp]

theorem TauCeti.E6Minuscule.loweringMatrix_pow_two (i : Fin 6) : loweringMatrix i ^ 2 = 0

Every lowering matrix of the minuscule weight table squares to zero.

The Serre relations

theorem TauCeti.E6Minuscule.isSl2Triple (i : Fin 6) : IsSl2Triple (cartanGeneratorMatrix i) (raisingMatrix i) (loweringMatrix i)

At each simple node, the three integral minuscule matrices form an sl₂ triple.

theorem TauCeti.E6Minuscule.isSerreSystem : IsSerreSystem ℤ (CartanMatrix.E 6).transpose cartanGeneratorMatrix raisingMatrix loweringMatrix

The integral 27-dimensional minuscule matrices satisfy the Serre relations of type E₆. The transpose is the convention in which the coroot index precedes the root index.

noncomputable def TauCeti.E6Minuscule.serreRepresentation : Matrix.ToLieAlgebra ℤ (CartanMatrix.E 6).transpose →ₗ⁅ℤ⁆ Matrix (Fin 27) (Fin 27) ℤ

The integral 27-dimensional minuscule representation of the type-E₆ Serre presentation.

Equations

• TauCeti.E6Minuscule.serreRepresentation = TauCeti.E6Minuscule.weightTable.serreRepresentation

@[simp]

theorem TauCeti.E6Minuscule.serreRepresentation_serreH (i : Fin 6) : serreRepresentation (serreH ℤ (CartanMatrix.E 6).transpose i) = cartanGeneratorMatrix i

The minuscule representation sends a Cartan generator to its diagonal weight matrix.

@[simp]

theorem TauCeti.E6Minuscule.serreRepresentation_serreE (i : Fin 6) : serreRepresentation (serreE ℤ (CartanMatrix.E 6).transpose i) = raisingMatrix i

The minuscule representation sends a positive generator to its raising matrix.

@[simp]

theorem TauCeti.E6Minuscule.serreRepresentation_serreF (i : Fin 6) : serreRepresentation (serreF ℤ (CartanMatrix.E 6).transpose i) = loweringMatrix i

The minuscule representation sends a negative generator to its lowering matrix.