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

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 := ⋯ }

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] : ComposableArrows C 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.

def CategoryTheory.nerve.representableBy {n : ℕ} (α : Type u) [Preorder α] (e : α ≃o Fin (n + 1)) : Functor.RepresentableBy (nerve α) (SimplexCategory.mk n)

Nerves of finite non-empty ordinals are representable functors.

Equations

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

theorem CategoryTheory.nerve.δ_obj {C : Type u} [Category.{v, u} C] {n : ℕ} (i : Fin (n + 2)) (x : ComposableArrows C (n + 1)) (j : Fin (n + 1)) : (SimplicialObject.δ (nerve C) i x).obj j = x.obj (i.succAbove j)

theorem CategoryTheory.nerve.σ_obj {C : Type u} [Category.{v, u} C] {n : ℕ} (i : Fin (n + 1)) (x : ComposableArrows C n) (j : Fin (n + 2)) : (SimplicialObject.σ (nerve C) i x).obj j = x.obj (i.predAbove j)

theorem CategoryTheory.nerve.δ₀_eq {C : Type u} [Category.{v, u} C] {n : ℕ} {x : ComposableArrows C (n + 1)} : SimplicialObject.δ (nerve C) 0 x = x.δ₀

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

theorem CategoryTheory.nerve.δ₂_mk₂_eq {C : Type u} [Category.{v, u} 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} [Category.{v, u} 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} [Category.{v, u} 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)

theorem CategoryTheory.nerve.ext_of_isThin {C : Type u} [Category.{v, u} C] [Quiver.IsThin C] {n : SimplexCategoryᵒᵖ} {x y : (nerve C).obj n} (h : x.obj = y.obj) : x = y

theorem CategoryTheory.nerve.ext_of_isThin_iff {C : Type u} [Category.{v, u} C] [Quiver.IsThin C] {n : SimplexCategoryᵒᵖ} {x y : (nerve C).obj n} : x = y ↔ x.obj = y.obj

@[simp]

theorem CategoryTheory.nerve.left_edge {C : Type u} [Category.{v, u} C] {x y : ComposableArrows C 0} (e : SSet.Edge x y) : ComposableArrows.left e.edge = nerveEquiv x

@[simp]

theorem CategoryTheory.nerve.right_edge {C : Type u} [Category.{v, u} C] {x y : ComposableArrows C 0} (e : SSet.Edge x y) : ComposableArrows.right e.edge = nerveEquiv y

theorem CategoryTheory.nerve.δ₂_two {C : Type u} [Category.{v, u} C] (x : ComposableArrows C 2) : SimplicialObject.δ (nerve C) 2 x = ComposableArrows.mk₁ (x.map' 0 1 ⋯ ⋯)

theorem CategoryTheory.nerve.δ₂_zero {C : Type u} [Category.{v, u} C] (x : ComposableArrows C 2) : SimplicialObject.δ (nerve C) 0 x = ComposableArrows.mk₁ (x.map' 1 2 ⋯ ⋯)

def CategoryTheory.nerve.homEquiv {C : Type u} [Category.{v, u} C] {x y : ComposableArrows C 0} : SSet.Edge x y ≃ (nerveEquiv x ⟶ nerveEquiv y)

Bijection between edges in the nerve of category and morphisms in the category.

Equations

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

theorem CategoryTheory.nerve.mk₁_homEquiv_apply {C : Type u} [Category.{v, u} C] {x y : ComposableArrows C 0} (e : SSet.Edge x y) : ComposableArrows.mk₁ (homEquiv e) = ComposableArrows.mk₁ (ComposableArrows.hom e.edge)

def CategoryTheory.nerve.edgeMk {C : Type u} [Category.{v, u} C] {x y : C} (f : x ⟶ y) : SSet.Edge (nerveEquiv.symm x) (nerveEquiv.symm y)

Constructor for edges in the nerve of a category. (See also homEquiv.)

Equations

• CategoryTheory.nerve.edgeMk f = SSet.Edge.mk (CategoryTheory.ComposableArrows.mk₁ f) ⋯ ⋯

@[simp]

theorem CategoryTheory.nerve.edgeMk_edge {C : Type u} [Category.{v, u} C] {x y : C} (f : x ⟶ y) : (edgeMk f).edge = ComposableArrows.mk₁ f

theorem CategoryTheory.nerve.edgeMk_surjective {C : Type u} [Category.{v, u} C] {x y : C} : Function.Surjective edgeMk

@[simp]

theorem CategoryTheory.nerve.homEquiv_edgeMk {C : Type u} [Category.{v, u} C] {x y : C} (f : x ⟶ y) : homEquiv (edgeMk f) = f

theorem CategoryTheory.nerve.homEquiv_id {C : Type u} [Category.{v, u} C] (x : ComposableArrows C 0) : homEquiv (SSet.Edge.id x) = CategoryStruct.id (nerveEquiv x)

theorem CategoryTheory.nerve.nonempty_compStruct_iff {C : Type u} [Category.{v, u} C] {x₀ x₁ x₂ : C} (f₀₁ : x₀ ⟶ x₁) (f₁₂ : x₁ ⟶ x₂) (f₀₂ : x₀ ⟶ x₂) : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)) ↔ CategoryStruct.comp f₀₁ f₁₂ = f₀₂

theorem CategoryTheory.nerve.homEquiv_comp {C : Type u} [Category.{v, u} C] {x₀ x₁ x₂ : ComposableArrows C 0} {e₀₁ : SSet.Edge x₀ x₁} {e₁₂ : SSet.Edge x₁ x₂} {e₀₂ : SSet.Edge x₀ x₂} (h : e₀₁.CompStruct e₁₂ e₀₂) : CategoryStruct.comp (homEquiv e₀₁) (homEquiv e₁₂) = homEquiv e₀₂

theorem CategoryTheory.nerve.σ_zero_nerveEquiv_symm {C : Type u} [Category.{v, u} C] (x : C) : SimplicialObject.σ (nerve C) 0 (nerveEquiv.symm x) = ComposableArrows.mk₁ (CategoryStruct.id x)

@[simp]

theorem CategoryTheory.nerve.homEquiv_edgeMk_map_nerveMap {C : Type u} [Category.{v, u} C] {D : Type u} [Category.{v, u} D] {x y : C} (f : x ⟶ y) (F : Functor C D) : homEquiv ((edgeMk f).map (nerveMap F)) = F.map f