English
For a family f_i: β1_i → β2_i, the range of the global mapRange.linearMap f is exactly the comap of the coordinate-wise ranges: the i-th component lies in the range of f_i for all i.
Русский
Для семейства f_i: β1_i → β2_i образ глобального mapRange.linearMap f равен комапу координатных образов: каждая i-я компонента лежит в образе f_i.
LaTeX
$$$\\mathrm{range}(\\mathrm{mapRange.linearMap}\\; f) = \\Big( \\mathrm{Submodule.pi} \\; \\mathrm{Set.univ} \\; (\\mathrm{range}\\; f_i) \\Big).\\mathrm{comap}\\; (\\mathrm{coeFnLinearMap}\\; R)$$$
Lean4
theorem range_mapRangeLinearMap (f : ∀ i, β₁ i →ₗ[R] β₂ i) :
LinearMap.range (mapRange.linearMap f) =
(Submodule.pi Set.univ (LinearMap.range <| f ·)).comap (coeFnLinearMap R) :=
Submodule.toAddSubmonoid_injective <| mrange_mapRangeAddMonoidHom (f · |>.toAddMonoidHom)
