Coskeletal simplicial objects #

The identity natural transformation exhibits a simplicial object X as a right extension of its restriction along (Truncated.inclusion n).op recorded by rightExtensionInclusion X n.

The simplicial object X is n-coskeletal if rightExtensionInclusion X n is a right Kan extension.

When the ambient category admits right Kan extensions along (Truncated.inclusion n).op, then when X is n-coskeletal, the unit of coskAdj n defines an isomorphism: isoCoskOfIsCoskeletal : X ≅ (cosk n).obj X.

TODO: Prove that X is n-coskeletal whenever a certain canonical cone is a limit cone.

source

def CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion {C : Type u} [Category.{v, u} C] (X : SimplicialObject C) (n : ℕ) :

(SimplexCategory.Truncated.inclusion n).op.RightExtension ((SimplexCategory.Truncated.inclusion n).op.comp X)

The identity natural transformation exhibits a simplicial set as a right extension of its restriction along (Truncated.inclusion n).op.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion_hom_app {C : Type u} [Category.{v, u} C] (X : SimplicialObject C) (n : ℕ) (X✝ : (SimplexCategory.Truncated n)ᵒᵖ) :

(rightExtensionInclusion X n).hom.app X✝ = CategoryStruct.id (X.obj (Opposite.op ((SimplexCategory.Truncated.inclusion n).obj (Opposite.unop X✝))))

source

@[simp]

theorem CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion_left {C : Type u} [Category.{v, u} C] (X : SimplicialObject C) (n : ℕ) :

(rightExtensionInclusion X n).left = X

source

@[simp]

theorem CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion_right_as {C : Type u} [Category.{v, u} C] (X : SimplicialObject C) (n : ℕ) :

(rightExtensionInclusion X n).right.as = PUnit.unit

source

class CategoryTheory.SimplicialObject.IsCoskeletal {C : Type u} [Category.{v, u} C] (X : SimplicialObject C) (n : ℕ) :

Prop

A simplicial object X is n-coskeletal when it is the right Kan extension of its restriction along (Truncated.inclusion n).op via the identity natural transformation.

isRightKanExtension : Functor.IsRightKanExtension X (CategoryStruct.id ((SimplexCategory.Truncated.inclusion n).op.comp X))

Instances

source

theorem CategoryTheory.SimplicialObject.isCoskeletal_iff {C : Type u} [Category.{v, u} C] (X : SimplicialObject C) (n : ℕ) :

X.IsCoskeletal n ↔ Functor.IsRightKanExtension X (CategoryStruct.id ((SimplexCategory.Truncated.inclusion n).op.comp X))

source

noncomputable def CategoryTheory.SimplicialObject.IsCoskeletal.isUniversalOfIsRightKanExtension {C : Type u} [Category.{v, u} C] (X : SimplicialObject C) (n : ℕ) [X.IsCoskeletal n] :

CostructuredArrow.IsUniversal (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).

Equations