truncation — Mathlib

English

There is a functor that sends a simplicial object in C to its truncated version in SimplicialObject.Truncated C n, preserving structure up to level n.

Русский

Существует функтор, переводящий симплициальный объект в C в усечённый симплициальный объект в SimplicialObject.Truncated C n, сохраняя структуру до уровня n.

LaTeX

$$$$ \\mathrm{truncation}(n) : \\mathrm{SimplicialObject}\\, C \\longrightarrow \\mathrm{SimplicialObject.Truncated}\\, C\\ n $$$$

Lean4

/-- The truncation functor from simplicial objects to truncated simplicial objects. -/
def truncation (n : ℕ) : SimplicialObject C ⥤ SimplicialObject.Truncated C n :=
  (whiskeringLeft _ _ _).obj (SimplexCategory.Truncated.inclusion n).op

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