English
Let (s_i) and (t_i) be families of R-modules and f_i : s_i → t_i be linear maps. The map map f : ⨂_i s_i → ⨂_i t_i sends a simple tensor ⊗_i x_i to ⊗_i f_i(x_i). The range of this map is exactly the submodule generated by all tensors of the form ⊗_i f_i(m_i) with m_i ∈ s_i; equivalently, the image is the span of all tensors arising from applying the f_i to elements of s_i.
Русский
Пусть (s_i) и (t_i) — семейства модулей над кольцом R, и для каждого i имеется линейное отображение f_i : s_i → t_i. Отображение map f: ⨂_i s_i → ⨂_i t_i отправляет простое тензорное произведение ⊗_i x_i в ⊗_i f_i(x_i). Образ этого отображения состоит в точности в подмодуля, порождаемого всеми тензорами тождественной формы ⊗_i f_i(m_i) (где m_i ∈ s_i); другими словами, образ равен линейной оболочке множества таких тензоров.
LaTeX
$$$\operatorname{range}(\mathrm{map}\ f) = \operatorname{span}_R\{ t \;|\; \exists m : \prod_i s_i,\; t = tprod\,R (\lambda i. f_i(m_i)) \}$$$
Lean4
theorem map_range_eq_span_tprod :
LinearMap.range (map f) = Submodule.span R {t | ∃ (m : Π i, s i), tprod R (fun i ↦ f i (m i)) = t} :=
by
rw [← Submodule.map_top, ← span_tprod_eq_top, Submodule.map_span, ← Set.range_comp]
apply congrArg; ext x
simp only [Set.mem_range, comp_apply, map_tprod, Set.mem_setOf_eq]
