English
A pushout cocone in C is a colimit cocone if and only if the corresponding pullback cone in the opposite category is a limit cone.
Русский
Кокон копроизведения в C является колимитом тогда и только тогда, когда соответствующий конус прообратной категории является пределом.
LaTeX
$$$$\mathrm{IsColimit}(c) \simeq \mathrm{IsLimit}(c^{\mathrm{op}}).$$$$
Lean4
/-- A pushout cone is a colimit cocone if and only if the corresponding pullback cone
in the opposite category is a limit cone. -/
noncomputable -- just for performance; compilation takes several seconds
def isColimitEquivIsLimitOp {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) :
IsColimit c ≃ IsLimit c.op := by
apply equivOfSubsingletonOfSubsingleton
· intro h
exact
(IsLimit.postcomposeHomEquiv _ _).invFun ((IsLimit.whiskerEquivalenceEquiv walkingSpanOpEquiv.symm).toFun h.op)
· intro h
exact
(IsColimit.equivIsoColimit c.opUnop).toFun
(((IsLimit.postcomposeHomEquiv _ _).invFun ((IsLimit.whiskerEquivalenceEquiv _).toFun h)).unop)
