English
Let S act on R and M with M a module over R and P a submodule of M. If S acts on R and M in a compatible way (IsScalarTower S R M), then M/P carries a natural action of S defined by a • (x + P) = (a • x) + P; this makes M/P into an S-module and the action is well-defined because the submodule P is preserved by the action of S.
Русский
Пусть S действует на кольцо R и на модуль M, причём M является R-модулем, а P — подмодуль M. Если действия совместимы (IsScalarTower S R M), то на фактормодуле M/P существует естественное действие S, заданное выражением a • (x + P) = (a • x) + P; это превращает M/P в S-модуль, и действие корректно определяется по эквивалентности в фактор-модуле, так как P сохраняется действием S.
LaTeX
$$$\forall a \in S, \forall x \in M,\ a \cdot (x + P) = (a \cdot x) + P$$$
Lean4
instance instSMul' : SMul S (M ⧸ P) :=
⟨fun a =>
Quotient.map' (a • ·) fun x y h =>
leftRel_apply.mpr <| by simpa using Submodule.smul_mem P (a • (1 : R)) (leftRel_apply.mp h)⟩
