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

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

def CategoryTheory.nerveMap {C D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] (F : CategoryTheory.Functor C D) : CategoryTheory.nerve C ⟶ CategoryTheory.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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] (F : CategoryTheory.Functor C D) (x✝ : SimplexCategoryᵒᵖ) (a✝ : CategoryTheory.ComposableArrows C (Opposite.unop x✝).len) : (CategoryTheory.nerveMap F).app x✝ a✝ = (F.mapComposableArrows (Opposite.unop x✝).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.

@[simp]

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

@[simp]

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

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