Cartier's theorem for affine group schemes #
Every affine group scheme of finite type over a field of characteristic zero is smooth.
This transports TauCeti.smoothCommHopfAlgProperty_of_charZero from coordinate Hopf
algebras to native group objects in schemes. In particular it applies to closed subgroup
schemes without a prior reducedness or smoothness assumption.
References #
- J. S. Milne, Algebraic Groups (2017), Chapter 3, Cartier's theorem.
theorem
TauCeti.AlgebraicGeometry.smooth_of_grpObj_of_charZero
{k : Type u}
[Field k]
[CharZero k]
(G : CategoryTheory.Over (AlgebraicGeometry.Spec ↧k))
[CategoryTheory.GrpObj G]
[AlgebraicGeometry.IsAffine G.left]
[AlgebraicGeometry.LocallyOfFiniteType G.hom]
:
An affine group scheme of finite type over a field of characteristic zero is smooth.