English
A submodule of a k-vector space V that is stable under all g-scalar actions of G via the embedding of G in MonoidAlgebra k G yields a submodule of V under the MonoidAlgebra action.
Русский
Подмодуля пространства V над k, устойчивого к всем действиям g по элементам G через вложение G в MonoidAlgebra k G, образуется подмодуль над MonoidAlgebra k G.
LaTeX
$$$$\text{If }W\leq_k V\text{ and }\forall g\in G,\ v\in V,\ v\in W \Rightarrow (\,of\ k G\ g)\cdot v\in W,\text{ then }W\text{ is a }(\,MonoidAlgebra k G)\text{-submodule of }V.$$$$
Lean4
/-- A submodule over `k` which is stable under scalar multiplication by elements of `G` is a
submodule over `MonoidAlgebra k G` -/
def submoduleOfSMulMem (W : Submodule k V) (h : ∀ (g : G) (v : V), v ∈ W → of k G g • v ∈ W) :
Submodule (MonoidAlgebra k G) V where
carrier := W
zero_mem' := W.zero_mem'
add_mem' := W.add_mem'
smul_mem' := by
intro f v hv
rw [← Finsupp.sum_single f, Finsupp.sum, Finset.sum_smul]
simp_rw [← smul_of, smul_assoc]
exact Submodule.sum_smul_mem W _ fun g _ => h g v hv
