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 [GJ09], 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

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

The nerve of a category

Equations

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

@[simp]

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

@[simp]

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

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

Equations

• CategoryTheory.instCategoryObjOppositeSimplexCategoryNerve = inferInstance

def CategoryTheory.nerveMap {C D : Type u} [Category.{v, u} C] [Category.{v, u} D] (F : Functor C D) : nerve C ⟶ nerve D

Given a functor C ⥤ D, we obtain a morphism nerve C ⟶ nerve D of simplicial sets.

Equations

• CategoryTheory.nerveMap F = { app := fun (x : SimplexCategoryᵒᵖ) => (F.mapComposableArrows (Opposite.unop x).len).obj, naturality := ⋯ }

@[simp]

theorem CategoryTheory.nerveMap_app {C D : Type u} [Category.{v, u} C] [Category.{v, u} D] (F : Functor C D) (x✝ : SimplexCategoryᵒᵖ) (a✝ : ComposableArrows C (Opposite.unop x✝).len) : (nerveMap F).app x✝ a✝ = (F.mapComposableArrows (Opposite.unop x✝).len).obj a✝

def CategoryTheory.nerveFunctor : Functor 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.

@[simp]

theorem CategoryTheory.nerveFunctor_map {X✝ Y✝ : Cat} (F : X✝ ⟶ Y✝) : nerveFunctor.map F = nerveMap F

@[simp]

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

def CategoryTheory.nerveEquiv (C : Type u) [Category.{v, u} C] : (nerve C).obj (Opposite.op (SimplexCategory.mk 0)) ≃ C

The 0-simplices of the nerve of a category are equivalent to the objects of the category.

Equations

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

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