truncation — Mathlib

English

For each n, there is a functor truncation_n: SSet → SSet.Truncated(n) that assigns to a simplicial set its n-truncated version.

Русский

Для каждого n существует функтор truncation_n: SSet → SSet.Truncated(n), который присваивает симпликсальному множеству его n-усечение.

LaTeX

$$$\mathrm{truncation}_n: \mathrm{SSet} \to \mathrm{SSet.Truncated}(n)$$$

Lean4

/-- The truncation functor on simplicial sets. -/
abbrev truncation (n : ℕ) : SSet ⥤ SSet.Truncated n :=
  SimplicialObject.truncation n

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