map_homMk'_ι — Mathlib

English

For a pullback-like homMk' construction, image.map preserves the corresponding ι maps: image.map (Arrow.homMk' _ _ w) ≫ image.ι l = image.ι k ≫ n.

Русский

Для конструирования homMk' сохраняя ι-множители выполняется: image.map (Arrow.homMk' _ _ w) ≫ image.ι l = image.ι k ≫ n.

LaTeX

$$$\mathrm{image.map}(\mathrm{Arrow.homMk'}(m,n,w)) \circ \mathrm{image.\iota}(l) = \mathrm{image.\iota}(k) \circ n$$$

Lean4

theorem map_homMk'_ι {X Y P Q : C} {k : X ⟶ Y} [HasImage k] {l : P ⟶ Q} [HasImage l] {m : X ⟶ P} {n : Y ⟶ Q}
    (w : m ≫ l = k ≫ n) [HasImageMap (Arrow.homMk' _ _ w)] :
    image.map (Arrow.homMk' _ _ w) ≫ image.ι l = image.ι k ≫ n :=
  image.map_ι _

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