mathlib3 documentation

algebraic_topology.nerve

The nerve of a category #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

References #

source
@[simp]
theorem category_theory.nerve_obj (C : Type u) [category_theory.category C] (Δ : simplex_categoryᵒᵖ) :
(category_theory.nerve C).obj Δ = (↥(simplex_category.to_Cat.obj (opposite.unop Δ)) ⥤ C)
source
@[simp]
theorem category_theory.nerve_map (C : Type u) [category_theory.category C] (Δ₁ Δ₂ : simplex_categoryᵒᵖ) (f : Δ₁ ⟶ Δ₂) (x : ↥(simplex_category.to_Cat.obj (opposite.unop Δ₁)) ⥤ C) :
(category_theory.nerve C).map f x = simplex_category.to_Cat.map f.unop ⋙ x
source
def category_theory.nerve (C : Type u) [category_theory.category C] :
sSet

The nerve of a category

Equations
source
@[protected, instance]
def category_theory.obj.category {C : Type u_1} [category_theory.category C] {Δ : simplex_categoryᵒᵖ} :
category_theory.category ((category_theory.nerve C).obj Δ)
Equations
source
@[simp]
theorem category_theory.nerve_functor_obj (C : category_theory.Cat) :
category_theory.nerve_functor.obj C = category_theory.nerve ↥C
source
def category_theory.nerve_functor  :
category_theory.Cat ⥤ sSet

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

Equations
source
@[simp]
theorem category_theory.nerve_functor_map_app (C C' : category_theory.Cat) (F : C ⟶ C') (Δ : simplex_categoryᵒᵖ) (x : (category_theory.nerve ↥C).obj Δ) :
(category_theory.nerve_functor.map F).app Δ x = x ⋙ F