isoIsPullback_hom_snd — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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