The simplicial nerve of a simplicial category

This file defines the simplicial nerve (sometimes called homotopy coherent nerve) of a simplicial category.

We define the simplicial thickening of a linear order J as the simplicial category whose hom objects i ⟶ j are given by the nerve of the poset of "paths" from i to j in J. This is the poset of subsets of the interval [i, j] in J, containing the endpoints.

The simplicial nerve of a simplicial category C is then defined as the simplicial set whose n-simplices are given by the set of simplicial functors from the simplicial thickening of the linear order Fin (n + 1) to C, in other words SimplicialNerve C _[n] := EnrichedFunctor SSet (SimplicialThickening (Fin (n + 1))) C.

Projects

• Prove that the 0-simplicies of SimplicialNerve C may be identified with the objects of C
• Prove that the 1-simplicies of SimplicialNerve C may be identified with the morphisms of C
• Prove that the simplicial nerve of a simplicial category C, such that sHom X Y is a Kan complex for every pair of objects X Y : C, is a quasicategory.
• Define the quasicategory of anima as the simplicial nerve of the simplicial category of Kan complexes.
• Define the functor from topological spaces to anima.

References

• Jacob Lurie, Higher Topos Theory, Section 1.1.5

def CategoryTheory.SimplicialThickening (J : Type u_1) [LinearOrder J] : Type u_1

A type synonym for a linear order J, will be equipped with a simplicial category structure.

Equations

• CategoryTheory.SimplicialThickening J = J

instance CategoryTheory.instLinearOrderSimplicialThickening (J : Type u_1) [LinearOrder J] : LinearOrder (CategoryTheory.SimplicialThickening J)

Equations

• CategoryTheory.instLinearOrderSimplicialThickening J = inferInstanceAs (LinearOrder J)

structure CategoryTheory.SimplicialThickening.Path {J : Type u_1} [LinearOrder J] (i j : J) : Type u_1

A path from i to j in a linear order J is a subset of the interval [i, j] in J containing the endpoints.

• I : Set J

  The underlying subset

• left : i ∈ self.I
• right : j ∈ self.I
• left_le (k : J) : k ∈ self.I → i ≤ k
• le_right (k : J) : k ∈ self.I → k ≤ j

theorem CategoryTheory.SimplicialThickening.Path.ext {J : Type u_1} {inst✝ : LinearOrder J} {i j : J} {x y : CategoryTheory.SimplicialThickening.Path i j} (I : x.I = y.I) : x = y

theorem CategoryTheory.SimplicialThickening.Path.le {J : Type u_1} [LinearOrder J] {i j : J} (f : CategoryTheory.SimplicialThickening.Path i j) : i ≤ j

instance CategoryTheory.SimplicialThickening.instCategoryPath {J : Type u_1} [LinearOrder J] (i j : J) : CategoryTheory.Category.{u_1, u_1} (CategoryTheory.SimplicialThickening.Path i j)

Equations

• CategoryTheory.SimplicialThickening.instCategoryPath i j = CategoryTheory.InducedCategory.category fun (f : CategoryTheory.SimplicialThickening.Path i j) => f.I

instance CategoryTheory.SimplicialThickening.instCategoryStruct (J : Type u_1) [LinearOrder J] : CategoryTheory.CategoryStruct.{u_1, u_1} (CategoryTheory.SimplicialThickening J)

Equations

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

@[simp]

theorem CategoryTheory.SimplicialThickening.instCategoryStruct_id_I (J : Type u_1) [LinearOrder J] (i : CategoryTheory.SimplicialThickening J) : (CategoryTheory.CategoryStruct.id i).I = {i}

@[simp]

theorem CategoryTheory.SimplicialThickening.instCategoryStruct_Hom (J : Type u_1) [LinearOrder J] (i j : CategoryTheory.SimplicialThickening J) : (i ⟶ j) = CategoryTheory.SimplicialThickening.Path i j

@[simp]

theorem CategoryTheory.SimplicialThickening.instCategoryStruct_comp_I (J : Type u_1) [LinearOrder J] {i j k : CategoryTheory.SimplicialThickening J} (f : i ⟶ j) (g : j ⟶ k) : (CategoryTheory.CategoryStruct.comp f g).I = f.I ∪ g.I

instance CategoryTheory.SimplicialThickening.instCategoryHom {J : Type u_1} [LinearOrder J] (i j : CategoryTheory.SimplicialThickening J) : CategoryTheory.Category.{u_1, u_1} (i ⟶ j)

