[Merged by Bors] - feat(AlgebraicTopology): define the simplicial nerve of a simplicial category

Mathlib.lean

@@ -1053,6 +1053,7 @@ import Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
 import Mathlib.AlgebraicTopology.SimplexCategory
 import Mathlib.AlgebraicTopology.SimplicialCategory.Basic
 import Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject
+import Mathlib.AlgebraicTopology.SimplicialNerve
 import Mathlib.AlgebraicTopology.SimplicialObject.Basic
 import Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal
 import Mathlib.AlgebraicTopology.SimplicialSet.Basic

Mathlib/AlgebraicTopology/SimplicialNerve.lean

@@ -0,0 +1,232 @@
+/-
+Copyright (c) 2024 Dagur Asgeirsson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Dagur Asgeirsson
+-/
+import Mathlib.AlgebraicTopology.SimplicialCategory.Basic
+import Mathlib.AlgebraicTopology.SimplicialSet.Nerve
+/-!
+
+# The simplicial nerve of a simplicial category
+
+This file defines the simplicial nerve (sometimes called homotopy coherent nerve) of a simplicial
+category.
+
+We define the *simplicial thickening* of a linear order `J` as the simplicial category whose hom
+objects `i ⟶ j` are given by the nerve of the poset of "paths" from `i` to `j` in `J`. This is the
+poset of subsets of the interval `[i, j]` in `J`, containing the endpoints.
+
+The simplicial nerve of a simplicial category `C` is then defined as the simplicial set whose
+`n`-simplices are given by the set of simplicial functors from the simplicial thickening of
+the linear order `Fin (n + 1)` to `C`, in other words
+`SimplicialNerve C _[n] := EnrichedFunctor SSet (SimplicialThickening (Fin (n + 1))) C`.
+
+## Projects
+
+* Prove that the 0-simplicies of `SimplicialNerve C` may be identified with the objects of `C`
+* Prove that the 1-simplicies of `SimplicialNerve C` may be identified with the morphisms of `C`
+* Prove that the simplicial nerve of a simplicial category `C`, such that `sHom X Y` is a Kan
+  complex for every pair of objects `X Y : C`, is a quasicategory.
+* Define the quasicategory of anima as the simplicial nerve of the simplicial category of
+  Kan complexes.
+* Define the functor from topological spaces to anima.
+
+## References
+* [Jacob Lurie, *Higher Topos Theory*, Section 1.1.5][LurieHTT]
+-/
+
+universe v u
+
+namespace CategoryTheory
+
+-- This is to improve automation throughout this file, because `simp` doesn't apply
+-- `NatTrans.comp_app` to morphisms of simplicial sets.
+attribute [local simp] SSet.comp_app
+
+open SimplicialCategory EnrichedCategory EnrichedOrdinaryCategory MonoidalCategory
+
+open scoped Simplicial
+
+section SimplicialNerve
+
+/-- A type synonym for a linear order `J`, will be equipped with a simplicial category structure. -/
+@[nolint unusedArguments]
+def SimplicialThickening (J : Type*) [LinearOrder J] : Type _ := J
+
+instance (J : Type*) [LinearOrder J] : LinearOrder (SimplicialThickening J) :=
+  inferInstanceAs (LinearOrder J)
+
+namespace SimplicialThickening
+
+/--
+A path from `i` to `j` in a linear order `J` is a subset of the interval `[i, j]` in `J` containing
+the endpoints.
+-/
+@[ext]
+structure Path {J : Type*} [LinearOrder J] (i j : J) where
+  /-- The underlying subset -/
+  I : Set J
+  left : i ∈ I := by simp
+  right : j ∈ I := by simp
+  left_le (k : J) (_ : k ∈ I) : i ≤ k := by simp
+  le_right (k : J) (_ : k ∈ I) : k ≤ j := by simp
+
+lemma Path.le {J : Type*} [LinearOrder J] {i j : J} (f : Path i j) : i ≤ j :=
+  f.left_le _ f.right
+
+instance {J : Type*} [LinearOrder J] (i j : J) : Category (Path i j) :=
+  InducedCategory.category (fun f : Path i j ↦ f.I)
+
+@[simps]
+instance (J : Type*) [LinearOrder J] : CategoryStruct (SimplicialThickening J) where
+  Hom i j := Path i j
+  id i := { I := {i} }
+  comp {i j k} f g := {
+    I := f.I ∪ g.I
+    left := Or.inl f.left
+    right := Or.inr g.right
+    left_le l := by
+      rintro (h | h)
+      exacts [(f.left_le l h), (Path.le f).trans (g.left_le l h)]
+    le_right l := by
+      rintro (h | h)
+      exacts [(f.le_right _ h).trans (Path.le g), (g.le_right l h)] }
+
+instance {J : Type*} [LinearOrder J] (i j : SimplicialThickening J) : Category (i ⟶ j) :=
+  inferInstanceAs (Category (Path _ _))
+
+@[ext]
+lemma hom_ext {J : Type*} [LinearOrder J]
+    (i j : SimplicialThickening J) (x y : i ⟶ j) (h : ∀ t, t ∈ x.I ↔ t ∈ y.I) : x = y := by
+  apply Path.ext
+  ext
+  apply h
+
+instance (J : Type*) [LinearOrder J] : Category (SimplicialThickening J) where
+  id_comp f := by ext; simpa using fun h ↦ h ▸ f.left
+  comp_id f := by ext; simpa using fun h ↦ h ▸ f.right
+
+/--
+Composition of morphisms in `SimplicialThickening J`, as a functor `(i ⟶ j) × (j ⟶ k) ⥤ (i ⟶ k)`
+-/
+@[simps]
+def compFunctor {J : Type*} [LinearOrder J]
+    (i j k : SimplicialThickening J) : (i ⟶ j) × (j ⟶ k) ⥤ (i ⟶ k) where
+  obj x := x.1 ≫ x.2
+  map f := ⟨⟨Set.union_subset_union f.1.1.1 f.2.1.1⟩⟩
+
+namespace SimplicialCategory
+
+variable {J : Type*} [LinearOrder J]
+
+/-- The hom simplicial set of the simplicial category structure on `SimplicialThickening J` -/
+abbrev Hom (i j : SimplicialThickening J) : SSet := (nerve (i ⟶ j))
+
+/-- The identity of the simplicial category structure on `SimplicialThickening J` -/
+abbrev id (i : SimplicialThickening J) : 𝟙_ SSet ⟶ Hom i i :=
+  ⟨fun _ _ ↦ (Functor.const _).obj (𝟙 _), fun _ _ _ ↦ by simp; rfl⟩
+
+/-- The composition of the simplicial category structure on `SimplicialThickening J` -/
+abbrev comp (i j k : SimplicialThickening J) : Hom i j ⊗ Hom j k ⟶ Hom i k :=
+  ⟨fun _ x ↦ x.1.prod' x.2 ⋙ compFunctor i j k, fun _ _ _ ↦ by simp; rfl⟩
+
+@[simp]
+lemma id_comp (i j : SimplicialThickening J) :
+    (λ_ (Hom i j)).inv ≫ id i ▷ Hom i j ≫ comp i i j = 𝟙 (Hom i j) := by
+  rw [Iso.inv_comp_eq]
+  ext
+  exact Functor.ext (fun _ ↦ by simp)
+
+@[simp]
+lemma comp_id (i j : SimplicialThickening J) :
+    (ρ_ (Hom i j)).inv ≫ Hom i j ◁ id j ≫ comp i j j = 𝟙 (Hom i j) := by
+  rw [Iso.inv_comp_eq]
+  ext
+  exact Functor.ext (fun _ ↦ by simp)
+
+@[simp]
+lemma assoc (i j k l : SimplicialThickening J) :
+    (α_ (Hom i j) (Hom j k) (Hom k l)).inv ≫ comp i j k ▷ Hom k l ≫ comp i k l =
+      Hom i j ◁ comp j k l ≫ comp i j l := by
+  ext
+  exact Functor.ext (fun _ ↦ by simp)
+
+end SimplicialCategory
+
+open SimplicialThickening.SimplicialCategory
+
+noncomputable instance (J : Type*) [LinearOrder J] :
+    SimplicialCategory (SimplicialThickening J) where
+  Hom := Hom
+  id := id
+  comp := comp
+  homEquiv {i j} := (nerveEquiv _).symm.trans (SSet.unitHomEquiv _).symm
+
+/-- Auxiliary definition for `SimplicialThickening.functorMap` -/
+def orderHom {J K : Type*} [LinearOrder J] [LinearOrder K] (f : J →o K) :
+    SimplicialThickening J →o SimplicialThickening K := f
+
+/-- Auxiliary definition for `SimplicialThickening.functor` -/
+noncomputable abbrev functorMap {J K : Type u} [LinearOrder J] [LinearOrder K]
+    (f : J →o K) (i j : SimplicialThickening J) : (i ⟶ j) ⥤ ((orderHom f i) ⟶ (orderHom f j)) where
+  obj I := ⟨f '' I.I, Set.mem_image_of_mem f I.left, Set.mem_image_of_mem f I.right,
+    by rintro _ ⟨k, hk, rfl⟩; exact f.monotone (I.left_le k hk),
+    by rintro _ ⟨k, hk, rfl⟩; exact f.monotone (I.le_right k hk)⟩
+  map f := ⟨⟨Set.image_subset _ f.1.1⟩⟩
+
+/--
+The simplicial thickening defines a functor from the category of linear orders to the category of
+simplicial categories
+-/
+@[simps]
+noncomputable def functor {J K : Type u} [LinearOrder J] [LinearOrder K]
+    (f : J →o K) : EnrichedFunctor SSet (SimplicialThickening J) (SimplicialThickening K) where
+  obj := f
+  map i j := nerveMap ((functorMap f i j))
+  map_id i := by
+    ext
+    simp only [eId, EnrichedCategory.id]
+    exact Functor.ext (by aesop_cat)
+  map_comp i j k := by
+    ext
+    simp only [eComp, EnrichedCategory.comp]
+    exact Functor.ext (by aesop_cat)
+
+lemma functor_id (J : Type u) [LinearOrder J] :
+    (functor (OrderHom.id (α := J))) = EnrichedFunctor.id _ _ := by
+  refine EnrichedFunctor.ext _ (fun _ ↦ rfl) fun i j ↦ ?_
+  ext
+  exact Functor.ext (by aesop_cat)
+
+lemma functor_comp {J K L : Type u} [LinearOrder J] [LinearOrder K]
+    [LinearOrder L] (f : J →o K) (g : K →o L) :
+    functor (g.comp f) =
+      (functor f).comp _ (functor g) := by
+  refine EnrichedFunctor.ext _ (fun _ ↦ rfl) fun i j ↦ ?_
+  ext
+  exact Functor.ext (by aesop_cat)
+
+end SimplicialThickening
+
+/--
+The simplicial nerve of a simplicial category `C` is defined as the simplicial set whose
+`n`-simplices are given by the set of simplicial functors from the simplicial thickening of
+the linear order `Fin (n + 1)` to `C`
+-/
+noncomputable def SimplicialNerve (C : Type u) [Category.{v} C] [SimplicialCategory C] :
+    SSet.{max u v} where
+  obj n := EnrichedFunctor SSet (SimplicialThickening (ULift (Fin (n.unop.len + 1)))) C
+  map f := (SimplicialThickening.functor f.unop.toOrderHom.uliftMap).comp (E := C) SSet
+  map_id i := by
+    change EnrichedFunctor.comp SSet (SimplicialThickening.functor (OrderHom.id)) = _
+    rw [SimplicialThickening.functor_id]
+    rfl
+  map_comp f g := by
+    change EnrichedFunctor.comp SSet (SimplicialThickening.functor
+      (f.unop.toOrderHom.uliftMap.comp g.unop.toOrderHom.uliftMap)) = _
+    rw [SimplicialThickening.functor_comp]
+    rfl
+
+end SimplicialNerve
+
+end CategoryTheory

