The quotient represented by the modular F₄ short-root action #

The adjoint action on the twenty-six-dimensional short-root ideal detects the ambient modular Chevalley Lie algebra modulo the short-root ideal. Consequently, the quotient by that ideal is linearly equivalent to the represented range modulo the image of the ideal.

source

theorem TauCeti.DynkinType.ker_f4ShortRootAdjoint_le_f4ShortRootSubspace :

(↑f4ShortRootAdjoint).ker ≤ f4ShortRootSubspace

The kernel of the adjoint action on the modular short-root ideal is contained in that ideal.

source

@[reducible, inline]

noncomputable abbrev TauCeti.DynkinType.f4ShortRootRepresentedRange :

Submodule (ZMod 2) (Module.End (ZMod 2) ↥f4ShortRootLieIdeal)

The range of the modular short-root adjoint action.

Equations