English
Given a family of subspaces p_i ⊆ E_i, there is a natural continuous linear map from the tensor product of the p_i to the tensor product of E_i, obtained by tensoring the inclusion maps p_i ↪ E_i.
Русский
Пусть для каждого i имеется подпространство p_i ⊆ E_i. Тогда существует естественное непрерывное линейное отображение из тензорного произведения ⨂ i p_i в ⨂ i E_i, получаемое тензорированием включений p_i ↪ E_i.
LaTeX
$$$ p : \\Pi i, \\mathrm{Submodule}\\; 𝕜(E_i) \\,\\;\\Longrightarrow \\\\ (⨂[𝕜] i, p i) \\toL[𝕜] (⨂[𝕜] i, E i) = \\mathrm{mapL} (\\lambda i, (p i).\\mathrm{subtypeL}) $$$
Lean4
/-- Given submodules `pᵢ ⊆ Eᵢ`, this is the natural map: `⨂[𝕜] i, pᵢ → ⨂[𝕜] i, Eᵢ`.
This is the continuous version of `PiTensorProduct.mapIncl`.
-/
@[simp]
noncomputable def mapLIncl (p : Π i, Submodule 𝕜 (E i)) : (⨂[𝕜] i, p i) →L[𝕜] ⨂[𝕜] i, E i :=
mapL fun (i : ι) ↦ (p i).subtypeL
