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