English
Given submodules p_i of s_i, there is a natural linear map from the tensor product of these submodules to the tensor product of the ambient modules, obtained by applying the inclusion maps p_i ↪ s_i coordinatewise.
Русский
Пусть p_i ⊆ s_i — подмодули. Существует естественный линейный отображение ⨂_i p_i → ⨂_i s_i, получаемый приложением вложений (p_i) ↪ s_i в каждой координате.
LaTeX
$$$\text{Let } p = \{p_i \subseteq s_i\}.\; (\⨂[R] i, p_i) \to (\⨂[R] i, s_i) \,;\;\text{mapIncl}(p) = \text{map}(\lambda i, (p_i).subtype)$$$
Lean4
/-- Given submodules `p i ⊆ s i`, this is the natural map: `⨂[R] i, p i → ⨂[R] i, s i`.
This is `TensorProduct.mapIncl` for an arbitrary family of modules.
-/
@[simp]
def mapIncl (p : Π i, Submodule R (s i)) : (⨂[R] i, p i) →ₗ[R] ⨂[R] i, s i :=
map fun (i : ι) ↦ (p i).subtype
