Integral matrices of doubled minuscule E₆ generators

The numbered root operators on V(ϖ₁) ⊕ V(ϖ₆) preserve its two summands. This file records that property in the carrier's Fin 54 coordinates, obtained by matrixIndexEquiv from the block coordinates. Each root operator squares to zero, so the corresponding root subgroup is 1 + t X over any commutative ring. These formulas allow block preservation to be checked on the universal root-subgroup coordinate maps, including over nonreduced rings.

The integral matrix interface follows TauCeti.Algebra.Lie.Orthogonal.TypeB.SpinCarrier.IntegralMatrix.

References

• J. C. Jantzen, Representations of Algebraic Groups, II.1–2.
• R. W. Carter, Simple Groups of Lie Type, §12.2.

def TauCeti.E6DoubledMinuscule.matrixSummand (a : Fin 54) : ℤ

The summand label of a matrix coordinate: zero for V(ϖ₁), one for V(ϖ₆).

Equations

• TauCeti.E6DoubledMinuscule.matrixSummand a = if (TauCeti.E6DoubledMinuscule.matrixIndexEquiv.symm a).isRight = true then 1 else 0

@[simp]

theorem TauCeti.E6DoubledMinuscule.matrixSummand_inl (a : Fin 27) : matrixSummand (matrixIndexEquiv (Sum.inl a)) = 0

Coordinates of the first minuscule summand have label zero.

@[simp]

theorem TauCeti.E6DoubledMinuscule.matrixSummand_inr (a : Fin 27) : matrixSummand (matrixIndexEquiv (Sum.inr a)) = 1

Coordinates of the dual minuscule summand have label one.

@[simp]

theorem TauCeti.E6DoubledMinuscule.matrixSummand_reflection (i : Fin 6) (a : Fin 54) : matrixSummand (matrixIndexEquiv ((reflection i) (matrixIndexEquiv.symm a))) = matrixSummand a

A simple reflection preserves the minuscule summand label.

noncomputable def TauCeti.E6DoubledMinuscule.rootIntMatrix (j : Fin 6 ⊕ Fin 6) : Matrix (Fin 54) (Fin 54) ℤ

The integral matrix of a numbered simple root operator in the carrier's lattice basis.

Equations

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

theorem TauCeti.E6DoubledMinuscule.rep_rootGenerator_matrixBasis_eq_sum (j : Fin 6 ⊕ Fin 6) (s : Fin 54) : (rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator (CartanMatrix.E 6).transpose j))) ↑(matrixBasis s) = ∑ r : Fin 54, rootIntMatrix j r s • ↑(matrixBasis r)

A represented root operator acts on a lattice basis vector by its integral matrix column.

theorem TauCeti.E6DoubledMinuscule.nilpotencyClass_rep_rootGenerator_le_two (j : Fin 6 ⊕ Fin 6) : nilpotencyClass (rep ((UniversalEnvelopingAlgebra.ι ℚ) (serreRootGenerator (CartanMatrix.E 6).transpose j))) ≤ 2

Numbered root operators have nilpotency class at most two on the doubled module.

@[simp]

theorem TauCeti.E6DoubledMinuscule.rootIntMatrix_apply (j : Fin 6 ⊕ Fin 6) (a b : Fin 54) : rootIntMatrix j a b = if a = matrixIndexEquiv ((reflection (Sum.elim id id j)) (matrixIndexEquiv.symm b)) then if matrixWeight b (Sum.elim id id j) = Sum.elim (fun (x : Fin 6) => -1) (fun (x : Fin 6) => 1) j then summandSign (matrixIndexEquiv.symm b) else 0 else 0

A numbered root operator moves a coordinate to its simple reflection, with coefficient 1 on the minuscule block and -1 on the dual block, when its weight permits the move.

theorem TauCeti.E6DoubledMinuscule.rootIntMatrix_eq_zero_of_summand_ne (j : Fin 6 ⊕ Fin 6) {a b : Fin 54} (hab : matrixSummand a ≠ matrixSummand b) : rootIntMatrix j a b = 0

The root-operator matrices have zero entries between distinct minuscule summands.

theorem TauCeti.E6DoubledMinuscule.coe_rootSubgroupPoints_eq_one_add_smul (j : Fin 6 ⊕ Fin 6) (A : Type u_1) [CommRing A] (u : Multiplicative A) : ↑↑((rootSubgroupPoints j A) u) = 1 + Multiplicative.toAdd u • (rootIntMatrix j).map Int.cast

A numbered root subgroup is 1 + t X for its integral root-operator matrix.