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.

Equations

• SSet.Truncated.rightExtensionInclusion X n = CategoryTheory.Functor.RightExtension.mk X (CategoryTheory.CategoryStruct.id ((SimplexCategory.Truncated.inclusion n).op.comp X))

@[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) : 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.

Equations

• SSet.StrictSegal.isPointwiseRightKanExtensionAt.strArrowMk₂ φ hi = CategoryTheory.StructuredArrow.mk φ.op

noncomputable def SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift {X : SSet} [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.

Equations

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

theorem SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₁ (X : SSet) [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 s x) = s.π.app (strArrowMk₂ (SimplexCategory.mkOfSucc ⟨i, hi⟩) ⋯) x

theorem SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₂ (X : SSet) [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 s x) = s.π.app (strArrowMk₂ (SimplexCategory.mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) ⋯) x

theorem SSet.StrictSegal.isPointwiseRightKanExtensionAt.fac_aux₃ (X : SSet) [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 s x) = s.π.app (strArrowMk₂ φ ⋯) x

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

A strict Segal simplicial set is 2-coskeletal.

Equations

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

noncomputable def SSet.StrictSegal.isPointwiseRightKanExtension (X : SSet) [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.

Equations

• SSet.StrictSegal.isPointwiseRightKanExtension X Δ = SSet.StrictSegal.isPointwiseRightKanExtensionAt X (Opposite.unop Δ).len

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

instance SSet.StrictSegal.isCoskeletal (X : SSet) [X.StrictSegal] : CategoryTheory.SimplicialObject.IsCoskeletal X 2

When X is StrictSegal, X is 2-coskeletal.

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

Equations

• CategoryTheory.Nerve.nerveFunctor₂ = CategoryTheory.nerveFunctor.comp (SSet.truncation 2)

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.

Equations

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