hasColimit_of_hasColimit_comp_eval

English

If each F ⋙ Pi.eval C i has a colimit, then F has a colimit in ∀ i, C i.

Русский

Если для каждой i композиция F ⋙ Pi.eval C_i имеет колимит, то F имеет колимит в ∀ i, C_i.

LaTeX

$$$ [\\forall i, HasColimit (F .\\!\\cdot (\\Pi.eval C i))] \\Rightarrow HasColimit F $$$

Lean4

/-- If we have a functor `F : J ⥤ Π i, C i` into a category of indexed families,
and colimits exist for each of the `F ⋙ Pi.eval C i`,
there is a colimit for `F`.
-/
theorem hasColimit_of_hasColimit_comp_eval : HasColimit F :=
  HasColimit.mk
    { cocone := coconeOfCoconeCompEval fun _ => colimit.cocone _
      isColimit := coconeOfCoconeEvalIsColimit fun _ => colimit.isColimit _ }

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