English
If sq is a square between f and g, then imageSubobjectMap sq composed with the arrow of g equals the arrow of f composed with the right side of the square.
Русский
Если $sq$ — квадрат между $f$ и $g$, то $imageSubobjectMap(sq)$ составленный с стрелой $g$ равен стреле $f$ составленной с правой частью квадрата.
LaTeX
$$$imageSubobjectMap\; sq \; \; \cdot (imageSubobject\; g).arrow = (imageSubobject\; f).arrow \cdot sq.right$$$
Lean4
@[reassoc (attr := simp)]
theorem imageSubobjectMap_arrow {W X Y Z : C} {f : W ⟶ X} [HasImage f] {g : Y ⟶ Z} [HasImage g]
(sq : Arrow.mk f ⟶ Arrow.mk g) [HasImageMap sq] :
imageSubobjectMap sq ≫ (imageSubobject g).arrow = (imageSubobject f).arrow ≫ sq.right :=
by
simp only [imageSubobjectMap, Category.assoc, imageSubobject_arrow']
erw [image.map_ι, ← Category.assoc, imageSubobject_arrow]
