English
A pushout cocone c in C is a colimit iff for every X, the induced cone c.op.map(yoneda.obj X) is a limit.
Русский
Копоновый конус-пушаут c в C является колимитом тогда, когда для каждого X полученный конус c.op.map(yoneda.obj X) является пределом.
LaTeX
$$$\\text{IsColimit}(c) \\;\\cong\\; \\forall X,\\; \\text{IsLimit}(c^{op}.map(\\yoneda.obj X)).$$$
Lean4
/-- A pushout cocone in `C` is colimit iff it becomes limit
after the application of `yoneda.obj X` for all `X : C`. -/
def isColimitYonedaEquiv (c : PushoutCocone f g) : IsColimit c ≃ ∀ (X : C), IsLimit (c.op.map (yoneda.obj X)) :=
(Limits.Cocone.isColimitYonedaEquiv c).trans
(Equiv.piCongrRight
(fun X ↦
(IsLimit.whiskerEquivalenceEquiv walkingSpanOpEquiv.symm).trans
((IsLimit.postcomposeHomEquiv (isoWhiskerRight (cospanOp f g).symm (yoneda.obj X)) _).symm.trans
(Equiv.trans (IsLimit.equivIsoLimit (by exact Cones.ext (Iso.refl _) (by rintro (_ | _ | _) <;> simp)))
(c.op.isLimitMapConeEquiv (yoneda.obj X))))))