Mathlib/AlgebraicTopology/SimplicialSet/Basic.lean

@@ -61,6 +61,12 @@ instance hasColimits : HasColimits SSet := by
 lemma hom_ext {X Y : SSet} {f g : X ⟶ Y} (w : ∀ n, f.app n = g.app n) : f = g :=
   SimplicialObject.hom_ext _ _ w
 
+-- Even though `NatTrans.comp_app` is a `@[simp]` lemma, `simp` is unable to prove this.
+-- Why is this?
+-- Do we want `SSet.comp_app` as a global `@[simp]` lemma?
+lemma comp_app {X Y Z : SSet} (f : X ⟶ Y) (g : Y ⟶ Z) (n : SimplexCategoryᵒᵖ) :
+    (f ≫ g).app n = f.app n ≫ g.app n := NatTrans.comp_app _ _ _
+
 /-- The ulift functor `SSet.{u} ⥤ SSet.{max u v}` on simplicial sets. -/
 def uliftFunctor : SSet.{u} ⥤ SSet.{max u v} :=
   (SimplicialObject.whiskering _ _).obj CategoryTheory.uliftFunctor.{v, u}

Mathlib/AlgebraicTopology/SimplicialSet/Nerve.lean

@@ -35,11 +35,23 @@ def nerve (C : Type u) [Category.{v} C] : SSet.{max u v} where
 instance {C : Type*} [Category C] {Δ : SimplexCategoryᵒᵖ} : Category ((nerve C).obj Δ) :=
   (inferInstance : Category (ComposableArrows C (Δ.unop.len)))
 
