Smoothness of finite commutative group algebras

Over a field, the group algebra of a finite commutative group is smooth precisely when the group order is invertible in the field. The forward direction uses reducedness of a smooth algebra: in the defining characteristic, Cauchy's theorem supplies a nontrivial torsion element, whose difference from the identity is nilpotent in the group algebra. The reverse direction uses étaleness of group algebras of invertible order.

This criterion detects smoothness of finite diagonalizable groups, including the roots-of-unity group schemes.

References

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

@[simp]

theorem TauCeti.MonoidAlgebra.smooth_iff_isUnit_card (k : Type u_1) (G : Type u_2) [Field k] [CommGroup G] [Finite G] : Algebra.Smooth k (MonoidAlgebra k G) ↔ IsUnit ↑(Nat.card G)

A finite commutative group algebra over a field is smooth if and only if the order of the group is invertible in the field.