English
Equivalence between IsColimit of a cocone c and the property that all Yoneda-mapped cones are limits; the second proof branch establishes the equivalence in a particular internal form.
Русский
Эквивалентность между IsColimit кокона c и свойством, что все конусы после отображения Yoneda являются пределами; во втором доказательном ответе формулировка приводится в конкретной форме.
LaTeX
$$$\\text{Eq}((\\text{yonedaJointlyReflectsLimits } F\\ op\\ c\\ op)\\, \\text{unop},\\; \\mathrm{IsColimit}\\, c)$$$
Lean4
/-- A cocone is colimit iff it becomes limit after the
application of `yoneda.obj X` for all `X : C`. -/
noncomputable def isColimitYonedaEquiv {F : J ⥤ C} (c : Cocone F) :
IsColimit c ≃ ∀ (X : C), IsLimit ((yoneda.obj X).mapCone c.op)
where
toFun h _ := isLimitOfPreserves _ h.op
invFun h := IsLimit.unop (yonedaJointlyReflectsLimits _ _ h)
left_inv _ := Subsingleton.elim _ _
right_inv _ := by ext; apply Subsingleton.elim
