English
For a commutative square between f: W → X and g: Y → Z, there is a canonical morphism from imageSubobject f to imageSubobject g.
Русский
Для коммутативного квадрата между $f: W\to X$ и $g: Y\to Z$ существует каноническое отображение образа подобъекта $f$ в образ подобъекта $g$.
LaTeX
$$$sq : Arrow.mk f \to Arrow.mk g$ with HasImageMap sq yields $imageSubobject f \to imageSubobject g$.$$
Lean4
/-- Given a commutative square between morphisms `f` and `g`,
we have a morphism in the category from `imageSubobject f` to `imageSubobject g`. -/
def imageSubobjectMap {W X Y Z : C} {f : W ⟶ X} [HasImage f] {g : Y ⟶ Z} [HasImage g] (sq : Arrow.mk f ⟶ Arrow.mk g)
[HasImageMap sq] : (imageSubobject f : C) ⟶ (imageSubobject g : C) :=
(imageSubobjectIso f).hom ≫ image.map sq ≫ (imageSubobjectIso g).inv
