Smoothness of group schemes #
Main results #
AlgebraicGeometry.smooth_of_grpObj_of_isAlgClosed: IfGis a group scheme over an algebraically closed fieldkthat is reduced and locally of finite type, thenGis smooth overk.
theorem
AlgebraicGeometry.smooth_of_grpObj_of_isAlgClosed
{K : Type u}
[Field K]
[IsAlgClosed K]
{G : Scheme}
(f : G ⟶ Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing })
[LocallyOfFinitePresentation f]
[IsReduced G]
[CategoryTheory.GrpObj (CategoryTheory.Over.mk f)]
:
Smooth f
If G is a group scheme over an algebraically closed field k that is reduced and locally
of finite type, then G is smooth over k.