hasColimit_of_created — Mathlib

English

If F creates the colimit of K and K ⋙ F has a colimit, then K has a colimit.

Русский

Если F создаёт колимит для K и K ⋙ F имеет колимит, то K имеет колимит.

LaTeX

$$$\forall K : J \to C,\ F : C \to D\, [\text{HasColimit } (K \circ F)] \wedge [\text{CreatesColimit } K F] \Rightarrow \text{HasColimit } K$$$

Lean4

/-- If `F` creates the limit of `K` and `K ⋙ F` has a limit, then `K` has a limit. -/
theorem hasColimit_of_created (K : J ⥤ C) (F : C ⥤ D) [HasColimit (K ⋙ F)] [CreatesColimit K F] : HasColimit K :=
  HasColimit.mk
    { cocone := liftColimit (colimit.isColimit (K ⋙ F))
      isColimit := liftedColimitIsColimit _ }

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