Connected spectra of group algebras in positive characteristic

For an abelian p-group, every element of its group algebra in exponential characteristic p differs from its augmentation by a nilpotent. Thus the group algebra has connected spectrum whenever the coefficient ring does. In prime characteristic p, the converse holds for finite abelian groups.

This detects connected finite diagonalizable group schemes, including the nonreduced groups of roots of unity of prime-power order.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, Chapter 2.
• J. S. Milne, Algebraic Groups (2017), §12.

theorem TauCeti.isNilpotent_sub_algebraMap_counit_of_isPGroup (R : Type u_1) [CommRing R] {G : Type u_2} [CommGroup G] (p : ℕ) [ExpChar R p] (hG : IsPGroup p G) (x : MonoidAlgebra R G) : IsNilpotent (x - (algebraMap R (MonoidAlgebra R G)) (CoalgebraStruct.counit x))

In the group algebra of an abelian p-group in exponential characteristic p, every element differs from its augmentation by a nilpotent. No finiteness assumption on the group is needed.

theorem TauCeti.connectedSpace_primeSpectrum_monoidAlgebra_of_isPGroup (R : Type u_1) [CommRing R] {G : Type u_2} [CommGroup G] (p : ℕ) [ExpChar R p] [ConnectedSpace (PrimeSpectrum R)] (hG : IsPGroup p G) : ConnectedSpace (PrimeSpectrum (MonoidAlgebra R G))

An abelian p-group has connected group-algebra spectrum over a connected commutative ring of exponential characteristic p.

theorem TauCeti.connectedSpace_primeSpectrum_monoidAlgebra_iff_isPGroup (R : Type u_1) [CommRing R] [ConnectedSpace (PrimeSpectrum R)] (G : Type u_3) [CommGroup G] [Finite G] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] : ConnectedSpace (PrimeSpectrum (MonoidAlgebra R G)) ↔ IsPGroup p G

A finite abelian group has connected group-algebra spectrum over a connected commutative ring of prime characteristic p if and only if it is a p-group.

Use rw [connectedSpace_primeSpectrum_monoidAlgebra_iff_isPGroup R G p] to supply the characteristic explicitly when rewriting a connectedness goal.