has_colimits_of_finite_and_filtered

English

If C has finite coproducts and HasFilteredColimitsOfSize, then C has coproducts of every small size; i.e., HasCoproducts of size w.

Русский

Если в C существуют конечные копроизводы и имеет HasFilteredColimitsOfSize, то C имеет копроизводы для всех малых размеров; то есть HasCoproducts размерa w.

LaTeX

$$$$ \text{hasCoproducts_of_finite_and_filtered} \;:\; [HasFiniteCoproducts\, C] \to [HasFilteredColimitsOfSize\{w,w\}\, C] \to [HasCoproducts\, C]. $$$$

Lean4

theorem has_colimits_of_finite_and_filtered [HasFiniteColimits C] [HasFilteredColimitsOfSize.{w, w} C] :
    HasColimitsOfSize.{w, w} C :=
  have : HasCoproducts.{w} C := hasCoproducts_of_finite_and_filtered
  has_colimits_of_hasCoequalizers_and_coproducts

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