hasColimit_of_small_quot — Mathlib

English

If J is small and F: J ⥤ AddCommGrpCat, then F has a colimit in AddCommGrpCat. In particular, HasColimit F holds.

Русский

Если J малая категория и F: J ⥤ AddCommGrpCat, то F имеет колимит в AddCommGrpCat; то есть существует колимит F.

LaTeX

$$$ \text{HasColimit } F $$$

Lean4

theorem hasColimit_of_small_quot [DecidableEq J] (h : Small.{w} (Quot F)) : HasColimit F :=
  ⟨_, colimitCoconeIsColimit F⟩

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