hasColimitsOfShape_of_has_filtered_colimits

English

If C has filtered colimits of a given size, then for any I that is filtered, C has colimits of shape I.

Русский

Если в C существуют отфильтрованные колимиты заданного размера, то для любого I, являющегося фильтрованным, C имеет колимиты по форме I.

LaTeX

$$$[HasFilteredColimitsOfSize C] \Rightarrow [HasColimitsOfShape I C]$ for IsFiltered I$$

Lean4

instance (priority := 100) hasColimitsOfShape_of_has_filtered_colimits [HasFilteredColimitsOfSize.{w', w} C]
    (I : Type w) [Category.{w'} I] [IsFiltered I] : HasColimitsOfShape I C :=
  HasFilteredColimitsOfSize.HasColimitsOfShape _

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