English
For SimplicialObject C, the n-coskeleton is an endofunctor: cosk(n) : SimplicialObject.Truncated C n ⥤ SimplicialObject C, defined via the right Kan extension ran along the truncated inclusion.
Русский
Для симплициального объекта C коскелетон уровня n образует эндофунктор: cosk(n) : SimplicialObject.Truncated C n ⥤ SimplicialObject C, задаётся через правый кан-расширение вдоль усечённого включения.
LaTeX
$$$$ \\mathrm{cosk}(n) : \\mathrm{SimplicialObject.Truncated}\\, C\\ n \\longrightarrow \\mathrm{SimplicialObject}\\, C \\;:=\\; \\mathrm{ran}((\\mathrm{SimplexCategory.Truncated.inclusion}\\ n)^{\\mathrm{op}}) $$$$
Lean4
/-- The n-coskeleton as a functor `SimplicialObject.Truncated C n ⥤ SimplicialObject C`. -/
protected abbrev cosk (n : ℕ)
[∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F] :
SimplicialObject.Truncated C n ⥤ SimplicialObject C :=
ran (SimplexCategory.Truncated.inclusion n).op
