instHasColimits — Mathlib

English

The truncated construction preserves both limits and colimits: if C has limits, then CosimplicialObject.Truncated C n has limits; if C has colimits, then CosimplicialObject.Truncated C n has colimits.

Русский

Усечение сохраняет пределы и копределы: если в C существуют пределы, то CosimplicialObject.Truncated C n имеет пределы; если существуют копределы, то есть копределы.

LaTeX

$$$\text{HasLimits } C \Rightarrow \text{HasLimits } (\mathrm{CosimplicialObject.Truncated } C\ n), \quad \text{HasColimits } C \Rightarrow \text{HasColimits } (\mathrm{CosimplicialObject.Truncated } C\ n).$$$

Lean4

instance {n} [HasColimits C] : HasColimits (CosimplicialObject.Truncated C n) :=
  ⟨inferInstance⟩

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