Smoothness and geometric reducedness of affine groups

Mathlib proves that a geometrically reduced group scheme locally of finite type over a field is smooth. Conversely, a smooth algebra over a field remains smooth, and hence reduced, after every field extension. Transporting both directions through Tau Ceti's affine Hopf/group-scheme dictionary gives the coordinate criterion

finite type + commutative Hopf algebra: geometrically reduced ⇔ smooth.

The finite-type hypothesis is kept separate throughout. In particular, neither geometric reducedness nor smoothness is built into the category of commutative Hopf algebras.

Main declarations

• TauCeti.smoothCommHopfAlgProperty_of_geometricallyReduced: a finite-type geometrically reduced commutative Hopf algebra over a field is smooth.
• TauCeti.geometricallyReducedCommHopfAlgProperty_of_smooth: a smooth commutative Hopf algebra over a field is geometrically reduced.
• TauCeti.smoothCommHopfAlgProperty_iff_geometricallyReduced: the finite-type equivalence.

References

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

The forward implication uses Mathlib's AlgebraicGeometry.smooth_of_grpObj; the reverse uses TauCeti.isReduced_of_smooth after arbitrary field extension.

theorem TauCeti.geometricallyReducedCommHopfAlgProperty_of_smooth (k : Type u) [Field k] (H : CommHopfAlgCat k) (hH : smoothCommHopfAlgProperty k H) : geometricallyReducedCommHopfAlgProperty k H

A smooth commutative Hopf algebra over a field is geometrically reduced.

Smoothness is preserved by extension of the ground field. The resulting tensor product is reduced by TauCeti.isReduced_of_smooth; commuting the tensor factors puts the result in the orientation used by geometricallyReducedCommHopfAlgProperty.

theorem TauCeti.smoothCommHopfAlgProperty_of_geometricallyReduced (k : Type u) [Field k] (H : CommHopfAlgCat k) [Algebra.FiniteType k ↑H] (hH : geometricallyReducedCommHopfAlgProperty k H) : smoothCommHopfAlgProperty k H

A finite-type geometrically reduced commutative Hopf algebra over a field is smooth.

theorem TauCeti.smoothCommHopfAlgProperty_iff_geometricallyReduced (k : Type u) [Field k] (H : CommHopfAlgCat k) [Algebra.FiniteType k ↑H] : smoothCommHopfAlgProperty k H ↔ geometricallyReducedCommHopfAlgProperty k H

For a finite-type commutative Hopf algebra over a field, smoothness is equivalent to geometric reducedness.