hasColimit_of_hasColimit_liftFromUnder

English

If liftFromUnder.obj F has a colimit for a diagram F: J ⥤ Under X, then F itself has a colimit.

Русский

Если у диаграммы F : J ⥤ Under X есть колимит, полученный посредством liftFromUnder, то сама диаграмма F имеет колимит.

LaTeX

$$$\text{HasColimit }(F)\quad\text{given }\text{HasColimit}(\mathrm{liftFromUnder}.\mathrm{obj}\, F)$$$

Lean4

theorem hasColimit_of_hasColimit_liftFromUnder {X : C} (F : J ⥤ Under X) [HasColimit (liftFromUnder.obj F)] :
    HasColimit F :=
  ⟨_, isColimitEquiv <| .ofIsoColimit (colimit.isColimit (liftFromUnder.obj F)) (coconeEquiv.counitIso.app _).symm⟩

Похожие утверждения