Cartier's theorem

Every affine group scheme of finite type over a field of characteristic zero is smooth. In Hopf coordinates: a finite-type commutative Hopf algebra over a field of characteristic zero is smooth, and in particular reduced. Nonreduced groups such as μ_p and αₚ therefore occur only in positive characteristic.

The proof runs over an algebraically closed field k first. Let H be the coordinate ring and N its nilradical, a Hopf ideal since k is perfect.

• Every tangent vector at the identity extends to an invariant derivation of H, and in characteristic zero derivations send nilpotent functions into the augmentation ideal. Hence N lies in the square of the augmentation ideal, and the reduced group H ⧸ N has the same Lie algebra as H.
• The reduced group is smooth over k, so it is regular at the identity, and its Lie algebra has dimension dim (H ⧸ N) = dim H.
• So the Lie algebra of H has dimension dim H, which makes the local ring of H at the identity regular, hence a domain. Each nilpotent function is then killed by a function not vanishing at the identity.
• Translating by rational points moves the identity to every closed point, so each nilpotent function is killed by a function outside every maximal ideal, and is zero.

Over a general field of characteristic zero, each extension field embeds in an algebraically closed one, over which the base-changed Hopf algebra is reduced. This is geometric reducedness, which for finite-type Hopf algebras is equivalent to smoothness.

Main results

• TauCeti.smoothCommHopfAlgProperty_of_charZero: Cartier's theorem, a finite-type commutative Hopf algebra over a field of characteristic zero is smooth.
• TauCeti.HopfAlgebra.isReduced_of_charZero: such a Hopf algebra is reduced.

References

• J. S. Milne, Algebraic Groups (2017), Chapter 3 (Cartier's theorem).
• W. C. Waterhouse, Introduction to Affine Group Schemes, §11.4.

theorem TauCeti.smoothCommHopfAlgProperty_of_charZero (k : Type u) [Field k] [CharZero k] (H : CommHopfAlgCat k) [Algebra.FiniteType k ↑H] : smoothCommHopfAlgProperty k H

Cartier's theorem: a finite-type commutative Hopf algebra over a field of characteristic zero is smooth. Equivalently, every affine group scheme of finite type over such a field is smooth.

theorem TauCeti.HopfAlgebra.isReduced_of_charZero (k : Type u) [Field k] [CharZero k] (H : Type v) [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] : IsReduced H

A finite-type commutative Hopf algebra over a field of characteristic zero is reduced: affine group schemes of finite type in characteristic zero have no nilpotent functions.