English
For SimplicialObject C, the n-skeleton is an endofunctor: sk(n) : SimplicialObject C ⥤ SimplicialObject C, defined by composing truncation with the truncated-sk construction.
Русский
Для симпликциального объекта C скелет в уровне n образует эндофунктор: sk(n) : SimplicialObject C ⥤ SimplicialObject C, задаётся как композиция усечения и конструкции усечённого скелета.
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 a functor `SimplicialObject.Truncated C n ⥤ SimplicialObject C`. -/
protected abbrev sk (n : ℕ)
[∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F] :
SimplicialObject.Truncated C n ⥤ SimplicialObject C :=
lan (SimplexCategory.Truncated.inclusion n).op
