isoIsPullback_hom_fst — Mathlib

English

If h and h' are pullbacks of the same pair (f,g), then the canonical isomorphism between the pullbacks respects the left projection: the hom part composed with fst' equals fst.

Русский

Пусть существуют два пулбэпа для одной пары морфизмов (f,g). Тогда канонический изоморфизм между пулбэпами сохраняет левую проекцию: композиция его составляющей hom с fst' равна fst.

LaTeX

$$$(h.isoIsPullback\ _\ _\ h').hom \; ≫ \; fst' = fst.$$$

Lean4

@[reassoc (attr := simp)]
theorem isoIsPullback_hom_fst (h : IsPullback fst snd f g) (h' : IsPullback fst' snd' f g) :
    (h.isoIsPullback _ _ h').hom ≫ fst' = fst :=
  IsLimit.conePointUniqueUpToIso_hom_comp h.isLimit h'.isLimit WalkingCospan.left

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