English
There is a natural action of the monoid G on the skew monoid algebra SkewMonoidAlgebra M α induced by comapSMul, making SkewMonoidAlgebra a G-set. This action is a genuine MulAction, i.e., 1 acts trivially and (g g') acts as g acting on (g' acting on f).
Русский
Существует естественное действие моноида G на skew-монойдную алгебру SkewMonoidAlgebra M α, индуцированное через comapSMul, образующее действие типа MulAction: единичный элемент действует тривиально, а произведение двух элементов действует как композиция соответствующих действий.
LaTeX
$$$1 \cdot f = f \quad\land\quad (g g') \cdot f = g \cdot (g' \cdot f) \qquad( f \in \mathrm{SkewMonoidAlgebra}(M,\alpha),\ g,g' \in G)$$$
Lean4
/-- `comapSMul` is multiplicative -/
def comapMulAction : MulAction G (SkewMonoidAlgebra M α)
where
one_smul f := by rw [comapSMul_def, one_smul_eq_id, mapDomain_id]
mul_smul g g' f := by rw [comapSMul_def, comapSMul_def, comapSMul_def, ← comp_smul_left, mapDomain_comp]
