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

References

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

@[simp]

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

@[simp]

theorem CategoryTheory.nerve_map (C : Type u) [CategoryTheory.Category.{v, u} C] : ∀ {X Y : SimplexCategoryᵒᵖ} (f : X ⟶ Y) (x : CategoryTheory.Functor (↑(SimplexCategory.toCat.obj X.unop)) C), (CategoryTheory.nerve C).map f x = CategoryTheory.Functor.comp (SimplexCategory.toCat.map f.unop) x

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

The nerve of a category

instance CategoryTheory.instCategoryObjOppositeSimplexCategoryToQuiverToCategoryStructOppositeSmallCategoryTypeToQuiverToCategoryStructTypesToPrefunctorNerve {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 Δ)

@[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ᵒᵖ) (x : ((fun C => CategoryTheory.nerve ↑C) X).obj Δ), (CategoryTheory.nerveFunctor.map F).app Δ x = CategoryTheory.Functor.comp x F

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

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