The augmentation of a monoid algebra

The coefficient-sum augmentation R[K] → R sends each singleton single k r to r. It is natural in the monoid K and is defined over any semiring R. As an R-linear map it is surjective, and its kernel is the augmentation ideal with scalars restricted to R.

The augmentation gives the trivial action of K on R and is the counit of the monoid-algebra bialgebra. Descriptions of its kernel by generators and the resulting exactness statements live in TauCeti.Algebra.MonoidAlgebra.Exactness.

Main declarations

• TauCeti.MonoidAlgebra.augmentation: the coefficient-sum ring homomorphism.
• TauCeti.MonoidAlgebra.augmentation_comp_mapDomainRingHom: naturality in the monoid.
• MonoidAlgebra.augmentation_mapDomainRingEquiv: invariance under monoid isomorphisms.
• MonoidAlgebra.augmentationLinearMap: the coefficient-sum linear map.
• MonoidAlgebra.augmentationLinearMap_surjective: surjectivity over any semiring.
• MonoidAlgebra.ker_augmentationLinearMap: the linear kernel is the augmentation ideal.
• MonoidAlgebra.eq_sum_single_of_mul_single_eq_self: over an additively torsion-free semiring, an element invariant under every right translation and with augmentation |G| is the norm.

References

• J. S. Milne, Algebraic Groups (2017), Theorem 12.9(b), for the augmentation of a group algebra.

noncomputable def TauCeti.MonoidAlgebra.augmentation (R : Type u) [Semiring R] (K : Type v) [Monoid K] : MonoidAlgebra R K →+* R

The coefficient-sum augmentation of a monoid algebra. It sends every standard basis element to 1 and acts identically on coefficients.

@[simp]

theorem TauCeti.MonoidAlgebra.augmentation_single (R : Type u) [Semiring R] {K : Type v} [Monoid K] (k : K) (r : R) : (augmentation R K) (MonoidAlgebra.single k r) = r

The coefficient-sum augmentation sends a singleton to its coefficient.

@[simp]

theorem TauCeti.MonoidAlgebra.augmentation_comp_mapDomainRingHom (R : Type u) [Semiring R] {M : Type v} {N : Type w} [Monoid M] [Monoid N] (f : M →* N) : (augmentation R N).comp (MonoidAlgebra.mapDomainRingHom R f) = augmentation R M

The coefficient-sum augmentation is natural with respect to homomorphisms of monoids.

@[simp]

theorem MonoidAlgebra.augmentation_mapDomainRingEquiv (R : Type u) [Semiring R] {M : Type v} {N : Type w} [Monoid M] [Monoid N] (e : M ≃* N) (x : MonoidAlgebra R M) : (TauCeti.MonoidAlgebra.augmentation R N) ((mapDomainRingEquiv R e) x) = (TauCeti.MonoidAlgebra.augmentation R M) x

The coefficient-sum augmentation is invariant under an isomorphism of monoids.

noncomputable def MonoidAlgebra.augmentationLinearMap (R : Type u) [Semiring R] (K : Type v) [Monoid K] : MonoidAlgebra R K →ₗ[R] R

The coefficient-sum augmentation as an R-linear map R[K] → R.

@[simp]

theorem MonoidAlgebra.augmentationLinearMap_apply (R : Type u) [Semiring R] (K : Type v) [Monoid K] (x : MonoidAlgebra R K) : (augmentationLinearMap R K) x = (TauCeti.MonoidAlgebra.augmentation R K) x

theorem MonoidAlgebra.augmentationLinearMap_surjective (R : Type u) [Semiring R] (K : Type v) [Monoid K] : Function.Surjective ⇑(augmentationLinearMap R K)

Over any semiring, the coefficient-sum linear map is surjective.

theorem MonoidAlgebra.ker_augmentationLinearMap (R : Type u) [Semiring R] (K : Type v) [Monoid K] : (augmentationLinearMap R K).ker = Submodule.restrictScalars R (RingHom.ker (TauCeti.MonoidAlgebra.augmentation R K))

The kernel of the linear augmentation is the augmentation ideal, with scalars restricted.

theorem MonoidAlgebra.eq_sum_single_of_mul_single_eq_self {R : Type u_1} {G : Type u_2} [Semiring R] [IsAddTorsionFree R] [Group G] [Fintype G] {γ : MonoidAlgebra R G} (hinv : ∀ (g : G), γ * single g 1 = γ) (hε : (TauCeti.MonoidAlgebra.augmentation R G) γ = ↑(Fintype.card G)) : γ = ∑ g : G, single g 1

Over an additively torsion-free semiring, an element of a finite group algebra invariant under right multiplication by every group element and with augmentation |G| is the norm element ∑ g, single g 1.