feat(AlgebraicTopology/SimplicialSet): paths and the strict segal condition (#18499)

A path in a simplicial set `X` of length `n` is a directed path comprised of `n` 1-simplices.

An `n`-simplex has a maximal path, the `spine` of the simplex, which is a path of length `n`. A simplicial set `X` satisfies the `StrictSegal` condition if for all `n`, the map `X.spine n : X _[n] → X.Path n` is a bijection.

Examples of `StrictSegal` simplicial sets are given by nerves of categories. Future work will show these are the only examples: that a `StrictSegal` simplicial set is isomorphic to the nerve of its homotopy category.

Co-Authored-By: [Mario Carneiro](https://github.com/digama0) and [Joël Riou](https://github.com/joelriou)

Author: emilyriehl

Mathlib.lean

@@ -1000,7 +1000,9 @@ import Mathlib.AlgebraicTopology.SimplicialSet.Basic
 import Mathlib.AlgebraicTopology.SimplicialSet.KanComplex
 import Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
 import Mathlib.AlgebraicTopology.SimplicialSet.Nerve
+import Mathlib.AlgebraicTopology.SimplicialSet.Path
 import Mathlib.AlgebraicTopology.SimplicialSet.Quasicategory
+import Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
 import Mathlib.AlgebraicTopology.SingularSet
 import Mathlib.AlgebraicTopology.SplitSimplicialObject
 import Mathlib.AlgebraicTopology.TopologicalSimplex

Mathlib/AlgebraicTopology/SimplexCategory.lean

@@ -3,6 +3,7 @@ Copyright (c) 2020 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Kim Morrison, Adam Topaz
 -/
+import Mathlib.Tactic.FinCases
 import Mathlib.Tactic.Linarith
 import Mathlib.CategoryTheory.Skeletal
 import Mathlib.Data.Fintype.Sort
@@ -168,6 +169,10 @@ theorem const_fac_thru_zero (n m : SimplexCategory) (i : Fin (m.len + 1)) :
     const n m i = const n [0] 0 ≫ SimplexCategory.const [0] m i := by
   rw [const_comp]; rfl
 
+theorem Hom.ext_zero_left {n : SimplexCategory} (f g : ([0] : SimplexCategory) ⟶ n)
+    (h0 : f.toOrderHom 0 = g.toOrderHom 0 := by rfl) : f = g := by
+  ext i; match i with | 0 => exact h0 ▸ rfl
+
 theorem eq_const_of_zero {n : SimplexCategory} (f : ([0] : SimplexCategory) ⟶ n) :
     f = const _ n (f.toOrderHom 0) := by
   ext x; match x with | 0 => rfl
@@ -180,6 +185,14 @@ theorem eq_const_to_zero {n : SimplexCategory} (f : n ⟶ [0]) :
   ext : 3
   apply @Subsingleton.elim (Fin 1)
 
+theorem Hom.ext_one_left {n : SimplexCategory} (f g : ([1] : SimplexCategory) ⟶ n)
+    (h0 : f.toOrderHom 0 = g.toOrderHom 0 := by rfl)
+    (h1 : f.toOrderHom 1 = g.toOrderHom 1 := by rfl) : f = g := by
+  ext i
+  match i with
+  | 0 => exact h0 ▸ rfl
+  | 1 => exact h1 ▸ rfl
+
 theorem eq_of_one_to_one (f : ([1] : SimplexCategory) ⟶ [1]) :
     (∃ a, f = const [1] _ a) ∨ f = 𝟙 _ := by
   match e0 : f.toOrderHom 0, e1 : f.toOrderHom 1 with
@@ -218,6 +231,14 @@ def mkOfLe {n} (i j : Fin (n+1)) (h : i ≤ j) : ([1] : SimplexCategory) ⟶ [n]
       | 0, 1, _ => h
   }
 
+/-- The morphism `[1] ⟶ [n]` that picks out the "diagonal composite" edge-/
+def diag (n : ℕ) : ([1] : SimplexCategory) ⟶ [n] :=
+  mkOfLe 0 n (Fin.zero_le _)
+
+/-- The morphism `[1] ⟶ [n]` that picks out the edge spanning the interval from `j` to `j + l`.-/
+def intervalEdge {n} (j l : ℕ) (hjl : j + l ≤ n) : ([1] : SimplexCategory) ⟶ [n] :=
+  mkOfLe ⟨j, (by omega)⟩ ⟨j + l, (by omega)⟩ (Nat.le_add_right j l)
+
 /-- The morphism `[1] ⟶ [n]` that picks out the arrow `i ⟶ i+1` in `Fin (n+1)`.-/
 def mkOfSucc {n} (i : Fin n) : ([1] : SimplexCategory) ⟶ [n] :=
   SimplexCategory.mkHom {
@@ -227,6 +248,15 @@ def mkOfSucc {n} (i : Fin n) : ([1] : SimplexCategory) ⟶ [n] :=
       | 0, 1, _ => Fin.castSucc_le_succ i
   }
 
+@[simp]
+lemma mkOfSucc_homToOrderHom_zero {n} (i : Fin n) :
+    DFunLike.coe (F := Fin 2 →o Fin (n+1)) (Hom.toOrderHom (mkOfSucc i)) 0 = i.castSucc := rfl
+
+@[simp]
+lemma mkOfSucc_homToOrderHom_one {n} (i : Fin n) :
+    DFunLike.coe (F := Fin 2 →o Fin (n+1)) (Hom.toOrderHom (mkOfSucc i)) 1 = i.succ := rfl
+
+
 /-- The morphism `[2] ⟶ [n]` that picks out a specified composite of morphisms in `Fin (n+1)`.-/
 def mkOfLeComp {n} (i j k : Fin (n + 1)) (h₁ : i ≤ j) (h₂ : j ≤ k) :
     ([2] : SimplexCategory) ⟶ [n] :=
@@ -239,6 +269,60 @@ def mkOfLeComp {n} (i j k : Fin (n + 1)) (h₁ : i ≤ j) (h₂ : j ≤ k) :
       | 0, 2, _ => Fin.le_trans h₁ h₂
   }
 
