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

Equations

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

theorem CategoryTheory.nerve_map (C : Type u) [Category.{v, u} C] {X✝ Y✝ : SimplexCategoryᵒᵖ} (f : X✝ ⟶ Y✝) : (nerve C).map f = TypeCat.ofHom fun (x : ComposableArrows C (Opposite.unop X✝).len) => x.whiskerLeft (SimplexCategory.toCat.map f.unop).toFunctor

@[simp]

theorem CategoryTheory.nerve_obj (C : Type u) [Category.{v, u} C] (Δ : SimplexCategoryᵒᵖ) : (nerve C).obj Δ = ComposableArrows C (Opposite.unop Δ).len

@[instance_reducible]

instance CategoryTheory.instCategoryObjOppositeSimplexCategoryNerve {C : Type u_1} [Category.{v_1, u_1} C] {Δ : SimplexCategoryᵒᵖ} : Category.{v_1, max u_1 v_1} ((nerve C).obj Δ)

Equations

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

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

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

theorem CategoryTheory.nerveMap_app {C D : Type u} [Category.{v, u} C] [Category.{v, u} D] (F : Functor C D) (x✝ : SimplexCategoryᵒᵖ) : (nerveMap F).app x✝ = TypeCat.ofHom fun (X : (nerve C).obj x✝) => (F.mapComposableArrows (Opposite.unop x✝).len).obj X

theorem CategoryTheory.nerveMap_app_mk₀ {C D : Type u} [Category.{v, u} C] [Category.{v, u} D] (F : Functor C D) (x : C) : (ConcreteCategory.hom ((nerveMap F).app (Opposite.op { len := 0 }))) (ComposableArrows.mk₀ x) = ComposableArrows.mk₀ (F.obj x)

theorem CategoryTheory.nerveMap_app_mk₁ {C D : Type u} [Category.{v, u} C] [Category.{v, u} D] (F : Functor C D) {x y : C} (f : x ⟶ y) : (ConcreteCategory.hom ((nerveMap F).app (Opposite.op { len := 1 }))) (ComposableArrows.mk₁ f) = ComposableArrows.mk₁ (F.map f)

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

@[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 α) { len := 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)) : ((ConcreteCategory.hom (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)) : ((ConcreteCategory.hom (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)} : (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 0)) x = x.δ₀

theorem CategoryTheory.nerve.σ₀_mk₀_eq {C : Type u} [Category.{v, u} C] (x : C) : (ConcreteCategory.hom (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₂) : (ConcreteCategory.hom (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₂) : (ConcreteCategory.hom (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₂) : (ConcreteCategory.hom (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) : (ConcreteCategory.hom (SimplicialObject.δ (nerve C) 2)) x = ComposableArrows.mk₁ (x.map' 0 1 δ₂_two._proof_1 δ₂_two._proof_3)

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

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.homEquiv_symm_apply {C : Type u} [Category.{v, u} C] {x y : ComposableArrows C 0} (f : nerveEquiv x ⟶ nerveEquiv y) : homEquiv.symm f = SSet.Edge.mk (ComposableArrows.mk₁ f) ⋯ ⋯

theorem CategoryTheory.nerve.homEquiv_apply {C : Type u} [Category.{v, u} C] {x y : ComposableArrows C 0} (e : SSet.Edge x y) : homEquiv e = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (ComposableArrows.hom e.edge) (eqToHom ⋯))

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

@[simp]

theorem CategoryTheory.nerve.edgeMk_id {C : Type u} [Category.{v, u} C] (x : C) : edgeMk (CategoryStruct.id x) = SSet.Edge.id (nerveEquiv.symm x)

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) : (ConcreteCategory.hom (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

def PartOrd.nerveFunctor : CategoryTheory.Functor PartOrd SSet

The functor PartOrd ⥤ SSet which sends a partially ordered type to its nerve.

Equations

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

@[simp]

theorem PartOrd.nerveFunctor_obj (X : PartOrd) : nerveFunctor.obj X = CategoryTheory.nerve ↑X

@[simp]

theorem PartOrd.nerveFunctor_map {X✝ Y✝ : PartOrd} (f : X✝ ⟶ Y✝) : nerveFunctor.map f = CategoryTheory.nerveMap ⋯.functor