Étaleness of finite commutative group algebras

A finite commutative group algebra is étale when the group order is invertible in the base ring. Over a field this condition is also necessary: torsion of prime order equal to the characteristic produces a nonzero nilpotent. Applied to character groups, this detects the infinitesimal structure of finite diagonalizable groups.

References

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

The converse uses TauCeti.not_isReduced_monoidAlgebra and Mathlib's Cauchy theorem.

theorem TauCeti.MonoidAlgebra.formallyUnramified_of_isUnit_card (R : Type u_1) (G : Type u_2) [CommRing R] [CommGroup G] (h : IsUnit ↑(Nat.card G)) : Algebra.FormallyUnramified R (MonoidAlgebra R G)

A commutative group algebra is formally unramified if its group order is invertible in the base ring.

theorem TauCeti.MonoidAlgebra.etale_of_isUnit_card (R : Type u_1) (G : Type u_2) [CommRing R] [CommGroup G] [Finite G] (h : IsUnit ↑(Nat.card G)) : Algebra.Etale R (MonoidAlgebra R G)

A finite commutative group algebra is étale if its group order is invertible in the base ring. This includes arbitrary, possibly non-Noetherian, base rings.

theorem TauCeti.MonoidAlgebra.etale_iff_isUnit_card (G : Type u_2) [CommGroup G] [Finite G] (k : Type u_3) [Field k] : Algebra.Etale k (MonoidAlgebra k G) ↔ IsUnit ↑(Nat.card G)

Over a field, a finite commutative group algebra is étale exactly when its group order is invertible, equivalently when the characteristic does not divide that order.