Smoothness of the generated short-root type-F₄ subgroup after scalar extension

The short-root type-F₄ carrier over 𝔽₂ is generated by eight numbered root subgroups and its rank-four weight torus. After extending the coordinate maps to an algebraically closed characteristic-two field, their common-kernel quotient is reduced and smooth. This quotient is the scalar extension of the prime-field carrier; see TauCeti.F4ShortRoot.PrimeField.baseChangeDefiningIdeal_eq_generatedDefiningIdeal.

References

• J. E. Humphreys, Linear Algebraic Groups, §§26–27.
• J. S. Milne, Algebraic Groups (2017), §2.h.

The generated-subgroup smoothness interface originates in TauCeti.Algebra.Lie.E7.Minuscule.Generated.Smooth.

theorem TauCeti.F4ShortRoot.PrimeField.isReduced_generatedCoordinateHopfAlgebra (k : Type u) [Field k] [Algebra (ZMod 2) k] [IsAlgClosed k] : IsReduced ↑(generatedCoordinateHopfAlgebra k)

The subgroup generated after scalar extension has reduced coordinate algebra over an algebraically closed field.

theorem TauCeti.F4ShortRoot.PrimeField.smoothCommHopfAlgProperty_generatedCoordinateHopfAlgebra (k : Type u) [Field k] [Algebra (ZMod 2) k] [IsAlgClosed k] : smoothCommHopfAlgProperty k (generatedCoordinateHopfAlgebra k)

The subgroup generated after scalar extension is smooth over an algebraically closed field.