Reductivity of the short-root F₄ carrier over 𝔽₂

The short-root type-F₄ carrier over 𝔽₂ is the closed subgroup scheme of GL₂₆ generated over 𝔽₂ by eight numbered root subgroups and a rank-four weight torus. Since every 𝔽₂-algebra is free as an 𝔽₂-module, the formation of generated subgroups commutes with scalar extension (TauCeti.CommHopfAlgCat.baseChangeHopfIdeal_commonKernelHopfIdeal). Thus the scalar extension of the carrier to any commutative 𝔽₂-algebra is the subgroup generated by the scalar-extended root subgroups and torus, and the properties already proved for that generated subgroup over an algebraically closed field transfer to the carrier itself; in particular the carrier is geometrically connected (TauCeti.F4ShortRoot.PrimeField.geometricallyConnectedCommHopfAlgProperty_quotient_definingIdeal).

Combining this with smoothness of the carrier and simplicity of its twenty-six-dimensional standard representation shows that the carrier is a reductive group over 𝔽₂: it is smooth and geometrically connected, and its geometric unipotent radical is trivial because a normal smooth unipotent subgroup acts trivially on the faithful simple standard representation.

The carrier is not identified here with the pinned simply connected group scheme of type F₄; constructions on it transfer to that group only along such an identification.

Main declarations

In the namespace TauCeti.F4ShortRoot.PrimeField:

• unipotentRadicalDefiningIdeal_baseChange_eq_augmentation: over an algebraically closed field of characteristic two, the unipotent radical of the scalar-extended carrier is trivial.
• reductiveCommHopfAlgProperty_finiteTypeCoordinateHopfAlgebra: the carrier is reductive.

References

• J. S. Milne, Algebraic Groups (2017), §2.h and Chapter 19.
• J. E. Humphreys, Linear Algebraic Groups, §§19 and 26.
• J. C. Jantzen, Representations of Algebraic Groups, I.2 and II.2.

The radical argument follows TauCeti.Algebra.Lie.G2.ShortRoot.PrimeField.Generated.UnipotentRadical.

theorem TauCeti.F4ShortRoot.PrimeField.unipotentRadicalDefiningIdeal_baseChange_eq_augmentation (k : Type u) [Field k] [Algebra (ZMod 2) k] [IsAlgClosed k] : finiteTypeCoordinateHopfAlgebra.baseChange.unipotentRadicalDefiningIdeal = HopfIdeal.augmentation k ↑finiteTypeCoordinateHopfAlgebra.baseChange.obj

The unipotent radical of the scalar-extended short-root type-F₄ carrier is trivial, over every algebraically closed field of characteristic two.

theorem TauCeti.F4ShortRoot.PrimeField.reductiveCommHopfAlgProperty_finiteTypeCoordinateHopfAlgebra : reductiveCommHopfAlgProperty (ZMod 2) finiteTypeCoordinateHopfAlgebra

The short-root type-F₄ carrier over 𝔽₂ is reductive: it is smooth and geometrically connected, and its geometric unipotent radical is trivial.