instHasFiniteColimits — Mathlib

English

If the base category C has finite colimits, then the category of HomologicalComplex C c has finite colimits as well (pointwise construction).

Русский

Если база C имеет конечные колимиты, то категория гомологического комплекса HC имеет конечные колимиты (построение по точкам).

LaTeX

$$$\operatorname{HasFiniteColimits}(\mathrm{HomologicalComplex}(C,c))$$$

Lean4

instance [HasFiniteColimits C] : HasFiniteColimits (HomologicalComplex C c) :=
  ⟨fun _ _ => inferInstance⟩

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