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.

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.

@[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✝))))

@[simp]

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

@[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

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

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

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

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

theorem CategoryTheory.SimplicialObject.isCoskeletal_iff_isIso {C : Type u} [Category.{v, u} C] (X : SimplicialObject C) (n : ℕ) [∀ (F : Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F] : X.IsCoskeletal n ↔ IsIso ((coskAdj n).unit.app X)

instance CategoryTheory.SimplicialObject.instIsIsoAppUnitTruncatedCoskAdj {C : Type u} [Category.{v, u} C] (X : SimplicialObject C) (n : ℕ) [∀ (F : Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F] [X.IsCoskeletal n] : IsIso ((coskAdj n).unit.app X)

noncomputable def CategoryTheory.SimplicialObject.isoCoskOfIsCoskeletal {C : Type u} [Category.{v, u} C] (X : SimplicialObject C) (n : ℕ) [∀ (F : Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F] [X.IsCoskeletal n] : X ≅ (cosk n).obj X

The canonical isomorphism X ≅ (cosk n).obj X defined when X is coskeletal and the n-coskeleton functor exists.

Equations

• X.isoCoskOfIsCoskeletal n = CategoryTheory.asIso ((CategoryTheory.SimplicialObject.coskAdj n).unit.app X)

@[simp]

theorem CategoryTheory.SimplicialObject.isoCoskOfIsCoskeletal_hom {C : Type u} [Category.{v, u} C] (X : SimplicialObject C) (n : ℕ) [∀ (F : Functor (SimplexCategory.Truncated n)ᵒᵖ C), (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F] [X.IsCoskeletal n] : (X.isoCoskOfIsCoskeletal n).hom = (coskAdj n).unit.app X