colimit — Mathlib

English

If P is closed under isomorphisms and F: J ⥤ C has a colimit with all F.obj j ∈ P, then P(colimit F).

Русский

Если P замкнуто по изоморфизмам и диаграмма F: J ⥤ C имеет ко-лимит, причём все домены F.obj j принадлежат P, то P(colimit F).

LaTeX

$$$[P.IsClosedUnderIsomorphisms] \\Rightarrow (\\forall F: J ⥤ C\\,[HasColimit F]\\; (\\forall j, P(F.obj j)) \\Rightarrow P(\\operatorname{colimit} F))$$$

Lean4

protected theorem colimit (h : ClosedUnderColimitsOfShape J P) {F : J ⥤ C} [HasColimit F] :
    (∀ j, P (F.obj j)) → P (colimit F) :=
  h (colimit.isColimit _)

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