English
Let k be a commutative semiring and G a group. The k[G]-action on the left-regular object G (viewed as a k[G]-module) coincides with multiplication in the group algebra: for all x ∈ k[G] and y ∈ k[G] (viewed in the left-regular module), x acts on y by left multiplication, i.e. x • y = x y.
Русский
Пусть k — коммутативная полугруппа, G — группа. Действие k[G] на объекты, образующие левое регулярное представление на самом G, совпадает с умножением в групповой алгебре: для всех x ∈ k[G] и y ∈ k[G], действие x на y равно произведению x y.
LaTeX
$$$ x \cdot y = x y \quad \\text{для всех } x \\in k[G],\\; y \\in k[G]. $$$
Lean4
theorem ofMulAction_self_smul_eq_mul (x : MonoidAlgebra k G) (y : (ofMulAction k G G).asModule) :
x • y = (x * y : MonoidAlgebra k G) := by
induction x using MonoidAlgebra.induction_on with
| hM g =>
change asAlgebraHom (ofMulAction k G G) _ _ = _
ext
-- Porting note: single_mul_apply not firing in simp without parentheses, probably due to the
-- defeq abuse in `change` above.
simp [(MonoidAlgebra.single_mul_apply)]
| hadd x y hx hy => simp only [hx, hy, add_mul, add_smul]
| hsmul r x hx => simp [← hx]