+/-- The "inert" morphism associated to a subinterval `j ≤ i ≤ j + l` of `Fin (n + 1)`.-/
+def subinterval {n} (j l : ℕ) (hjl : j + l ≤ n) :
+    ([l] : SimplexCategory) ⟶ [n] :=
+  SimplexCategory.mkHom {
+    toFun := fun i => ⟨i.1 + j, (by omega)⟩
+    monotone' := fun i i' hii' => by simpa only [Fin.mk_le_mk, add_le_add_iff_right] using hii'
+  }
+
+lemma const_subinterval_eq {n} (j l : ℕ) (hjl : j + l ≤ n) (i : Fin (l + 1)) :
+    [0].const [l] i ≫ subinterval j l hjl =
+    [0].const [n] ⟨j + i.1, lt_add_of_lt_add_right (Nat.add_lt_add_left i.2 j) hjl⟩  := by
+  rw [const_comp]
+  congr
+  ext
+  dsimp [subinterval]
+  rw [add_comm]
+
+@[simp]
+lemma mkOfSucc_subinterval_eq {n} (j l : ℕ) (hjl : j + l ≤ n) (i : Fin l) :
+    mkOfSucc i ≫ subinterval j l hjl =
+    mkOfSucc ⟨j + i.1, Nat.lt_of_lt_of_le (Nat.add_lt_add_left i.2 j) hjl⟩ := by
+  unfold subinterval mkOfSucc
+  ext i
+  match i with
+  | 0 =>
+    simp only [len_mk, Nat.reduceAdd, mkHom, comp_toOrderHom, Hom.toOrderHom_mk,
+      OrderHom.mk_comp_mk, Fin.isValue, OrderHom.coe_mk, Function.comp_apply, Fin.castSucc_mk,
+      Fin.succ_mk]
+    rw [add_comm]
+    rfl
+  | 1 =>
+    simp only [len_mk, Nat.reduceAdd, mkHom, comp_toOrderHom, Hom.toOrderHom_mk,
+      OrderHom.mk_comp_mk, Fin.isValue, OrderHom.coe_mk, Function.comp_apply, Fin.castSucc_mk,
+      Fin.succ_mk]
+    rw [← Nat.add_comm j _]
+    rfl
+
+@[simp]
+lemma diag_subinterval_eq {n} (j l : ℕ) (hjl : j + l ≤ n) :
+    diag l ≫ subinterval j l hjl = intervalEdge j l hjl := by
+  unfold subinterval intervalEdge diag mkOfLe
+  ext i
+  match i with
+  | 0 =>
+    simp only [len_mk, Nat.reduceAdd, mkHom, Fin.natCast_eq_last, comp_toOrderHom,
+      Hom.toOrderHom_mk, OrderHom.mk_comp_mk, Fin.isValue, OrderHom.coe_mk, Function.comp_apply]
+    rw [Nat.add_comm]
+    rfl
+  | 1 =>
+    simp only [len_mk, Nat.reduceAdd, mkHom, Fin.natCast_eq_last, comp_toOrderHom,
+      Hom.toOrderHom_mk, OrderHom.mk_comp_mk, Fin.isValue, OrderHom.coe_mk, Function.comp_apply]
+    rw [Nat.add_comm]
+    rfl
+
 instance (Δ : SimplexCategory) : Subsingleton (Δ ⟶ [0]) where
   allEq f g := by ext : 3; apply Subsingleton.elim (α := Fin 1)
 
