comp — Mathlib

English

If sq1 and sq2 are composable, and HasImageMap sq1, HasImageMap sq2, then HasImageMap (sq1 ≫ sq2).

Русский

Если есть сопоставления изображений для sq1 и sq2, то для их композиции существует HasImageMap.

LaTeX

$$$ \\text{HasImageMap}( (\\mathrm{CategoryTheory.instCategoryArrow C}).comp \\; sq1 \\; sq2) $$$

Lean4

instance comp {f g h : Arrow C} [HasImage f.hom] [HasImage g.hom] [HasImage h.hom] (sq1 : f ⟶ g) (sq2 : g ⟶ h)
    [HasImageMap sq1] [HasImageMap sq2] : HasImageMap (sq1 ≫ sq2) :=
  HasImageMap.mk
    { map := (HasImageMap.imageMap sq1).map ≫ (HasImageMap.imageMap sq2).map
      map_ι := by rw [Category.assoc, ImageMap.map_ι, ImageMap.map_ι_assoc, Comma.comp_right] }

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