nerve

Mathlib.AlgebraicTopology.SimplicialSet.Nerve

URI: https://scilib.ai/kg/mathlib#CategoryTheory.nerve

Lean4

/-- The nerve of a category -/
@[simps]
def nerve (C : Type u) [Category.{v} C] : SSet.{max u v}
    where
  obj Δ := ComposableArrows C (Δ.unop.len)
  map f
    x :=
    x.whiskerLeft
      (SimplexCategory.toCat.map f.unop)
        -- `aesop` can prove these but is slow, help it out:

  map_id _ := rfl
  map_comp _ _ := rfl

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru