inl_isoIsPushout_hom — Mathlib

English

If f,g have two pushouts with left legs inl,inr and inl',inr', then the left legs are related by the pushout iso: inl ≫ (h.isoIsPushout _ _ h').hom = inl'.

Русский

Пусть для пары морфизмов f,g существуют два пушаута с левыми ножками inl,inr и inl',inr'. Тогда левые ножки связаны изоморфизмом пушаут: inl ≫ (h.isoIsPushout _ _ h').hom = inl'.

LaTeX

$$$\forall h,h' : IsPushout\ f\ g\ inl\ inr,\ inl' , inr' : IsPushout\ f\ g\ inl'\ inr'\;:\; inl \;\ggg\; (h.isoIsPushout\\_\\_h').hom = inl'$$$

Lean4

@[reassoc (attr := simp)]
theorem inl_isoIsPushout_hom (h : IsPushout f g inl inr) (h' : IsPushout f g inl' inr') :
    inl ≫ (h.isoIsPushout _ _ h').hom = inl' :=
  IsColimit.comp_coconePointUniqueUpToIso_hom h.isColimit h'.isColimit WalkingSpan.left

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