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-simplices of SimplicialNerve C may be identified with the objects of C
• Prove that the 1-simplices 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][LurieHTT]

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

• as : J

  The underlying object of the linear order.

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 : Path i j} (I : x.I = y.I) : x = y

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

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

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

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

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

Equations

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

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

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

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

Equations

• CategoryTheory.SimplicialThickening.instCategory J = { toCategoryStruct := CategoryTheory.SimplicialThickening.instCategoryStruct J, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }

def CategoryTheory.SimplicialThickening.compFunctor {J : Type u_1} [LinearOrder J] (i j k : SimplicialThickening J) : 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 : SimplicialThickening J) (x : (i ⟶ j) × (j ⟶ k)) : (i.compFunctor j k).obj x = CategoryStruct.comp x.1 x.2

@[reducible, inline]

abbrev CategoryTheory.SimplicialThickening.SimplicialCategory.Hom {J : Type u_1} [LinearOrder J] (i j : 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 : SimplicialThickening J) : MonoidalCategoryStruct.tensorUnit SSet ⟶ 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 : SimplicialThickening J) : MonoidalCategoryStruct.tensorObj (Hom i j) (Hom j k) ⟶ 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 : SimplicialThickening J) : CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (Hom i j)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (id i) (Hom i j)) (comp i i j)) = CategoryStruct.id (Hom i j)

@[simp]

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

@[simp]

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

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

Equations

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

@[reducible, inline]

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

Auxiliary definition for SimplicialThickening.functor

Equations

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

@[deprecated CategoryTheory.SimplicialThickening.functorMap "No replacement, was using a bad instance" (since := "01-12-2026")]

def CategoryTheory.SimplicialThickening.orderHom {J K : Type u} [LinearOrder J] [LinearOrder K] (f : J →o K) (i j : SimplicialThickening J) : Functor (i ⟶ j) ({ as := f i.as } ⟶ { as := f j.as })

Alias of CategoryTheory.SimplicialThickening.functorMap.

---

Auxiliary definition for SimplicialThickening.functor

Equations

• @CategoryTheory.SimplicialThickening.orderHom = @CategoryTheory.SimplicialThickening.functorMap

noncomputable def CategoryTheory.SimplicialThickening.functor {J K : Type u} [LinearOrder J] [LinearOrder K] (f : J →o K) : EnrichedFunctor SSet (SimplicialThickening J) (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 : SimplicialThickening J) : (functor f).map i j = nerveMap (functorMap f i j)

@[simp]

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

theorem CategoryTheory.SimplicialThickening.functor_id (J : Type u) [LinearOrder J] : functor OrderHom.id = EnrichedFunctor.id SSet (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) : functor (g.comp f) = EnrichedFunctor.comp SSet (functor f) (functor g)

noncomputable def CategoryTheory.SimplicialNerve (C : Type u) [Category.{v, u} C] [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.