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