Centralizers of the short-root vectors in modular type F₄

The main result, mem_f4ShortRootSubspace_of_forall_lie_rootVector_eq_zero, shows that an element of the modular Chevalley algebra bracketing to zero with every short-root vector lies in the short-root subspace. Thus the kernel of the adjoint action on the short-root ideal is contained in the ideal, as needed for the quotient construction.

The coordinate lemmas detect long-root and Cartan components from brackets with short-root vectors; together they give the centralizer inclusion above.

References

• R. Steinberg, Endomorphisms of linear algebraic groups, Memoirs AMS 80 (1968), §11.
• R. W. Carter, Simple Groups of Lie Type, §12.3.

theorem TauCeti.DynkinType.mem_f4ShortRootSubspace_of_forall_lie_rootVector_eq_zero (X : f4ModularChevalleyLieAlgebra) (hcentral : ∀ (β : Fin 48), f4Length β = 1 → ⁅X, f4ModularRootVector β⁆ = 0) : X ∈ f4ShortRootSubspace

A modular Chevalley vector that centralizes every short root vector belongs to the short-root coordinate subspace.