Equations

• i.instCategoryHom j = inferInstanceAs (CategoryTheory.Category.{?u.31, ?u.31} (CategoryTheory.SimplicialThickening.Path i j))

theorem CategoryTheory.SimplicialThickening.hom_ext {J : Type u_1} [LinearOrder J] (i j : CategoryTheory.SimplicialThickening J) (x y : i ⟶ j) (h : ∀ (t : CategoryTheory.SimplicialThickening J), t ∈ x.I ↔ t ∈ y.I) : x = y

instance CategoryTheory.SimplicialThickening.instCategory (J : Type u_1) [LinearOrder J] : CategoryTheory.Category.{u_1, u_1} (CategoryTheory.SimplicialThickening J)

Equations

• CategoryTheory.SimplicialThickening.instCategory J = CategoryTheory.Category.mk ⋯ ⋯ ⋯

def CategoryTheory.SimplicialThickening.compFunctor {J : Type u_1} [LinearOrder J] (i j k : CategoryTheory.SimplicialThickening J) : CategoryTheory.Functor ((i ⟶ j) × (j ⟶ k)) (i ⟶ k)

Composition of morphisms in SimplicialThickening J, as a functor (i ⟶ j) × (j ⟶ k) ⥤ (i ⟶ k)

Equations

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

@[simp]

theorem CategoryTheory.SimplicialThickening.compFunctor_obj {J : Type u_1} [LinearOrder J] (i j k : CategoryTheory.SimplicialThickening J) (x : (i ⟶ j) × (j ⟶ k)) : (i.compFunctor j k).obj x = CategoryTheory.CategoryStruct.comp x.1 x.2

@[simp]

theorem CategoryTheory.SimplicialThickening.compFunctor_map_down_down {J : Type u_1} [LinearOrder J] (i j k : CategoryTheory.SimplicialThickening J) {X✝ Y✝ : (i ⟶ j) × (j ⟶ k)} (f : X✝ ⟶ Y✝) : ⋯ = ⋯

@[reducible, inline]

abbrev CategoryTheory.SimplicialThickening.SimplicialCategory.Hom {J : Type u_1} [LinearOrder J] (i j : CategoryTheory.SimplicialThickening J) : SSet

The hom simplicial set of the simplicial category structure on SimplicialThickening J

Equations

• CategoryTheory.SimplicialThickening.SimplicialCategory.Hom i j = CategoryTheory.nerve (i ⟶ j)

@[reducible, inline]

abbrev CategoryTheory.SimplicialThickening.SimplicialCategory.id {J : Type u_1} [LinearOrder J] (i : CategoryTheory.SimplicialThickening J) : 𝟙_ SSet ⟶ CategoryTheory.SimplicialThickening.SimplicialCategory.Hom i i

The identity of the simplicial category structure on SimplicialThickening J

Equations

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

@[reducible, inline]

abbrev CategoryTheory.SimplicialThickening.SimplicialCategory.comp {J : Type u_1} [LinearOrder J] (i j k : CategoryTheory.SimplicialThickening J) : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.SimplicialThickening.SimplicialCategory.Hom i j) (CategoryTheory.SimplicialThickening.SimplicialCategory.Hom j k) ⟶ CategoryTheory.SimplicialThickening.SimplicialCategory.Hom i k

The composition of the simplicial category structure on SimplicialThickening J

Equations

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

@[simp]

theorem CategoryTheory.SimplicialThickening.SimplicialCategory.id_comp {J : Type u_1} [LinearOrder J] (i j : CategoryTheory.SimplicialThickening J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.SimplicialThickening.SimplicialCategory.Hom i j)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.SimplicialThickening.SimplicialCategory.id i) (CategoryTheory.SimplicialThickening.SimplicialCategory.Hom i j)) (CategoryTheory.SimplicialThickening.SimplicialCategory.comp i i j)) = CategoryTheory.CategoryStruct.id (CategoryTheory.SimplicialThickening.SimplicialCategory.Hom i j)

@[simp]

theorem CategoryTheory.SimplicialThickening.SimplicialCategory.comp_id {J : Type u_1} [LinearOrder J] (i j : CategoryTheory.SimplicialThickening J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor (CategoryTheory.SimplicialThickening.SimplicialCategory.Hom i j)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.SimplicialThickening.SimplicialCategory.Hom i j) (CategoryTheory.SimplicialThickening.SimplicialCategory.id j)) (CategoryTheory.SimplicialThickening.SimplicialCategory.comp i j j)) = CategoryTheory.CategoryStruct.id (CategoryTheory.SimplicialThickening.SimplicialCategory.Hom i j)

