hasColimit_of_comp — Mathlib

English

If HasColimit (F ⋙ G), then HasColimit G.

Русский

Если есть колимит у F ⋙ G, то есть колимит у G.

LaTeX

$$$$ \text{HasColimit}(F \circ G) \Rightarrow \text{HasColimit}(G). $$$$

Lean4

/-- When `F` is final, and `F ⋙ G` has a colimit, then `G` has a colimit also.

We can't make this an instance, because `F` is not determined by the goal.
(Even if this weren't a problem, it would cause a loop with `comp_hasColimit`.)
-/
theorem hasColimit_of_comp [HasColimit (F ⋙ G)] : HasColimit G :=
  HasColimit.mk (colimitCoconeOfComp F (getColimitCocone (F ⋙ G)))

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