Smoothness of group schemes over algebraically closed fields #
A reduced group scheme locally of finite type over an algebraically closed field is smooth. This upgrades a ring-theoretic reducedness hypothesis to geometric smoothness at the level of group schemes, and supplies the scheme-theoretic input for coordinate-ring consequences such as the finite-type commutative Hopf algebra smoothness criterion.
Main declarations #
TauCeti.AlgebraicGeometry.smooth_of_grpObj_of_isAlgClosed_of_isReduced: the reducedness criterion for smooth group schemes over algebraically closed fields.
References #
- J. S. Milne, Algebraic Groups (2017), Proposition 1.26.
theorem
TauCeti.AlgebraicGeometry.smooth_of_grpObj_of_isAlgClosed_of_isReduced
{K : Type u}
[Field K]
[IsAlgClosed K]
{G : AlgebraicGeometry.Scheme}
(f : G ⟶ AlgebraicGeometry.Spec ↧K)
[AlgebraicGeometry.LocallyOfFiniteType f]
[CategoryTheory.GrpObj (CategoryTheory.Over.mk f)]
[AlgebraicGeometry.IsReduced G]
:
A reduced group scheme locally of finite type over an algebraically closed field is smooth.