English
If two functors have equivalent categories of cocones, one can transport a colimiting cocone along the equivalence. More precisely, given an equivalence h between Cocone G and Cocone F, for any cocone c over G there is an equivalence between IsColimit (h.functor.obj c) and IsColimit c.
Русский
Если два канала (функторов) имеют эквивалентные категории коконов, можно перенести колимитный кокон вдоль этой эквивалентности. Точнее, при данных h: Cocone G ≃ Cocone F, для каждого кокона c над G имеется эквивалентность между IsColimit (h.functor.obj c) и IsColimit c.
LaTeX
$$$ IsColimit\bigl(h.\mathrm{functor}.\mathrm{obj} \; c\bigr) \simeq IsColimit\; c. $$$
Lean4
/-- Given two functors which have equivalent categories of cocones,
we can transport a colimiting cocone across the equivalence.
-/
def ofCoconeEquiv {D : Type u₄} [Category.{v₄} D] {G : K ⥤ D} (h : Cocone G ≌ Cocone F) {c : Cocone G} :
IsColimit (h.functor.obj c) ≃ IsColimit c
where
toFun P := ofIsoColimit (ofLeftAdjoint h.symm.toAdjunction P) (h.unitIso.symm.app c)
invFun := ofLeftAdjoint h.toAdjunction
left_inv := by cat_disch
right_inv := by cat_disch
