The doubled minuscule representation of type E6

The nontrivial diagram automorphism of type E₆ exchanges the minuscule representations V(ϖ₁) and V(ϖ₆) = V(ϖ₁)ˣ. Consequently the 27-dimensional carrier alone does not admit the pinned diagram symmetry. This file constructs the graph-stable direct sum V(ϖ₁) ⊕ V(ϖ₆) over ℤ.

The first block is TauCeti.E6Minuscule.serreRepresentation. The second is its contragredient: the Cartan matrices are negated and the raising and lowering matrices are exchanged and negated. The resulting 54-dimensional block matrices satisfy the type-E₆ Serre relations and have the weights TauCeti.DynkinType.e6DoubledMinusculeWeight.

This is the representation input for the graph-stable full-weight type-E₆ Chevalley--Demazure carrier required by Layer 9 of the ReductiveGroups roadmap.

Main declarations

• TauCeti.E6DoubledMinuscule.serreRepresentation: the integral doubled minuscule representation.
• TauCeti.E6DoubledMinuscule.cartanGeneratorMatrix, raisingMatrix, and loweringMatrix: its block-diagonal Chevalley generators.
• TauCeti.E6DoubledMinuscule.isSerreSystem: these generators satisfy the type-E₆ Serre relations.

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.
• R. W. Carter, Simple Groups of Lie Type, §12.2.

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

The integral Cartan generators on V(ϖ₁) ⊕ V(ϖ₆).

Equations

• TauCeti.E6DoubledMinuscule.cartanGeneratorMatrix i = Matrix.fromBlocks (TauCeti.E6Minuscule.cartanGeneratorMatrix i) 0 0 (-TauCeti.E6Minuscule.cartanGeneratorMatrix i)

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

The integral raising matrices on V(ϖ₁) ⊕ V(ϖ₆).

Equations

• TauCeti.E6DoubledMinuscule.raisingMatrix i = Matrix.fromBlocks (TauCeti.E6Minuscule.raisingMatrix i) 0 0 (-TauCeti.E6Minuscule.loweringMatrix i)

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

The integral lowering matrices on V(ϖ₁) ⊕ V(ϖ₆).

Equations

• TauCeti.E6DoubledMinuscule.loweringMatrix i = Matrix.fromBlocks (TauCeti.E6Minuscule.loweringMatrix i) 0 0 (-TauCeti.E6Minuscule.raisingMatrix i)

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

The integral 54-dimensional representation V(ϖ₁) ⊕ V(ϖ₆) of the type-E₆ Serre presentation.

Equations

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

@[simp]

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

The doubled representation sends a Cartan generator to its block-diagonal Cartan matrix.

@[simp]

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

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

@[simp]

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

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

@[simp]

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

Every raising matrix of the doubled minuscule representation squares to zero, each of its two diagonal blocks doing so.

@[simp]

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

Every lowering matrix of the doubled minuscule representation squares to zero, each of its two diagonal blocks doing so.

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

The integral doubled minuscule matrices satisfy the type-E₆ Serre relations.

def TauCeti.E6DoubledMinuscule.reflection (i : Fin 6) : Equiv.Perm (Fin 27 ⊕ Fin 27)

The simple reflection on the doubled weight basis, preserving each minuscule summand.

Equations

• TauCeti.E6DoubledMinuscule.reflection i = Equiv.sumCongr (TauCeti.DynkinType.e6MinusculeReflection i) (TauCeti.DynkinType.e6MinusculeReflection i)

@[simp]

theorem TauCeti.E6DoubledMinuscule.reflection_inl (i : Fin 6) (a : Fin 27) : (reflection i) (Sum.inl a) = Sum.inl ((DynkinType.e6MinusculeReflection i) a)

A simple reflection acts on the V(ϖ₁) block by the minuscule reflection.

@[simp]

theorem TauCeti.E6DoubledMinuscule.reflection_inr (i : Fin 6) (a : Fin 27) : (reflection i) (Sum.inr a) = Sum.inr ((DynkinType.e6MinusculeReflection i) a)

A simple reflection acts on the V(ϖ₆) block by the minuscule reflection.

@[simp]

theorem TauCeti.E6DoubledMinuscule.e6DoubledMinusculeWeight_reflection_apply_self (i : Fin 6) (a : Fin 27 ⊕ Fin 27) : DynkinType.e6DoubledMinusculeWeight ((reflection i) a) i = -DynkinType.e6DoubledMinusculeWeight a i

A simple reflection negates the corresponding simple-coroot coordinate of every doubled minuscule weight.

@[simp]

theorem TauCeti.E6DoubledMinuscule.reflection_apply_apply (i : Fin 6) (a : Fin 27 ⊕ Fin 27) : (reflection i) ((reflection i) a) = a

Every simple reflection on the doubled minuscule basis is an involution.

def TauCeti.E6DoubledMinuscule.summandSign : Fin 27 ⊕ Fin 27 → ℤ

The sign of the Chevalley root-matrix coefficient on each minuscule summand. The dual block has the negative structure constants.

Equations

• TauCeti.E6DoubledMinuscule.summandSign (Sum.inl val) = 1
• TauCeti.E6DoubledMinuscule.summandSign (Sum.inr val) = -1

@[simp]

theorem TauCeti.E6DoubledMinuscule.summandSign_inl (a : Fin 27) : summandSign (Sum.inl a) = 1

The structure constants of the V(ϖ₁) block are those of the minuscule representation.

@[simp]

theorem TauCeti.E6DoubledMinuscule.summandSign_inr (a : Fin 27) : summandSign (Sum.inr a) = -1

The structure constants of the V(ϖ₆) block are the negatives of the minuscule ones.

@[simp]

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

The Cartan generators are diagonal with the doubled minuscule weights on the diagonal.

@[simp]

theorem TauCeti.E6DoubledMinuscule.raisingMatrix_apply (i : Fin 6) (a b : Fin 27 ⊕ Fin 27) : raisingMatrix i a b = if DynkinType.e6DoubledMinusculeWeight b i = -1 ∧ a = (reflection i) b then summandSign b else 0

Entry formula for a simple raising matrix on the doubled minuscule basis.

@[simp]

theorem TauCeti.E6DoubledMinuscule.loweringMatrix_apply (i : Fin 6) (a b : Fin 27 ⊕ Fin 27) : loweringMatrix i a b = if DynkinType.e6DoubledMinusculeWeight b i = 1 ∧ a = (reflection i) b then summandSign b else 0

Entry formula for a simple lowering matrix on the doubled minuscule basis.