pullbackComp_left_fst_fst — Mathlib

English

If f = g as morphisms X ⟶ Y, then the left projection after the pullback congruence equals the left projection of f.

Русский

Если f = g как морфизмы X ⟶ Y, то левая проекция после конгруэнции вытяжки совпадает с левой проекцией f.

LaTeX

$$$ ((Over.pullbackCongr h).hom.app A).left \\;\\circ\\; pullback.fst A.hom g = pullback.fst A.hom f $$$

Lean4

theorem pullbackComp_left_fst_fst [Q.RespectsIso] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z) (A : P.Over Q Z) :
    ((Over.pullbackComp f g).hom.app A).left ≫ pullback.fst (pullback.snd A.hom g) f ≫ pullback.fst A.hom g =
      pullback.fst A.hom (f ≫ g) :=
  by simp

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