English
For a semilinear continuous linear map f, one can view f as a map into its range; this yields a natural continuous linear map to the submodule Range(f).
Русский
Для непрерывно-линейного отображения f существует каноничное представление f с кодом в его образ Range(f): f можно рассмотреть как отображение в Range(f) с сохранением линейности и непрерывности.
LaTeX
$$$\text{rangeRestrict}: M_1 \to_L[\sigma_{12}] \operatorname{range}(f), \quad f = \iota \circ \text{rangeRestrict}(f),$ where $\iota$ is the inclusion $\operatorname{range}(f) \hookrightarrow M_2$.$$
Lean4
/-- Restrict the codomain of a continuous linear map `f` to `f.range`. -/
abbrev rangeRestrict [RingHomSurjective σ₁₂] (f : M₁ →SL[σ₁₂] M₂) :=
f.codRestrict (LinearMap.range f) (LinearMap.mem_range_self f)
