English
Let r be a MonoidAlgebra element, x ∈ V, y ∈ W. The action of r on the tensor product (ρV ⊗ 1) acting on x ⊗ y equals the tensor of the action of r on x with y: r • (ρV ⊗ 1)(x ⊗ y) = (r • x) ⊗ y.
Русский
Пусть r ∈ MonoidAlgebra, x ∈ V, y ∈ W. Действие r на тензор-объединение (ρV ⊗ 1) применимо к x ⊗ y даёт тензорное произведение: (r • x) ⊗ y.
LaTeX
$$$ r \\cdot ( x \\otimes y ) = ( r \\cdot x ) \\otimes y $$$
Lean4
theorem smul_one_tprod_asModule (r : MonoidAlgebra k G) (x : V) (y : W) :
r • (show (1 ⊗ ρW).asModule from x ⊗ₜ y) = x ⊗ₜ (r • show ρW.asModule from y) :=
by
change asAlgebraHom (1 ⊗ ρW) _ _ = _ ⊗ₜ asAlgebraHom ρW _ _
simp only [asAlgebraHom_def, MonoidAlgebra.lift_apply, tprod_apply, MonoidHom.one_apply, LinearMap.finsupp_sum_apply,
LinearMap.smul_apply, TensorProduct.map_tmul, Module.End.one_apply]
simp only [Finsupp.sum, TensorProduct.tmul_sum, TensorProduct.tmul_smul]
