The modular F4 short-root action matrix

This file identifies the structurally constructed adjoint action on the modular short-root ideal with the existing sparse twenty-six-dimensional root matrices.

References

• R. Steinberg, Endomorphisms of linear algebraic groups, Memoirs AMS 80 (1968), §11.
• R. W. Carter, Simple Groups of Lie Type, §§4.2 and 12.3.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate VIII, for the root coordinates and the simple-root numbering.

def TauCeti.DynkinType.f4SimpleRootTarget : Fin 4 ⊕ Fin 4 → Fin 26 → Fin 26

The target of the unique possibly nonzero entry in a simple-root matrix column.

Equations

• TauCeti.DynkinType.f4SimpleRootTarget (Sum.inl i) = TauCeti.F4ShortRoot.raisingTarget i
• TauCeti.DynkinType.f4SimpleRootTarget (Sum.inr i) = TauCeti.F4ShortRoot.loweringTarget i

@[simp]

theorem TauCeti.DynkinType.f4SimpleRootTarget_inl (i : Fin 4) (b : Fin 26) : f4SimpleRootTarget (Sum.inl i) b = F4ShortRoot.raisingTarget i b

@[simp]

theorem TauCeti.DynkinType.f4SimpleRootTarget_inr (i : Fin 4) (b : Fin 26) : f4SimpleRootTarget (Sum.inr i) b = F4ShortRoot.loweringTarget i b

def TauCeti.DynkinType.f4SimpleRootCoeff : Fin 4 ⊕ Fin 4 → Fin 26 → ℤ

The integral coefficient of the unique possibly nonzero entry in a simple-root matrix column.

Equations

• TauCeti.DynkinType.f4SimpleRootCoeff (Sum.inl i) = TauCeti.F4ShortRoot.raisingCoeff i
• TauCeti.DynkinType.f4SimpleRootCoeff (Sum.inr i) = TauCeti.F4ShortRoot.loweringCoeff i

@[simp]

theorem TauCeti.DynkinType.f4SimpleRootCoeff_inl (i : Fin 4) (b : Fin 26) : f4SimpleRootCoeff (Sum.inl i) b = F4ShortRoot.raisingCoeff i b

@[simp]

theorem TauCeti.DynkinType.f4SimpleRootCoeff_inr (i : Fin 4) (b : Fin 26) : f4SimpleRootCoeff (Sum.inr i) b = F4ShortRoot.loweringCoeff i b

@[simp]

theorem TauCeti.DynkinType.rootMatrix_apply (k : Fin 4 ⊕ Fin 4) (a b : Fin 26) : F4ShortRoot.rootMatrix k a b = if a = f4SimpleRootTarget k b then f4SimpleRootCoeff k b else 0

Each simple-root matrix column is supported on the single entry named by f4SimpleRootTarget, where it carries the coefficient named by f4SimpleRootCoeff.

@[simp]

theorem TauCeti.DynkinType.f4ShortRootSignedSimpleAdjointMatrix_eq_rootMatrix_map (k : Fin 4 ⊕ Fin 4) : f4ShortRootSignedSimpleAdjointMatrix k = (F4ShortRoot.rootMatrix k).map Int.cast

The structural adjoint action on the modular short-root ideal is the reduction modulo two of the original sparse root matrix.