English
Let f: G → H be a morphism of R-modules. The categorical image of f is naturally isomorphic to the submodule range of the underlying linear map f.hom; equivalently Im(f) ≅_R ModuleCat.of(R, range(f.hom)).
Русский
Пусть f: G → H — морфизм модулей над кольцом R. Категорическое изображение f естественным образом изоморфно подмодулю образа линейного отображения f.hom; то есть изображение равно изоморфному модулю диапазона range(f.hom).
LaTeX
$$$$ \\operatorname{Im}(f) \\cong_R \\mathrm{ModuleCat.of}(R, \\operatorname{range}(f.hom)) $$$$
Lean4
/-- The categorical image of a morphism in `ModuleCat R` agrees with the linear algebraic range. -/
noncomputable def imageIsoRange {G H : ModuleCat.{v} R} (f : G ⟶ H) :
Limits.image f ≅ ModuleCat.of R (LinearMap.range f.hom) :=
IsImage.isoExt (Image.isImage f) (isImage f)