+/-- Given a functor `C ⥤ D`, we obtain a morphism `nerve C ⟶ nerve D` of simplicial sets. -/
+@[simps]
+def nerveMap {C D : Type u} [Category.{v} C] [Category.{v} D] (F : C ⥤ D) : nerve C ⟶ nerve D :=
+  { app := fun _ => (F.mapComposableArrows _).obj }
+
 /-- The nerve of a category, as a functor `Cat ⥤ SSet` -/
 @[simps]
 def nerveFunctor : Cat.{v, u} ⥤ SSet where
   obj C := nerve C
-  map F := { app := fun _ => (F.mapComposableArrows _).obj }
+  map F := nerveMap F
+
+/-- The 0-simplices of the nerve of a category are equivalent to the objects of the category. -/
+def nerveEquiv (C : Type u) [Category.{v} C] : nerve C _[0] ≃ C where
+  toFun f := f.obj ⟨0, by omega⟩
+  invFun f := (Functor.const _).obj f
+  left_inv f := ComposableArrows.ext₀ rfl
+  right_inv f := rfl
 
 namespace Nerve
 

Mathlib/CategoryTheory/Enriched/Basic.lean

@@ -297,6 +297,16 @@ def EnrichedFunctor.comp {C : Type u₁} {D : Type u₂} {E : Type u₃} [Enrich
   obj X := G.obj (F.obj X)
   map _ _ := F.map _ _ ≫ G.map _ _
 
+lemma EnrichedFunctor.ext {C : Type u₁} {D : Type u₂} [EnrichedCategory V C]
+    [EnrichedCategory V D] {F G : EnrichedFunctor V C D} (h_obj : ∀ X, F.obj X = G.obj X)
+    (h_map : ∀ (X Y : C), F.map X Y ≫ eqToHom (by rw [h_obj, h_obj]) = G.map X Y) : F = G := by
+  match F, G with
+  | mk F_obj F_map _ _, mk G_obj G_map _ _ =>
+    obtain rfl : F_obj = G_obj := funext fun X ↦ h_obj X
+    congr
+    ext X Y
+    simpa using h_map X Y
+
 section
 
 variable {W : Type (v + 1)} [Category.{v} W] [MonoidalCategory W]

Mathlib/Order/Hom/Basic.lean

@@ -521,6 +521,12 @@ protected def withBotMap (f : α →o β) : WithBot α →o WithBot β :=
 protected def withTopMap (f : α →o β) : WithTop α →o WithTop β :=
   ⟨WithTop.map f, f.mono.withTop_map⟩
 
+/-- Lift an order homomorphism `f : α →o β` to an order homomorphism `ULift α →o ULift β` in a
+higher universe. -/
+@[simps!]
+def uliftMap (f : α →o β) : ULift α →o ULift β :=
+  ⟨fun i => ⟨f i.down⟩, fun _ _ h ↦ f.monotone h⟩
+
 end OrderHom
 
 /-- Embeddings of partial orders that preserve `<` also preserve `≤`. -/

docs/references.bib

@@ -2557,6 +2557,13 @@ @InProceedings{   lewis2019
   keywords      = {Hensel's lemma, Lean, formal proof, p-adic}
 }
 
+@Book{            LurieHTT,
+  title         = {Higher Topos Theory},
+  author        = {Jacob Lurie},
+  url           = {https://www.math.ias.edu/~lurie/papers/HTT.pdf},
+  year          = {2009}
+}
+
 @Book{            LurieSAG,
   title         = {Spectral Algebraic Geometry},
   author        = {Jacob Lurie},