Smoothness of roots-of-unity group schemes

For positive n, the coordinate algebra of μ_n is the group algebra of the cyclic group ℤ/n. It is smooth over a field exactly when n is nonzero in that field. In particular, μ_p is non-smooth in characteristic p, even though its points over an algebraically closed field form the trivial group. This example keeps smoothness separate from the finite-type affine-group-scheme definition.

References

• J. S. Milne, Algebraic Groups (2017), §12.

theorem TauCeti.RootsOfUnityGroup.coordinateRing_smooth_iff {k : Type u} [Field k] (n : ℕ) [NeZero n] : Algebra.Smooth k ↑(DiagonalizableGroup.coordinateRing k (characterGroup n)).obj ↔ IsUnit ↑n

For positive n, the coordinate algebra of μ_n is smooth exactly when n is a unit in the ground field.

theorem TauCeti.RootsOfUnityGroup.coordinateRing_not_smooth {k : Type u} [Field k] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] : ¬Algebra.Smooth k ↑(DiagonalizableGroup.coordinateRing k (characterGroup p)).obj

In characteristic p, the coordinate algebra of μ_p is not smooth.

theorem TauCeti.RootsOfUnityGroup.groupScheme_smooth_iff {k : Type u} [Field k] (n : ℕ) [NeZero n] : AlgebraicGeometry.Smooth (groupScheme k n).X.hom ↔ IsUnit ↑n

The structural morphism of the group scheme μ_n is smooth exactly when n is a unit in the ground field.

theorem TauCeti.RootsOfUnityGroup.groupScheme_not_smooth {k : Type u} [Field k] (p : ℕ) [Fact (Nat.Prime p)] [CharP k p] : ¬AlgebraicGeometry.Smooth (groupScheme k p).X.hom

The roots-of-unity group scheme μ_p is not smooth in characteristic p.