isColimitMapCoconeEquiv — Mathlib

English

Isomorphism for PushoutPreservation: the isomorphism i maps the pushout consistently with the mapped morphisms.

Русский

Изоморфизм для сохранения пуш-аута: изomорфизм i согласован с отображёнными морфизмами.

LaTeX

$$$PreservesPushout.iso G f g$$$

Lean4

/-- The map (as a cocone) of a pushout cocone is colimit iff
the map (as a pushout cocone) is limit. -/
def isColimitMapCoconeEquiv : IsColimit (mapCocone G c) ≃ IsColimit (c.map G) :=
  (IsColimit.precomposeHomEquiv (diagramIsoSpan.{v₂} _).symm _).symm.trans <|
    IsColimit.equivIsoColimit <| by
      refine PushoutCocone.ext (Iso.refl _) ?_ ?_
      · dsimp only [inl]
        simp
      · dsimp only [inr]
        simp

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