English
In a category with a zero object, if a morphism f is mono and the coimage–image comparison map coimageImage f is an isomorphism, then the middle map e in the image factorisation of f is also an isomorphism. That is, IsIso (imageMonoFactorisation f).e.
Русский
В категории с нулевым объектом, если морфизм f моно и сопоставление кообраза и образа является изоморфизмом, то средний компонент факторизации изображения e также является изоморфизмом. То есть IsIso (imageMonoFactorisation f).e.
LaTeX
$$$$ [HasZeroObject\\ C] \\Rightarrow [\\text{Mono } f] \\Rightarrow [IsIso(\\Abelian.coimageImageComparison f)] \\Rightarrow IsIso\\big((\\text{imageMonoFactorisation } f).e\\big). $$$$
Lean4
instance [HasZeroObject C] {X Y : C} (f : X ⟶ Y) [Mono f] [IsIso (Abelian.coimageImageComparison f)] :
IsIso (imageMonoFactorisation f).e := by
rw [imageMonoFactorisation_e']
exact IsIso.comp_isIso
