A monoid algebra is non-reduced in the presence of p-torsion

This file records the failure of the monoid algebra R[G] of a monoid G to be reduced whenever R has prime characteristic p and G has a nontrivial element killed by p.

The mechanism is the freshman's dream: if g ≠ 1 with g ^ p = 1, then in characteristic p the group-like element single g 1 and the identity 1 = single 1 1 satisfy (single g 1 - 1) ^ p = single (g ^ p) 1 - 1 = single 1 1 - 1 = 0 by sub_pow_char, while single g 1 - 1 ≠ 0 by TauCeti.single_sub_one_ne_zero. So single g 1 - 1 is a nonzero nilpotent and R[G] is not reduced.

Main declarations

• TauCeti.single_sub_one_pow_eq_zero: (single g 1 - 1) ^ p = 0 when g ^ p = 1, in characteristic p.
• TauCeti.isNilpotent_single_sub_one: the element single g 1 - 1 is nilpotent.
• TauCeti.not_isReduced_monoidAlgebra: R[G] is not reduced when G has nontrivial p-torsion and R has characteristic p.
• TauCeti.not_isReduced_monoidAlgebra_of_not_isUnit_card: over a field, noninvertibility of the order of a finite group forces its group algebra to be non-reduced.

References

The freshman's-dream identity (x - y) ^ p = x ^ p - y ^ p in characteristic p is Mathlib's sub_pow_char; the monomial power law single m r ^ n = single (m ^ n) (r ^ n) is Mathlib's MonoidAlgebra.single_pow. The characteristic of the monoid algebra is transported from that of R along the injective algebraMap (charP_of_injective_algebraMap with FaithfulSMul.algebraMap_injective).

theorem TauCeti.single_sub_one_pow_eq_zero {R : Type u_1} [CommRing R] {G : Type u_2} [Monoid G] (p : ℕ) [hp : Fact (Nat.Prime p)] [CharP R p] {g : G} (hgp : g ^ p = 1) : (MonoidAlgebra.single g 1 - 1) ^ p = 0

In characteristic p, the p-th power of single g 1 - 1 vanishes when g ^ p = 1.

theorem TauCeti.isNilpotent_single_sub_one {R : Type u_1} [CommRing R] {G : Type u_2} [Monoid G] (p : ℕ) [hp : Fact (Nat.Prime p)] [CharP R p] {g : G} (hgp : g ^ p = 1) : IsNilpotent (MonoidAlgebra.single g 1 - 1)

The group-like difference single g 1 - 1 is nilpotent when g ^ p = 1 in characteristic p.

theorem TauCeti.not_isReduced_monoidAlgebra {R : Type u_1} [CommRing R] {G : Type u_2} [Monoid G] (p : ℕ) [hp : Fact (Nat.Prime p)] [CharP R p] [Nontrivial R] {g : G} (hg : g ≠ 1) (hgp : g ^ p = 1) : ¬IsReduced (MonoidAlgebra R G)

A monoid algebra with p-torsion is non-reduced in characteristic p. If R has characteristic p and G has a nontrivial element g with g ^ p = 1, then R[G] is not reduced.

theorem TauCeti.not_isReduced_monoidAlgebra_of_not_isUnit_card (k : Type u_3) (G : Type u_4) [Field k] [Group G] [Finite G] (h : ¬IsUnit ↑(Nat.card G)) : ¬IsReduced (MonoidAlgebra k G)

If the order of a finite group vanishes in a field, its group algebra is non-reduced. Cauchy's theorem supplies a nontrivial element of order the characteristic.