imageSubobjectIso_comp_image_map — Mathlib

English

The imageSubobjectIso interacts with image.map to produce a commuting diagram: the left and right iso morphisms align with image.map.

Русский

Изоморфизм образа взаимодействует с отображением образа так, что образ образа совместим с изображением левой и правой частей.

LaTeX

$$"imageSubobjectIso_comp_image_map": (imageSubobjectIso f).hom ≫ image.map sq = imageSubobjectMap sq ≫ (imageSubobjectIso g).hom$$

Lean4

theorem imageSubobjectIso_comp_image_map {W X Y Z : C} {f : W ⟶ X} [HasImage f] {g : Y ⟶ Z} [HasImage g]
    (sq : Arrow.mk f ⟶ Arrow.mk g) [HasImageMap sq] :
    (imageSubobjectIso _).hom ≫ image.map sq = imageSubobjectMap sq ≫ (imageSubobjectIso _).hom := by
  erw [← Iso.comp_inv_eq, Category.assoc, ← (imageSubobjectIso f).eq_inv_comp, image_map_comp_imageSubobjectIso_inv sq]

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