Coskeletal simplicial sets

In this file, we prove that if X is StrictSegal then X is 2-coskeletal, i.e. X ≅ (cosk 2).obj X. In particular, nerves of categories are 2-coskeletal.

This isomorphism follows from the fact that rightExtensionInclusion X 2 is a right Kan extension. In fact, we show that when X is StrictSegal then (rightExtensionInclusion X n).IsPointwiseRightKanExtension holds.

As an example, SimplicialObject.IsCoskeletal (nerve C) 2 shows that that nerves of categories are 2-coskeletal.

def SSet.Truncated.rightExtensionInclusion (X : SSet) (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 := n)).op.

@[simp]

theorem SSet.Truncated.rightExtensionInclusion_right_as (X : SSet) (n : ℕ) : (rightExtensionInclusion X n).right.as = PUnit.unit

@[simp]

theorem SSet.Truncated.rightExtensionInclusion_left (X : SSet) (n : ℕ) : (rightExtensionInclusion X n).left = X

@[simp]

theorem SSet.Truncated.rightExtensionInclusion_hom_app (X : SSet) (n : ℕ) (X✝ : (SimplexCategory.Truncated n)ᵒᵖ) (a✝ : ((SimplexCategory.Truncated.inclusion n).op.comp X).obj X✝) : (rightExtensionInclusion X n).hom.app X✝ a✝ = a✝

@[reducible, inline]

abbrev SSet.StrictSegal.isPointwiseRightKanExtensionAt.strArrowMk₂ {i n : ℕ} (φ : SimplexCategory.mk i ⟶ SimplexCategory.mk n) (hi : i ≤ 2 := by omega) : CategoryTheory.StructuredArrow (Opposite.op (SimplexCategory.mk n)) (SimplexCategory.Truncated.inclusion 2).op

A morphism in SimplexCategory with domain ⦋0⦌, ⦋1⦌, or ⦋2⦌ defines an object in the comma category StructuredArrow (op ⦋n⦌) (Truncated.inclusion (n := 2)).op.

noncomputable def SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift {X : SSet} (sx : X.StrictSegal) {n : ℕ} (s : CategoryTheory.Limits.Cone ((CategoryTheory.StructuredArrow.proj (Opposite.op (SimplexCategory.mk n)) (SimplexCategory.Truncated.inclusion 2).op).comp ((SimplexCategory.Truncated.inclusion 2).op.comp X))) (x : s.pt) : X.obj (Opposite.op (SimplexCategory.mk n))

Given a term in the cone over the diagram (proj (op ⦋n⦌) ((Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X) where X is Strict Segal, one can produce an n-simplex in X.

theorem SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₁ {X : SSet} (sx : X.StrictSegal) {n : ℕ} (s : CategoryTheory.Limits.Cone ((CategoryTheory.StructuredArrow.proj (Opposite.op (SimplexCategory.mk n)) (SimplexCategory.Truncated.inclusion 2).op).comp ((SimplexCategory.Truncated.inclusion 2).op.comp X))) (x : s.pt) (i : ℕ) (hi : i < n) : X.map (SimplexCategory.mkOfSucc ⟨i, hi⟩).op (lift sx s x) = s.π.app (strArrowMk₂ (SimplexCategory.mkOfSucc ⟨i, hi⟩) ⋯) x

theorem SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₂ {X : SSet} (sx : X.StrictSegal) {n : ℕ} (s : CategoryTheory.Limits.Cone ((CategoryTheory.StructuredArrow.proj (Opposite.op (SimplexCategory.mk n)) (SimplexCategory.Truncated.inclusion 2).op).comp ((SimplexCategory.Truncated.inclusion 2).op.comp X))) (x : s.pt) (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n) : X.map (SimplexCategory.mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op (lift sx s x) = s.π.app (strArrowMk₂ (SimplexCategory.mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) ⋯) x

theorem SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₃ {X : SSet} (sx : X.StrictSegal) {n : ℕ} (s : CategoryTheory.Limits.Cone ((CategoryTheory.StructuredArrow.proj (Opposite.op (SimplexCategory.mk n)) (SimplexCategory.Truncated.inclusion 2).op).comp ((SimplexCategory.Truncated.inclusion 2).op.comp X))) (x : s.pt) (φ : SimplexCategory.mk 1 ⟶ SimplexCategory.mk n) : X.map φ.op (lift sx s x) = s.π.app (strArrowMk₂ φ ⋯) x

noncomputable def SSet.StrictSegal.isPointwiseRightKanExtensionAt {X : SSet} (sx : X.StrictSegal) (n : ℕ) : (Truncated.rightExtensionInclusion X 2).IsPointwiseRightKanExtensionAt (Opposite.op (SimplexCategory.mk n))

A strict Segal simplicial set is 2-coskeletal.

noncomputable def SSet.StrictSegal.isPointwiseRightKanExtension {X : SSet} (sx : X.StrictSegal) : (Truncated.rightExtensionInclusion X 2).IsPointwiseRightKanExtension

Since StrictSegal.isPointwiseRightKanExtensionAt proves that the appropriate cones are limit cones, rightExtensionInclusion X 2 is a pointwise right Kan extension.

theorem SSet.StrictSegal.isRightKanExtension {X : SSet} (sx : X.StrictSegal) : CategoryTheory.Functor.IsRightKanExtension X (CategoryTheory.CategoryStruct.id ((SimplexCategory.Truncated.inclusion 2).op.comp X))

theorem SSet.StrictSegal.isCoskeletal {X : SSet} (sx : X.StrictSegal) : CategoryTheory.SimplicialObject.IsCoskeletal X 2

When X is StrictSegal, X is 2-coskeletal.

instance SSet.StrictSegal.isCoskeletal' {X : SSet} [X.IsStrictSegal] : CategoryTheory.SimplicialObject.IsCoskeletal X 2

When X satisfies IsStrictSegal, X is 2-coskeletal.

instance CategoryTheory.Nerve.instIsCoskeletalNerveOfNatNat (C : Type u) [Category.{v, u} C] : SimplicialObject.IsCoskeletal (nerve C) 2

def CategoryTheory.Nerve.nerveFunctor₂ : Functor Cat (SSet.Truncated 2)

The essential data of the nerve functor is contained in the 2-truncation, which is recorded by the composite functor nerveFunctor₂.

noncomputable def CategoryTheory.Nerve.cosk₂Iso : nerveFunctor ≅ nerveFunctor₂.comp (SSet.Truncated.cosk 2)

The natural isomorphism between nerveFunctor and nerveFunctor₂ ⋙ Truncated.cosk 2 whose components nerve C ≅ (Truncated.cosk 2).obj (nerveFunctor₂.obj C) shows that nerves of categories are 2-coskeletal.