English
The n-skeleton can be viewed as an endofunctor on SimplicialObject: sk(n) : SimplicialObject C ⥤ SimplicialObject C, via truncation n followed by Truncated.sk n.
Русский
Скелетон уровня n рассматривается как эндофунктор на SimplicialObject: sk(n) : SimplicialObject C ⥤ SimplicialObject C, через усечение n и затем Truncated.sk n.
LaTeX
$$$$ \\mathrm{sk}(n) : \\mathrm{SimplicialObject}\\, C \\longrightarrow \\mathrm{SimplicialObject}\\, C \\;:=\\; \\mathrm{truncation}(n) \\;\\circ\\; \\mathrm{Truncated}.\\mathrm{sk}\\ n $$$$
Lean4
/-- The n-skeleton as an endofunctor on `SimplicialObject C`. -/
abbrev sk (n : ℕ)
[∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F] :
SimplicialObject C ⥤ SimplicialObject C :=
truncation n ⋙ Truncated.sk n
