The integral minuscule representation of type E7

This file realizes the Chevalley generators of type E₇ on the fifty-six-element weight diagram TauCeti.DynkinType.e7MinusculeWeight. On the coordinate vector belonging to a weight lambda, the Cartan generator H_i acts by the simple-coroot coordinate lambda_i; the raising generator E_i carries lambda to its simple reflection when lambda_i = -1; and the lowering generator F_i makes the reverse move when lambda_i = 1.

The resulting integer matrices satisfy the Chevalley--Serre relations for the Bourbaki Cartan matrix. The universal property of the Serre presentation gives the explicit integral fifty-six-dimensional minuscule representation. Each raising and lowering matrix squares to zero. See TauCeti.Algebra.Lie.E7.Minuscule.AdmissibleLattice for the rational extension and the admissibility of its coordinate lattice.

No identification with the abstract irreducible highest-weight module is asserted here. The construction is explicit: every matrix entry is read from the already audited weight and reflection tables.

Main definitions

• TauCeti.E7Minuscule.cartanMatrix, raisingMatrix, and loweringMatrix: the integral Cartan, raising, and lowering matrices.
• TauCeti.E7Minuscule.isSl2Triple: the three matrices at a simple node form an sl₂ triple.
• TauCeti.E7Minuscule.isSerreSystem: the Chevalley--Serre relations between them over ℤ.
• TauCeti.E7Minuscule.serreRepresentation: the induced representation of the type-E₇ Serre Lie algebra.

References

The numbering and weight diagram follow Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate VI. The minuscule action follows J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §13.4, and J. C. Jantzen, Representations of Algebraic Groups, II.2.

This advances the explicit Chevalley--Demazure construction in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md. Its consumer is milestone L0 of TauCetiRoadmap/CFSGStatement/README.md, which needs an explicit simply connected type-E₇ carrier.

The weight table

def TauCeti.E7Minuscule.weightTable : MinusculeWeightTable (Fin 7) (Fin 56)

The fifty-six minuscule weights of type E₇, as a minuscule weight table.

Equations

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

@[simp]

theorem TauCeti.E7Minuscule.weightTable_cartanMatrix : weightTable.cartanMatrix = CartanMatrix.E 7

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

@[simp]

theorem TauCeti.E7Minuscule.weightTable_weight : weightTable.weight = DynkinType.e7MinusculeWeight

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

@[simp]

theorem TauCeti.E7Minuscule.weightTable_reflection (i : Fin 7) : weightTable.reflection i = ⇑(DynkinType.e7MinusculeReflection i)

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

The integral generator matrices

def TauCeti.E7Minuscule.cartanMatrix (i : Fin 7) : Matrix (Fin 56) (Fin 56) ℤ

The Cartan generator H_i in the minuscule weight basis.

Equations

• TauCeti.E7Minuscule.cartanMatrix i = TauCeti.E7Minuscule.weightTable.cartanGeneratorMatrix i

def TauCeti.E7Minuscule.raisingMatrix (i : Fin 7) : Matrix (Fin 56) (Fin 56) ℤ

The raising generator E_i in the minuscule weight basis.

Equations

• TauCeti.E7Minuscule.raisingMatrix i = TauCeti.E7Minuscule.weightTable.raisingMatrix i

def TauCeti.E7Minuscule.loweringMatrix (i : Fin 7) : Matrix (Fin 56) (Fin 56) ℤ

The lowering generator F_i in the minuscule weight basis.

Equations

• TauCeti.E7Minuscule.loweringMatrix i = TauCeti.E7Minuscule.weightTable.loweringMatrix i

@[simp]

theorem TauCeti.E7Minuscule.cartanMatrix_apply (i : Fin 7) (a b : Fin 56) : cartanMatrix i a b = if a = b then DynkinType.e7MinusculeWeight a i else 0

The entrywise formula for the diagonal Cartan generator matrix.

@[simp]

theorem TauCeti.E7Minuscule.raisingMatrix_apply (i : Fin 7) (a b : Fin 56) : raisingMatrix i a b = if DynkinType.e7MinusculeWeight b i = -1 ∧ a = (DynkinType.e7MinusculeReflection i) b then 1 else 0

The entrywise formula for the raising generator matrix.

@[simp]

theorem TauCeti.E7Minuscule.loweringMatrix_apply (i : Fin 7) (a b : Fin 56) : loweringMatrix i a b = if DynkinType.e7MinusculeWeight b i = 1 ∧ a = (DynkinType.e7MinusculeReflection i) b then 1 else 0

The entrywise formula for the lowering generator matrix.

Chevalley--Serre relations

theorem TauCeti.E7Minuscule.isSl2Triple (i : Fin 7) : IsSl2Triple (cartanMatrix i) (raisingMatrix i) (loweringMatrix i)

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

theorem TauCeti.E7Minuscule.isSerreSystem : IsSerreSystem ℤ (CartanMatrix.E 7) cartanMatrix raisingMatrix loweringMatrix

The integral minuscule generator matrices satisfy the Chevalley--Serre relations of type E₇, in Bourbaki numbering.

noncomputable def TauCeti.E7Minuscule.serreRepresentation : Matrix.ToLieAlgebra ℤ (CartanMatrix.E 7) →ₗ⁅ℤ⁆ Matrix (Fin 56) (Fin 56) ℤ

The explicit integral fifty-six-dimensional representation of the type-E₇ Serre Lie algebra.

Equations

• TauCeti.E7Minuscule.serreRepresentation = TauCeti.E7Minuscule.weightTable.serreRepresentation

@[simp]

theorem TauCeti.E7Minuscule.serreRepresentation_serreH (i : Fin 7) : serreRepresentation (serreH ℤ (CartanMatrix.E 7) i) = cartanMatrix i

The integral Serre representation sends H_i to the Cartan generator matrix.

@[simp]

theorem TauCeti.E7Minuscule.serreRepresentation_serreE (i : Fin 7) : serreRepresentation (serreE ℤ (CartanMatrix.E 7) i) = raisingMatrix i

The integral Serre representation sends E_i to the raising generator matrix.

@[simp]

theorem TauCeti.E7Minuscule.serreRepresentation_serreF (i : Fin 7) : serreRepresentation (serreF ℤ (CartanMatrix.E 7) i) = loweringMatrix i

The integral Serre representation sends F_i to the lowering generator matrix.

@[simp]

theorem TauCeti.E7Minuscule.raisingMatrix_mul_self (i : Fin 7) : raisingMatrix i * raisingMatrix i = 0

Every minuscule raising generator squares to zero.

@[simp]

theorem TauCeti.E7Minuscule.loweringMatrix_mul_self (i : Fin 7) : loweringMatrix i * loweringMatrix i = 0

Every minuscule lowering generator squares to zero.