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).toPrefunctor.obj Δ = CategoryTheory.ComposableArrows C (SimplexCategory.len Δ.unop)

@[simp]

theorem CategoryTheory.nerve_map (C : Type u) [CategoryTheory.Category.{v, u} C] : ∀ {X Y : SimplexCategoryᵒᵖ} (f : X ⟶ Y) (x : CategoryTheory.ComposableArrows C (SimplexCategory.len X.unop)), (CategoryTheory.nerve C).toPrefunctor.map f x = CategoryTheory.ComposableArrows.whiskerLeft x (SimplexCategory.toCat.toPrefunctor.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.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).toPrefunctor.obj Δ)

Equations

• CategoryTheory.instCategoryObjOppositeSimplexCategoryToQuiverToCategoryStructOppositeSmallCategoryTypeToQuiverToCategoryStructTypesToPrefunctorNerve = inferInstance

@[simp]

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

@[simp]

theorem CategoryTheory.nerveFunctor_map_app : ∀ {X Y : CategoryTheory.Cat} (F : X ⟶ Y) (Δ : SimplexCategoryᵒᵖ) (a : CategoryTheory.ComposableArrows (↑X) (SimplexCategory.len Δ.unop)), (CategoryTheory.nerveFunctor.toPrefunctor.map F).app Δ a = (CategoryTheory.Functor.mapComposableArrows F (SimplexCategory.len Δ.unop)).toPrefunctor.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).toPrefunctor.obj (Opposite.op (SimplexCategory.mk (n + 1)))} : CategoryTheory.SimplicialObject.δ (CategoryTheory.nerve C) 0 x = CategoryTheory.ComposableArrows.δ₀ x