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]

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

The nerve of a category

@[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 Δ)

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.

@[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

@[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.

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

theorem CategoryTheory.nerve.σ₀_mk₀_eq {C : Type u_1} [Category.{u_2, u_1} C] (x : C) : SimplicialObject.σ (nerve C) 0 (ComposableArrows.mk₀ x) = ComposableArrows.mk₁ (CategoryStruct.id x)

theorem CategoryTheory.nerve.δ₂_mk₂_eq {C : Type u_1} [Category.{u_2, u_1} C] {X₀ X₁ X₂ : C} (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂) : SimplicialObject.δ (nerve C) 2 (ComposableArrows.mk₂ f g) = ComposableArrows.mk₁ f

theorem CategoryTheory.nerve.δ₀_mk₂_eq {C : Type u_1} [Category.{u_2, u_1} C] {X₀ X₁ X₂ : C} (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂) : SimplicialObject.δ (nerve C) 0 (ComposableArrows.mk₂ f g) = ComposableArrows.mk₁ g

theorem CategoryTheory.nerve.δ₁_mk₂_eq {C : Type u_1} [Category.{u_2, u_1} C] {X₀ X₁ X₂ : C} (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂) : SimplicialObject.δ (nerve C) 1 (ComposableArrows.mk₂ f g) = ComposableArrows.mk₁ (CategoryStruct.comp f g)