Smoothness detected by Lie dimension

A finite-type affine group over a field is smooth exactly when its dimension equals the dimension of its tangent Lie algebra at the identity. No reducedness, connectedness, or perfection hypothesis is needed, and the criterion detects non-smooth group schemes in positive characteristic.

Over an algebraically closed field, translations identify the local rings at rational points with the local ring at the identity. Regularity at the identity therefore makes every maximal localization reduced, hence makes the coordinate ring reduced and the group smooth. The dimension criterion follows from the existing cotangent-space characterization of regularity. Extension to an algebraic closure preserves both dimensions and detects smoothness, giving the criterion over an arbitrary field.

References

• J. S. Milne, Algebraic Groups (2017), §§1.e and 10.a.
• W. C. Waterhouse, Introduction to Affine Group Schemes, §11.

The formal ingredients are TauCeti.HopfAlgebra.isRegularLocalRing_augmentationStalk_iff, TauCeti.IsRegularLocalRing.isDomain, and Mathlib's isReduced_ofLocalizationMaximal. The translation calculation uses TauCeti.HopfAlgebra.counitAlgHom_comp_rightTranslationAlgHom, as in the proof of TauCeti.HopfAlgebra.height_kernel_eq_height_augmentation.

theorem TauCeti.HopfAlgebra.smooth_iff_isRegularLocalRing_augmentationStalk {k : Type u} {H : Type v} [Field k] [CommRing H] [HopfAlgebra k H] [IsAlgClosed k] [Algebra.FiniteType k H] : Algebra.Smooth k H ↔ IsRegularLocalRing ↑((AlgebraicGeometry.Spec ↧H).presheaf.stalk (Bialgebra.augmentationPoint k H))

A finite-type affine group over an algebraically closed field is smooth exactly when its local ring at the identity is regular.

theorem TauCeti.HopfAlgebra.smooth_iff_finrank_lie_eq_ringKrullDim {k : Type u} {H : Type v} [Field k] [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] : Algebra.Smooth k H ↔ ↑(Module.finrank k (Derivation k H (Bialgebra.CounitAlgebra k H k))) = ringKrullDim H

A finite-type affine group over any field is smooth exactly when its Lie dimension equals its Krull dimension. This criterion includes non-reduced group schemes and imperfect fields.