English
There is a canonical way to lift the compatible scalar action to the product of modules indexed by ι, so that the coordinate projections remain compatible with the S-action; in particular, coordinatewise scalar multiplication commutes with the component maps.
Русский
Существует канонический способ перенести совместное действие скаляра на произведение модулей, индексируемых ι, так что координатные проекции сохраняют совместимость с действием S; в частности, скалярное умножение по координатам выполняется по каждому компоненту.
LaTeX
$$$\\forall r\\in S,\\ \\forall m=(m_i)_{i\\in\\iota},\\ (\\mathrm{proj}_i \\circ f)(r\\cdot m) = r\\cdot (\\mathrm{proj}_i \\circ f)(m)\\quad\\text{for all } i.$$$
Lean4
instance pi (R S M N ι : Type*) [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [SMul R M] [SMul R N] [Module S M]
[Module S N] [LinearMap.CompatibleSMul M N R S] : LinearMap.CompatibleSMul M (ι → N) R S where
map_smul f r m := by ext i; apply ((LinearMap.proj i).comp f).map_smul_of_tower
