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).
References #
@[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)
@[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
The nerve of a category
Equations
- category_theory.nerve C = {obj := λ (Δ : simplex_categoryᵒᵖ), ↥(simplex_category.to_Cat.obj (opposite.unop Δ)) ⥤ C, map := λ (Δ₁ Δ₂ : simplex_categoryᵒᵖ) (f : Δ₁ ⟶ Δ₂) (x : ↥(simplex_category.to_Cat.obj (opposite.unop Δ₁)) ⥤ C), simplex_category.to_Cat.map f.unop ⋙ x, map_id' := _, map_comp' := _}
@[protected, instance]
def
category_theory.obj.category
{C : Type u_1}
[category_theory.category C]
{Δ : simplex_categoryᵒᵖ} :
Equations
@[simp]
The nerve of a category, as a functor Cat ⥤ sSet
Equations
- category_theory.nerve_functor = {obj := λ (C : category_theory.Cat), category_theory.nerve ↥C, map := λ (C C' : category_theory.Cat) (F : C ⟶ C'), {app := λ (Δ : simplex_categoryᵒᵖ) (x : (category_theory.nerve ↥C).obj Δ), x ⋙ F, naturality' := _}, map_id' := category_theory.nerve_functor._proof_2, map_comp' := category_theory.nerve_functor._proof_3}
@[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