English
The forward map of the image-isomorphism followed by the canonical inclusion of the range back into H equals the canonical image inclusion; equivalently (imageIsoRange f).hom ∘ Subtype(range f.hom) = image_ι f.
Русский
Впереди образа через изоморфизм изображения затем следует каноническое включение диапазона в H дают отображение изображения в модуль; то есть (imageIsoRange f).hom ∘ subtype(range f.hom) = image_ι f.
LaTeX
$$$$(\\mathrm{imageIsoRange}(f)).\\mathrm{hom} \\circ \\mathrm{subtype}(\\mathrm{range}(f.hom)) = \\iota_f $$$$
Lean4
@[simp, reassoc, elementwise]
theorem imageIsoRange_hom_subtype {G H : ModuleCat.{v} R} (f : G ⟶ H) :
(imageIsoRange f).hom ≫ ModuleCat.ofHom (LinearMap.range f.hom).subtype = Limits.image.ι f := by
rw [← imageIsoRange_inv_image_ι f, Iso.hom_inv_id_assoc]
