isUniversalOfIsRightKanExtension — Mathlib

English

If X is n-coskeletal, then the right extension of Truncated.inclusion n along op X is universal as a right Kan extension; i.e., the corresponding object is terminal in the relevant comma/costructured arrow category.

Русский

Если X является n-кососкелетным, то правое продолжение along Truncated.inclusion n образует универсальный правый Кан-расширение; то есть соответствующий объект является терминальным в соответствующей категории Comma/Costructured Arrow.

LaTeX

$$$[X.IsCoskeletal\ n] \Rightarrow (\text{rightExtensionInclusion } X\ n).IsUniversal.$$$

Lean4

/-- If `X` is `n`-coskeletal, then `Truncated.rightExtensionInclusion X n` is a terminal object in
the category `RightExtension (Truncated.inclusion n).op (Truncated.inclusion.op ⋙ X)`. -/
noncomputable def isUniversalOfIsRightKanExtension [X.IsCoskeletal n] : (rightExtensionInclusion X n).IsUniversal := by
  apply Functor.isUniversalOfIsRightKanExtension

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