@@ -466,6 +550,19 @@ lemma factor_δ_spec {m n : ℕ} (f : ([m] : SimplexCategory) ⟶ [n+1]) (j : Fi
       · rwa [succ_le_castSucc_iff, lt_pred_iff]
       rw [succ_pred]
 
+@[simp]
+lemma δ_zero_mkOfSucc {n : ℕ} (i : Fin n) :
+    δ 0 ≫ mkOfSucc i = SimplexCategory.const _ [n] i.succ := by
+  ext x
+  fin_cases x
+  rfl
+
+@[simp]
+lemma δ_one_mkOfSucc {n : ℕ} (i : Fin n) :
+    δ 1 ≫ mkOfSucc i = SimplexCategory.const _ _ i.castSucc := by
+  ext x
+  fin_cases x
+  aesop
 
 theorem eq_of_one_to_two (f : ([1] : SimplexCategory) ⟶ [2]) :
     f = (δ (n := 1) 0) ∨ f = (δ (n := 1) 1) ∨ f = (δ (n := 1) 2) ∨

Mathlib/AlgebraicTopology/SimplicialObject.lean

@@ -88,6 +88,9 @@ def δ {n} (i : Fin (n + 2)) : X _[n + 1] ⟶ X _[n] :=
 def σ {n} (i : Fin (n + 1)) : X _[n] ⟶ X _[n + 1] :=
   X.map (SimplexCategory.σ i).op
 
+/-- The diagonal of a simplex is the long edge of the simplex.-/
+def diagonal {n : ℕ} : X _[n] ⟶ X _[1] := X.map ((SimplexCategory.diag n).op)
+
 /-- Isomorphisms from identities in ℕ. -/
 def eqToIso {n m : ℕ} (h : n = m) : X _[n] ≅ X _[m] :=
   X.mapIso (CategoryTheory.eqToIso (by congr))

Mathlib/AlgebraicTopology/SimplicialSet/Path.lean

@@ -0,0 +1,76 @@
+/-
+Copyright (c) 2024 Emily Riehl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro, Emily Riehl, Joël Riou
+-/
+import Mathlib.AlgebraicTopology.SimplicialSet.Basic
+
+/-!
+# Paths in simplicial sets
+
+A path in a simplicial set `X` of length `n` is a directed path comprised of `n + 1` 0-simplices
+and `n` 1-simplices, together with identifications between 0-simplices and the sources and targets
+of the 1-simplices.
+
+An `n`-simplex has a maximal path, the `spine` of the simplex, which is a path of length `n`.
+-/
+
+universe v u
+
+namespace SSet
+
+open CategoryTheory
+
+open Simplicial SimplexCategory
+
+variable (X : SSet.{u})
+
+/-- A path in a simplicial set `X` of length `n` is a directed path of `n` edges.-/
+@[ext]
+structure Path (n : ℕ) where
+  /-- A path includes the data of `n+1` 0-simplices in `X`.-/
+  vertex (i : Fin (n + 1)) : X _[0]
+  /-- A path includes the data of `n` 1-simplices in `X`.-/
+  arrow (i : Fin n) : X _[1]
+  /-- The sources of the 1-simplices in a path are identified with appropriate 0-simplices.-/
+  arrow_src (i : Fin n) : X.δ 1 (arrow i) = vertex i.castSucc
+  /-- The targets of the 1-simplices in a path are identified with appropriate 0-simplices.-/
+  arrow_tgt (i : Fin n) : X.δ 0 (arrow i) = vertex i.succ
+
+
+variable {X} in
+/-- For `j + l ≤ n`, a path of length `n` restricts to a path of length `l`, namely the subpath
+spanned by the vertices `j ≤ i ≤ j + l` and edges `j ≤ i < j + l`. -/
+def Path.interval {n : ℕ} (f : Path X n) (j l : ℕ) (hjl : j + l ≤ n) :
+    Path X l where
+  vertex i := f.vertex ⟨j + i, by omega⟩
+  arrow i := f.arrow ⟨j + i, by omega⟩
+  arrow_src i := f.arrow_src ⟨j + i, by omega⟩
+  arrow_tgt i := f.arrow_tgt ⟨j + i, by omega⟩
+
+/-- The spine of an `n`-simplex in `X` is the path of edges of length `n` formed by
+traversing through its vertices in order.-/
+@[simps]
+def spine (n : ℕ) (Δ : X _[n]) : X.Path n where
+  vertex i := X.map (SimplexCategory.const [0] [n] i).op Δ
+  arrow i := X.map (SimplexCategory.mkOfSucc i).op Δ
+  arrow_src i := by
+    dsimp [SimplicialObject.δ]
+    simp only [← FunctorToTypes.map_comp_apply, ← op_comp]
+    rw [SimplexCategory.δ_one_mkOfSucc]
+    simp only [len_mk, Fin.coe_castSucc, Fin.coe_eq_castSucc]
+  arrow_tgt i := by
+    dsimp [SimplicialObject.δ]
+    simp only [← FunctorToTypes.map_comp_apply, ← op_comp]
+    rw [SimplexCategory.δ_zero_mkOfSucc]
+
+lemma spine_map_subinterval {n : ℕ} (j l : ℕ) (hjl : j + l ≤ n) (Δ : X _[n]) :
+    X.spine l (X.map (subinterval j l (by omega)).op Δ) =
+      (X.spine n Δ).interval j l (by omega) := by
+  ext i
+  · simp only [spine_vertex, Path.interval, ← FunctorToTypes.map_comp_apply, ← op_comp,
+      const_subinterval_eq]
+  · simp only [spine_arrow, Path.interval, ← FunctorToTypes.map_comp_apply, ← op_comp,
+      mkOfSucc_subinterval_eq]
+
+end SSet

Mathlib/AlgebraicTopology/SimplicialSet/StrictSegal.lean

@@ -0,0 +1,121 @@
+/-
+Copyright (c) 2024 Emily Riehl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro, Emily Riehl, Joël Riou
+-/
+import Mathlib.AlgebraicTopology.SimplicialSet.Nerve
+import Mathlib.AlgebraicTopology.SimplicialSet.Path
+import Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
+import Mathlib.CategoryTheory.Functor.KanExtension.Basic
+
+/-!
+# Strict Segal simplicial sets
+
+A simplicial set `X` satisfies the `StrictSegal` condition if for all `n`, the map
+`X.spine n : X _[n] → X.Path n` is an equivalence, with equivalence inverse
+`spineToSimplex {n : ℕ} : Path X n → X _[n]`.
+
+Examples of `StrictSegal` simplicial sets are given by nerves of categories.
+
+TODO: Show that these are the only examples: that a `StrictSegal` simplicial set is isomorphic to
+the nerve of its homotopy category.
+-/
+
+universe v u
+
+open CategoryTheory
+
+open Simplicial SimplicialObject SimplexCategory
+
+namespace SSet
+
+variable (X : SSet.{u})
+
+/-- A simplicial set `X` satisfies the strict Segal condition if its simplices are uniquely
+determined by their spine. -/
+class StrictSegal where
+  /-- The inverse to `X.spine n`.-/
+  spineToSimplex {n : ℕ} : Path X n → X _[n]
+  /-- `spineToSimplex` is a right inverse to `X.spine n`.-/
+  spine_spineToSimplex {n : ℕ} (f : Path X n) : X.spine n (spineToSimplex f) = f
+  /-- `spineToSimplex` is a left inverse to `X.spine n`.-/
+  spineToSimplex_spine {n : ℕ} (Δ : X _[n]) : spineToSimplex (X.spine n Δ) = Δ
+
+namespace StrictSegal
+variable {X : SSet.{u}} [StrictSegal X] {n : ℕ}
+
+/-- The fields of `StrictSegal` define an equivalence between `X _[n]` and `Path X n`.-/
+def spineEquiv (n : ℕ) : X _[n] ≃ Path X n where
+  toFun := spine X n
+  invFun := spineToSimplex
+  left_inv := spineToSimplex_spine
+  right_inv := spine_spineToSimplex
+
+theorem spineInjective {n : ℕ} : Function.Injective (spineEquiv (X := X) n) := Equiv.injective _
+
+@[simp]
+theorem spineToSimplex_vertex (i : Fin (n + 1)) (f : Path X n) :
+    X.map (const [0] [n] i).op (spineToSimplex f) = f.vertex i := by
+  rw [← spine_vertex, spine_spineToSimplex]
+
+@[simp]
+theorem spineToSimplex_arrow (i : Fin n) (f : Path X n) :
+    X.map (mkOfSucc i).op (spineToSimplex f) = f.arrow i := by
+  rw [← spine_arrow, spine_spineToSimplex]
+
+/-- In the presence of the strict Segal condition, a path of length `n` can be "composed" by taking
+the diagonal edge of the resulting `n`-simplex. -/
+def spineToDiagonal (f : Path X n) : X _[1] := diagonal X (spineToSimplex f)
+
+@[simp]
+theorem spineToSimplex_interval (f : Path X n) (j l : ℕ) (hjl : j + l ≤  n)  :
+    X.map (subinterval j l hjl).op (spineToSimplex f) =
+      spineToSimplex (Path.interval f j l hjl) := by
+  apply spineInjective
+  unfold spineEquiv
+  dsimp
+  rw [spine_spineToSimplex]
+  convert spine_map_subinterval X j l hjl (spineToSimplex f)
+  exact Eq.symm (spine_spineToSimplex f)
+
+theorem spineToSimplex_edge (f : Path X n) (j l : ℕ) (hjl : j + l ≤ n) :
+    X.map (intervalEdge j l hjl).op (spineToSimplex f) =
+      spineToDiagonal (Path.interval f j l hjl) := by
+  unfold spineToDiagonal
+  rw [← congrArg (diagonal X) (spineToSimplex_interval f j l hjl)]
+  unfold diagonal
+  simp only [← FunctorToTypes.map_comp_apply, ← op_comp, diag_subinterval_eq]
+
+end StrictSegal
+
+end SSet
+
+namespace Nerve
+
+open SSet
+
+variable {C : Type*} [Category C] {n : ℕ}
+
+/-- Simplices in the nerve of categories are uniquely determined by their spine. Indeed, this
+property describes the essential image of the nerve functor.-/
+noncomputable instance strictSegal (C : Type u) [Category.{v} C] : StrictSegal (nerve C) where
+  spineToSimplex {n} F :=
+    ComposableArrows.mkOfObjOfMapSucc (fun i ↦ (F.vertex i).obj 0)
+      (fun i ↦ eqToHom (Functor.congr_obj (F.arrow_src i).symm 0) ≫
+        (F.arrow i).map' 0 1 ≫ eqToHom (Functor.congr_obj (F.arrow_tgt i) 0))
+  spine_spineToSimplex {n} F := by
+    ext i
+    · exact ComposableArrows.ext₀ rfl
+    · refine ComposableArrows.ext₁ ?_ ?_ ?_
+      · exact Functor.congr_obj (F.arrow_src i).symm 0
+      · exact Functor.congr_obj (F.arrow_tgt i).symm 0
+      · dsimp
+        apply ComposableArrows.mkOfObjOfMapSucc_map_succ
+  spineToSimplex_spine {n} F := by
+    fapply ComposableArrows.ext
+    · intro i
+      rfl
+    · intro i hi
+      apply ComposableArrows.mkOfObjOfMapSucc_map_succ
+
+end Nerve