@[simp]

theorem CategoryTheory.SimplicialThickening.SimplicialCategory.assoc {J : Type u_1} [LinearOrder J] (i j k l : CategoryTheory.SimplicialThickening J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (CategoryTheory.SimplicialThickening.SimplicialCategory.Hom i j) (CategoryTheory.SimplicialThickening.SimplicialCategory.Hom j k) (CategoryTheory.SimplicialThickening.SimplicialCategory.Hom k l)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.SimplicialThickening.SimplicialCategory.comp i j k) (CategoryTheory.SimplicialThickening.SimplicialCategory.Hom k l)) (CategoryTheory.SimplicialThickening.SimplicialCategory.comp i k l)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.SimplicialThickening.SimplicialCategory.Hom i j) (CategoryTheory.SimplicialThickening.SimplicialCategory.comp j k l)) (CategoryTheory.SimplicialThickening.SimplicialCategory.comp i j l)

noncomputable instance CategoryTheory.SimplicialThickening.instSimplicialCategory (J : Type u_1) [LinearOrder J] : CategoryTheory.SimplicialCategory (CategoryTheory.SimplicialThickening J)

Equations

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

def CategoryTheory.SimplicialThickening.orderHom {J : Type u_1} {K : Type u_2} [LinearOrder J] [LinearOrder K] (f : J →o K) : CategoryTheory.SimplicialThickening J →o CategoryTheory.SimplicialThickening K

Auxiliary definition for SimplicialThickening.functorMap

Equations

• CategoryTheory.SimplicialThickening.orderHom f = f

@[reducible, inline]

noncomputable abbrev CategoryTheory.SimplicialThickening.functorMap {J K : Type u} [LinearOrder J] [LinearOrder K] (f : J →o K) (i j : CategoryTheory.SimplicialThickening J) : CategoryTheory.Functor (i ⟶ j) ((CategoryTheory.SimplicialThickening.orderHom f) i ⟶ (CategoryTheory.SimplicialThickening.orderHom f) j)

Auxiliary definition for SimplicialThickening.functor

Equations

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

noncomputable def CategoryTheory.SimplicialThickening.functor {J K : Type u} [LinearOrder J] [LinearOrder K] (f : J →o K) : CategoryTheory.EnrichedFunctor SSet (CategoryTheory.SimplicialThickening J) (CategoryTheory.SimplicialThickening K)

The simplicial thickening defines a functor from the category of linear orders to the category of simplicial categories

Equations

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

@[simp]

theorem CategoryTheory.SimplicialThickening.functor_map {J K : Type u} [LinearOrder J] [LinearOrder K] (f : J →o K) (i j : CategoryTheory.SimplicialThickening J) : (CategoryTheory.SimplicialThickening.functor f).map i j = CategoryTheory.nerveMap (CategoryTheory.SimplicialThickening.functorMap f i j)

@[simp]

theorem CategoryTheory.SimplicialThickening.functor_obj {J K : Type u} [LinearOrder J] [LinearOrder K] (f : J →o K) (a : J) : (CategoryTheory.SimplicialThickening.functor f).obj a = f a

theorem CategoryTheory.SimplicialThickening.functor_id (J : Type u) [LinearOrder J] : CategoryTheory.SimplicialThickening.functor OrderHom.id = CategoryTheory.EnrichedFunctor.id SSet (CategoryTheory.SimplicialThickening J)

theorem CategoryTheory.SimplicialThickening.functor_comp {J K L : Type u} [LinearOrder J] [LinearOrder K] [LinearOrder L] (f : J →o K) (g : K →o L) : CategoryTheory.SimplicialThickening.functor (g.comp f) = CategoryTheory.EnrichedFunctor.comp SSet (CategoryTheory.SimplicialThickening.functor f) (CategoryTheory.SimplicialThickening.functor g)

noncomputable def CategoryTheory.SimplicialNerve (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.SimplicialCategory C] : SSet

The simplicial nerve of a simplicial category C is defined as the simplicial set whose n-simplices are given by the set of simplicial functors from the simplicial thickening of the linear order Fin (n + 1) to C

Equations

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