English
For a diagram K: J ⥤ Under X and a cocone t over K, t is a colimit iff the corresponding lifted cocone in C, obtained via coconeEquiv, is a colimit. The equivalence is given by IsColimit.ofCoconeEquiv coconeEquiv.
Русский
Для диаграммы K: J ⥤ Under X и коконуса t над K, коконус t является колимитом тогда и только тогда, когда соответствующий поднесенный коконус в C, полученный через coconeEquiv, является колимитом. Эквивалентность задается IsColimit.ofCoconeEquiv coconeEquiv.
LaTeX
$$$$ \text{IsColimit}(\mathrm{coconeEquiv.functor.obj}(t)) \simeq \text{IsColimit}(t). $$$$
Lean4
/-- A cocone `t` of `K : J ⥤ Under X` is a colimit if and only if the corresponding cocone
`coconeLift t` of `liftFromUnder.obj K : WithInitial K ⥤ C` is a colimit. -/
@[simps!]
def isColimitEquiv : IsColimit (coconeEquiv.functor.obj t) ≃ IsColimit t :=
IsColimit.ofCoconeEquiv coconeEquiv
