map_comp — Mathlib

English

In a pullback diagram for f: X → Y and g: Y → Z, the left projection of the pullback composed appropriately equals the left projection of the composed morphism f ≫ g.

Русский

В диаграмме вытяжки для f: X → Y и g: Y → Z левая проекция вытяжки, затем прямая композиция, совпадает с левой проекцией композиции f ≫ g.

LaTeX

$$$ ((Over.pullbackComp f g).hom.app A).left \\;\\circ\\; pullback.fst (pullback.snd A.hom g)\\, f \\;\\circ\\; pullback.fst A.hom g = pullback.fst A.hom (f \\circ g) $$$

Lean4

theorem map_comp {X Y Z : T} {f : X ⟶ Y} (hf : P f) {g : Y ⟶ Z} (hg : P g) :
    map Q (P.comp_mem f g hf hg) = map Q hf ⋙ map Q hg :=
  by
  fapply Functor.ext
  · simp [map, Comma.mapRight, CategoryTheory.Comma.mapRight, Comma.lift]
  · intro U V k
    ext
    simp

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