truncationCompTrunc — Mathlib

English

If C has colimits, then CosimplicialObject.Truncated C n has colimits; this provides a canonical way to compute colimits in truncated cosimplicial objects using those in C.

Русский

Если в C есть копределы, то CosimplicialObject.Truncated C n имеет копределы; это даёт способ вычисления копределов в усечённых косипликсоподобных объектах через копределы в C.

LaTeX

$$$[HasColimits C] \Rightarrow HasColimits (\mathrm{CosimplicialObject.Truncated } C\ n).$$$

Lean4

/-- For all `m ≤ n`, `truncation m` factors through `Truncated n`. -/
def truncationCompTrunc {n m : ℕ} (h : m ≤ n) : truncation n ⋙ Truncated.trunc C n m ≅ truncation m :=
  Iso.refl _

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