Smoothness of the prime-field short-root F₄ carrier

The short-root type-F₄ carrier over 𝔽₂ is smooth. Its eight numbered root subgroups and rank-four weight torus have reduced coordinate rings. Over the finite ground field, the common-kernel quotient they generate is therefore smooth. Consequently the scalar extension of this same prime-field carrier is smooth over every commutative 𝔽₂-algebra.

This proves smoothness of the actual prime-field carrier and its scalar extensions. It does not require identifying those scalar extensions with the subgroups generated after extension, and makes no assertion of reductivity or pinned-group recognition.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, §11.4.
• J. S. Milne, Algebraic Groups (2017), Proposition 1.26 and Corollary 1.27.

instance TauCeti.F4ShortRoot.PrimeField.algebraSmooth_quotient : Algebra.Smooth (ZMod 2) ↑(CommHopfAlgCat.quotient (GeneralLinear.coordinateHopfAlgebra (ZMod 2) 26) definingIdeal)

The coordinate Hopf algebra of the short-root type-F₄ carrier over 𝔽₂ is smooth.

instance TauCeti.F4ShortRoot.PrimeField.smooth_groupScheme : AlgebraicGeometry.Smooth groupScheme.X.hom

The structural morphism of the prime-field short-root type-F₄ carrier is smooth.