English
The hom part of imageSubobjectCompIso interacts with imageSubobject f.arrow via a standard arrow compatibility relation: (imageSubobjectCompIso f h).hom ≫ (imageSubobject f).arrow = (imageSubobject (f ≫ h)).arrow ≫ inv h.
Русский
Гом-часть imageSubobjectCompIso совместима с imageSubobject f.arrow: (imageSubobjectCompIso f h).hom ≫ (imageSubobject f).arrow = (imageSubobject (f ≫ h)).arrow ≫ inv h.
LaTeX
$$$(\mathrm{imageSubobjectCompIso}(f,h).\mathrm{hom}) \circ (\mathrm{imageSubobject} f).\mathrm{arrow} = (\mathrm{imageSubobject}(f \circ h)).\mathrm{arrow} \circ (\mathrm{inv} \, h)$$$
Lean4
/-- Postcomposing by an isomorphism gives an isomorphism between image subobjects. -/
def imageSubobjectCompIso (f : X ⟶ Y) [HasImage f] {Y' : C} (h : Y ⟶ Y') [IsIso h] :
(imageSubobject (f ≫ h) : C) ≅ (imageSubobject f : C) :=
imageSubobjectIso _ ≪≫ (image.compIso _ _).symm ≪≫ (imageSubobjectIso _).symm
