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

After extending the coordinate maps of the four numbered root subgroups and the rank-two weight torus of the short-root type-G₂ carrier over 𝔽₃ to an algebraically closed characteristic-three field, their common-kernel quotient is reduced and hence smooth.

Main declarations

In the namespace TauCeti.G2ShortRoot.PrimeField:

• isReduced_generatedCoordinateHopfAlgebra and smoothCommHopfAlgProperty_generatedCoordinateHopfAlgebra: reducedness and smoothness over an algebraically closed field.

References

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

The interface follows the generated-subgroup smoothness construction for the type-E₇ minuscule carrier in TauCeti.Algebra.Lie.E7.Minuscule.Generated.Smooth.

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

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

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

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