of_iso_pushout — Mathlib

English

If a commuting square h is embedded into a pushout via an isomorphism i: P ≅ pushout f g, with compatible left and right legs, then the resulting square is a pushout for f,g.

Русский

Если дан вскрывающийся квадрат CommSq с изоморфизмом P ≅ pushout f g и совместимыми нижними/верхними ножками, то получившийся квадрат является пушаутом для f,g.

LaTeX

$$$\text{of_iso_pushout}(h,i,w_1,w_2):\; IsPushout\ f\ g\ inl\ inr$$$

Lean4

theorem of_iso_pushout (h : CommSq f g inl inr) [HasPushout f g] (i : P ≅ pushout f g)
    (w₁ : inl ≫ i.hom = pushout.inl _ _) (w₂ : inr ≫ i.hom = pushout.inr _ _) : IsPushout f g inl inr :=
  of_isColimit' h
    (Limits.IsColimit.ofIsoColimit (colimit.isColimit _) (PushoutCocone.ext (s := PushoutCocone.mk ..) i w₁ w₂).symm)

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