feat(algebraic_topology): the nerve of a category (#14304)

joelriou · joelriou · commit 841aef25c9d7 · 2022-05-27T05:12:29.000Z
diff --git a/src/algebraic_topology/nerve.lean b/src/algebraic_topology/nerve.lean
@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2022 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+
+import algebraic_topology.simplicial_set
+
+/-!
+
+# 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).
+
+## References
+* [Paul G. Goerss, John F. Jardine, *Simplical Homotopy Theory*][goerss-jardine-2009]
+
+-/
+
+open category_theory.category
+
+universes v u
+
+namespace category_theory
+
+/-- The nerve of a category -/
+@[simps]
+def nerve (C : Type u) [category.{v} C] : sSet.{max u v} :=
+{ obj := λ Δ, (simplex_category.to_Cat.obj Δ.unop) ⥤ C,
+  map := λ Δ₁ Δ₂ f x, simplex_category.to_Cat.map f.unop ⋙ x,
+  map_id' := λ Δ, begin
+    rw [unop_id, functor.map_id],
+    ext x,
+    apply functor.id_comp,
+  end, }
+
+instance {C : Type*} [category C] {Δ : simplex_categoryᵒᵖ} : category ((nerve C).obj Δ) :=
+(infer_instance : category ((simplex_category.to_Cat.obj Δ.unop) ⥤ C))
+
+/-- The nerve of a category, as a functor `Cat ⥤ sSet` -/
+@[simps]
+def nerve_functor : Cat ⥤ sSet :=
+{ obj := λ C, nerve C,
+  map := λ C C' F,
+  { app := λ Δ x, x ⋙ F, },
+  map_id' := λ C, begin
+    ext Δ x,
+    apply functor.comp_id,
+  end, }
+
+end category_theory
diff --git a/src/algebraic_topology/simplex_category.lean b/src/algebraic_topology/simplex_category.lean
@@ -728,4 +728,12 @@ end
 
 end epi_mono
 
+/-- This functor `simplex_category ⥤ Cat` sends `[n]` (for `n : ℕ`)
+to the category attached to the ordered set `{0, 1, ..., n}` -/
+@[simps obj map]
+def to_Cat : simplex_category ⥤ Cat.{0} :=
+simplex_category.skeletal_functor ⋙ forget₂ NonemptyFinLinOrd LinearOrder ⋙
+  forget₂ LinearOrder Lattice ⋙ forget₂ Lattice PartialOrder ⋙
+  forget₂ PartialOrder Preorder ⋙ Preorder_to_Cat
+
 end simplex_category
