Monoid algebras over a local ring

For a finite monoid G (for instance a finite group) and a local ring R with residue field k, the free module R[G]^ι of finite rank is a finitely generated R-module, so Nakayama's lemma over R detects surjectivity of its endomorphisms after reduction to k[G]^ι. The Orzech property then upgrades surjectivity to bijectivity.

For a finite commutative p-group Q and a local ring R in which p is not a unit, the group algebra R[Q] is itself local, and the augmentation R[Q] → R is a local homomorphism: an element of R[Q] is a unit as soon as its augmentation is. Indeed every maximal ideal of R[Q] lies over the maximal ideal of R, because R[Q] is finite over R, so its residue field has characteristic p; there q - 1 is nilpotent, as (q - 1) ^ (p ^ k) = q ^ (p ^ k) - 1 = 0, and therefore zero. So every maximal ideal contains the augmentation ideal.

Main results

• TauCeti.MonoidAlgebra.bijective_of_forall_exists_mapRingHom_residue_eq: an R[G]-linear endomorphism of R[G]^ι that is onto modulo the maximal ideal is bijective.
• TauCeti.MonoidAlgebra.isLocalHom_lift_one_of_isPGroup: for a finite commutative p-group Q the augmentation R[Q] → R is a local homomorphism.
• TauCeti.MonoidAlgebra.isLocalRing_of_isPGroup: R[Q] is a local ring.

theorem TauCeti.MonoidAlgebra.bijective_of_forall_exists_mapRingHom_residue_eq {R : Type u_1} [CommRing R] [IsLocalRing R] {G : Type u_2} [Monoid G] [Finite G] {ι : Type u_3} [Finite ι] (θ : (ι → MonoidAlgebra R G) →ₗ[MonoidAlgebra R G] ι → MonoidAlgebra R G) (h : ∀ (y : ι → MonoidAlgebra R G), ∃ (x : ι → MonoidAlgebra R G), ∀ (i : ι), (MonoidAlgebra.mapRingHom G (IsLocalRing.residue R)) (θ x i) = (MonoidAlgebra.mapRingHom G (IsLocalRing.residue R)) (y i)) : Function.Bijective ⇑θ

Nakayama's lemma for R[G]^ι. An R[G]-linear endomorphism of R[G]^ι that is onto modulo the maximal ideal is bijective.

theorem TauCeti.MonoidAlgebra.isLocalHom_lift_one_of_isPGroup {R : Type u_4} [CommRing R] [IsLocalRing R] {p : ℕ} [Fact (Nat.Prime p)] {Q : Type u_5} [CommGroup Q] [Finite Q] (hp : ¬IsUnit ↑p) (hQ : IsPGroup p Q) : IsLocalHom ((MonoidAlgebra.lift R R Q) 1)

The augmentation of the group algebra of a p-group is local. For a finite commutative p-group Q and a local ring R in which p is not a unit, the augmentation R[Q] → R is a local homomorphism: an element of R[Q] whose augmentation is a unit is a unit.

theorem TauCeti.MonoidAlgebra.isLocalRing_of_isPGroup {R : Type u_4} [CommRing R] [IsLocalRing R] {p : ℕ} [Fact (Nat.Prime p)] {Q : Type u_5} [CommGroup Q] [Finite Q] (hp : ¬IsUnit ↑p) (hQ : IsPGroup p Q) : IsLocalRing (MonoidAlgebra R Q)

The group algebra of a p-group is local. For a finite commutative p-group Q and a local ring R in which p is not a unit, the group algebra R[Q] is a local ring.