comapDistribMulActionSelf — Mathlib

English

There is a natural left action of G on the monoid algebra k[G] given by translating the basis elements; this makes k[G] into a G-module, i.e., a distributive multiplicative action of G on k[G].

Русский

Существует естественное левое действие группы G на моноидальную алгебру k[G], задаваемое переносом базисных элементов; это превращает k[G] в модуль над G, то есть в распределённое действие умножения группы на алгебру.

LaTeX

$$$$\text{DistribMulAction } G\; (k[G]), \quad g\cdot\Big(\sum_{h\in G} c_h\,\delta_h\Big) = \sum_{h\in G} c_h\,\delta_{gh}. $$$$

Lean4

/-- This is not an instance as it conflicts with `MonoidAlgebra.distribMulAction` when `G = kˣ`.
-/
def comapDistribMulActionSelf [Group G] [Semiring k] : DistribMulAction G (MonoidAlgebra k G) :=
  Finsupp.comapDistribMulAction

Похожие утверждения