Theorems · Definition · category theory

CategoryTheory.SimplicialObject.IsCoskeletal.isUniversalOfIsRightKanExtension

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : CategoryTheory.SimplicialObject C) →
      (n : ℕ) →
        [X.IsCoskeletal n] →
          CategoryTheory.CostructuredArrow.IsUniversal
            (CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion X n)

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).

Defined in

Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal

Cited by

0 results in Mathlib

Foundations

Depth 33 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.SimplicialObject.IsCoskeletal