image_map_comp_imageSubobjectIso_inv

English

For sq, imageSubobjectMap sq equals a standard composite built from the imageSubobjectIso and image.map components (a definitional equality).

Русский

Для $sq$ отображение образа подобъекта совпадает с обычным композитом, построенным из компонентов $imageSubobjectIso$ и $image.map$.

LaTeX

$$imageSubobjectMap sq = imageSubobjectIso f .hom ≫ image.map sq ≫ imageSubobjectIso g .inv$$

Lean4

theorem image_map_comp_imageSubobjectIso_inv {W X Y Z : C} {f : W ⟶ X} [HasImage f] {g : Y ⟶ Z} [HasImage g]
    (sq : Arrow.mk f ⟶ Arrow.mk g) [HasImageMap sq] :
    image.map sq ≫ (imageSubobjectIso _).inv = (imageSubobjectIso _).inv ≫ imageSubobjectMap sq :=
  by
  ext
  simpa using image.map_ι sq

Похожие утверждения