English
The image of a morphism f: G ⟶ H in ModuleCat R is the module corresponding to the range of the linear map f.hom.
Русский
Образ морфизма f: G ⟶ H в ModuleCat R является модулем, соответствующим образу линейного отображения f.hom.
LaTeX
$$def image : ModuleCat R := ModuleCat.of R (LinearMap.range f.hom)$$
Lean4
/-- The image of a morphism in `ModuleCat R` is just the bundling of `LinearMap.range f` -/
def image : ModuleCat R :=
ModuleCat.of R (LinearMap.range f.hom)