The nerve of a category

This file provides the definition of the nerve of a category C, which is a simplicial set nerve C (see [goerss-jardine-2009], Example I.1.4). By definition, the type of n-simplices of nerve C is ComposableArrows C n, which is the category Fin (n + 1) ⥤ C.

References

• [Paul G. Goerss, John F. Jardine, Simplicial Homotopy Theory][goerss-jardine-2009]

@[simp]

theorem CategoryTheory.nerve_obj (C : Type u) [CategoryTheory.Category.{v, u} C] (Δ : SimplexCategoryᵒᵖ) : (CategoryTheory.nerve C).obj Δ = CategoryTheory.ComposableArrows C (Opposite.unop Δ).len

@[simp]

theorem CategoryTheory.nerve_map (C : Type u) [CategoryTheory.Category.{v, u} C] : ∀ {X Y : SimplexCategoryᵒᵖ} (f : X ⟶ Y) (x : CategoryTheory.ComposableArrows C (Opposite.unop X).len), (CategoryTheory.nerve C).map f x = x.whiskerLeft (SimplexCategory.toCat.map f.unop)

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

The nerve of a category

Equations

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

instance CategoryTheory.instCategoryObjOppositeSimplexCategoryNerve {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {Δ : SimplexCategoryᵒᵖ} : CategoryTheory.Category.{u_2, max u_1 u_2} ((CategoryTheory.nerve C).obj Δ)

Equations

• CategoryTheory.instCategoryObjOppositeSimplexCategoryNerve = inferInstance

@[simp]

theorem CategoryTheory.nerveFunctor_obj (C : CategoryTheory.Cat) : CategoryTheory.nerveFunctor.obj C = CategoryTheory.nerve ↑C

@[simp]

theorem CategoryTheory.nerveFunctor_map_app : ∀ {X Y : CategoryTheory.Cat} (F : X ⟶ Y) (Δ : SimplexCategoryᵒᵖ) (a : CategoryTheory.ComposableArrows (↑X) (Opposite.unop Δ).len), (CategoryTheory.nerveFunctor.map F).app Δ a = (CategoryTheory.Functor.mapComposableArrows F (Opposite.unop Δ).len).obj a

def CategoryTheory.nerveFunctor : CategoryTheory.Functor CategoryTheory.Cat SSet

The nerve of a category, as a functor Cat ⥤ SSet

Equations

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

theorem CategoryTheory.Nerve.δ₀_eq {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {n : ℕ} {x : (CategoryTheory.nerve C).obj (Opposite.op (SimplexCategory.mk (n + 1)))} : CategoryTheory.SimplicialObject.δ (CategoryTheory.nerve C) 0 x = CategoryTheory.ComposableArrows.δ₀ x