instHasFilteredColimitsInd — Mathlib

English

If C has filtered colimits, then Ind(C) has filtered colimits as well; these colimits are created by the inclusion Ind(C) → Ind(C).

Русский

Если у C есть фильтрованные колимиты, то и Ind(C) имеет фильтрованные колимиты; эти колимиты создаются включением Ind(C) в саму категорию Ind(C).

LaTeX

$$$\text{HasFilteredColimits}(\mathrm{Ind}(C))$$$

Lean4

instance : HasFilteredColimits (Ind C) where
  HasColimitsOfShape _ _ _ := hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape (Ind.inclusion C)

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