Smoothness of group schemes

Main results

• AlgebraicGeometry.smooth_of_grpObj: If G is a group scheme over a field k that is geometrically reduced and locally of finite type, then G is smooth over k.

theorem AlgebraicGeometry.smooth_of_grpObj {K : Type u} [Field K] {G : Scheme} (f : G ⟶ Spec (CommRingCat.of K)) [LocallyOfFiniteType f] [CategoryTheory.GrpObj (CategoryTheory.Over.mk f)] [GeometricallyReduced f] : Smooth f