Units in a finite p-group algebra are detected by augmentation

Proved

MonoidAlgebra.isUnit_iff_augmentation_of_isPGroup

by davidloeffler · Sep 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

commutative-algebragroup-ringsp-groups

For a finite commutative p-group G over a commutative local ring R of residue characteristic p, an element of R[G] is a unit if and only if its augmentation is a unit in R.

Preamble

import Definitions.Def_MonoidAlgebra_Augmentation
import Mathlib.GroupTheory.PGroup
import Mathlib.RingTheory.LocalRing.ResidueField.Basic
import Theorems.Thm_MonoidAlgebra_isLocalRing_of_isPGroup

set_option autoImplicit false
noncomputable section

Formal statement

/-- In the group ring of a finite `p`-group over a commutative local ring of
residue characteristic `p`, an element is a unit exactly when its augmentation
is a unit. This is the augmentation corollary of
`MonoidAlgebra.isLocalRing_of_isPGroup`. -/
theorem MonoidAlgebra.isUnit_iff_augmentation_of_isPGroup
    {R G : Type*} [CommRing R] [IsLocalRing R]
    {p : ℕ} [Fact p.Prime] [CommGroup G] [Finite G]
    (hp : (p : R) ∈ IsLocalRing.maximalIdeal R)
    (hG : IsPGroup p G) (x : MonoidAlgebra R G) :
    IsUnit x ↔ IsUnit (MonoidAlgebra.augmentation R G x) := by
  letI := MonoidAlgebra.isLocalRing_of_isPGroup hp hG
  let aug := MonoidAlgebra.augmentation R G
  have hsurj : Function.Surjective aug := by
    intro r
    refine ⟨MonoidAlgebra.single 1 r, ?_⟩
    simp [aug, MonoidAlgebra.augmentation]
  letI : IsLocalHom aug := IsLocalHom.of_surjective aug hsurj
  exact (isUnit_map_iff aug x).symm

Source

Corollary of Nicholson's local group-ring theorem and the standard augmentation map; https://doi.org/10.4153/CMB-1972-025-1.

View graph