Documentation

Mathlib.AlgebraicTopology.Nerve

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 #

@[simp]

The nerve of a category

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Equations
    • CategoryTheory.instCategoryObjOppositeSimplexCategoryNerve = inferInstance

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

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