English
There is a natural action of the multiplicative structure on the submodules of a module M, defined by applying the action to every element: for a ∈ α and a submodule S ≤ M, a · S is the submodule consisting of all a · x with x ∈ S. This action respects the lattice operations: a · (S ⊔ T) = (a · S) ⊔ (a · T), and a · ⊥ = ⊥, etc.
Русский
Существует естественное действие множества α на подпространства модуля M: для каждого a ∈ α и подмодуля S ≤ M выполняется a · S, состоящее из всех a · x при x ∈ S. Это действие сохраняет объединение и нулевой элемент: a · (S ⊔ T) = (a · S) ⊔ (a · T), a · ⊥ = ⊥ и пр.
LaTeX
$$$a \\cdot S = \\operatorname{Im}((\\mathrm{toLinearMap}\tfrac{R}{M}\\;a): M \\to M)\\big|_S$; in particular, $a \\cdot (S \\sqcup T) = (a \\cdot S) \\sqcup (a \\cdot T)$ and $a \\cdot \\bot = \\bot$.$$
Lean4
/-- The action on a submodule corresponding to applying the action to every element.
This is available as an instance in the `Pointwise` locale. -/
protected def pointwiseDistribMulAction : DistribMulAction α (Submodule R M)
where
smul a S := S.map (DistribMulAction.toLinearMap R M a : M →ₗ[R] M)
one_smul S := (congr_arg (fun f : Module.End R M => S.map f) (LinearMap.ext <| one_smul α)).trans S.map_id
mul_smul _a₁ _a₂
S := (congr_arg (fun f : Module.End R M => S.map f) (LinearMap.ext <| mul_smul _ _)).trans (S.map_comp _ _)
smul_zero _a := map_bot _
smul_add _a _S₁ _S₂ := map_sup _ _ _
