Smooth affine groups over algebraically closed fields

A reduced group scheme locally of finite type over an algebraically closed field is smooth. For finite-type commutative Hopf algebras this gives the particularly useful coordinate criterion

smooth over an algebraically closed field ↔ reduced coordinate ring.

These criteria let downstream constructions establish the ring-theoretic condition of ordinary reducedness instead of proving smoothness directly. The geometric-reducedness criterion also supplies the resulting stability under field extension when affine groups and their subgroup schemes are compared after base change.

Main declarations

• TauCeti.AlgebraicGeometry.smooth_of_grpObj_of_isAlgClosed_of_isReduced: the scheme-theoretic criterion.
• TauCeti.smoothCommHopfAlgProperty_of_isAlgClosed_of_isReduced: a reduced finite-type commutative Hopf algebra over an algebraically closed field is smooth.
• TauCeti.smoothCommHopfAlgProperty_iff_isReduced_of_isAlgClosed: the coordinate smoothness criterion.
• TauCeti.geometricallyReducedCommHopfAlgProperty_iff_isReduced_of_isAlgClosed: over an algebraically closed field, ordinary and geometric reducedness agree for finite-type commutative Hopf algebras.

References

• J. S. Milne, Algebraic Groups (2017), Proposition 1.26 and Corollary 1.27.

theorem TauCeti.smoothCommHopfAlgProperty_of_isAlgClosed_of_isReduced (k : Type u) [Field k] [IsAlgClosed k] (H : CommHopfAlgCat k) [Algebra.FiniteType k ↑H] [IsReduced ↑H] : smoothCommHopfAlgProperty k H

A reduced finite-type commutative Hopf algebra over an algebraically closed field is smooth.

theorem TauCeti.smoothCommHopfAlgProperty_iff_isReduced_of_isAlgClosed (k : Type u) [Field k] [IsAlgClosed k] (H : CommHopfAlgCat k) [Algebra.FiniteType k ↑H] : smoothCommHopfAlgProperty k H ↔ IsReduced ↑H

For a finite-type commutative Hopf algebra over an algebraically closed field, smoothness is equivalent to reducedness of its coordinate ring.

theorem TauCeti.geometricallyReducedCommHopfAlgProperty_iff_isReduced_of_isAlgClosed (k : Type u) [Field k] [IsAlgClosed k] (H : CommHopfAlgCat k) [Algebra.FiniteType k ↑H] : geometricallyReducedCommHopfAlgProperty k H ↔ IsReduced ↑H

Over an algebraically closed field, a finite-type commutative Hopf algebra is geometrically reduced exactly when its coordinate ring is reduced.