new PR focused on paths and the strict segal condition

Mathlib.lean

@@ -970,7 +970,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,10 @@ 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 mkOfDiag (n : ℕ) : ([1] : SimplexCategory) ⟶ [n] :=
+  mkOfLe 0 n (Fin.zero_le _)
+
 /-- 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 +244,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 +265,17 @@ 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 ≤ k` of `Fin (n + 1)`.-/
+def subinterval {n} (j l : ℕ) (hjl : j + l < n + 1) :
+    ([l] : SimplexCategory) ⟶ [n] :=
+  SimplexCategory.mkHom {
+    toFun := fun i => ⟨i.1 + j, (by omega)⟩
+    monotone' := by
+      intro i i' hii'
+      simp only [Fin.mk_le_mk, add_le_add_iff_right, Fin.val_fin_le]
+      exact hii'
+  }
+
 instance (Δ : SimplexCategory) : Subsingleton (Δ ⟶ [0]) where
   allEq f g := by ext : 3; apply Subsingleton.elim (α := Fin 1)
 
@@ -466,6 +503,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
+  aesop
+
+@[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/SimplicialSet/Path.lean

@@ -0,0 +1,85 @@
+/-
+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 ≤ k ≤ n`, a path of length `n` restricts to a path of length `k-j`, namely the subpath
+spanned by the vertices `j ≤ i ≤ k` and edges `j ≤ i < k`. -/
+def Path.interval {n : ℕ} (f : Path X n) (j l : ℕ) (hjl : j + l < n + 1) :
+    Path X l where
+  vertex i := f.vertex (Fin.addNat i j)
+  arrow i := f.arrow ⟨Fin.addNat i j, (by omega)⟩
+  arrow_src i := by
+    have eq := f.arrow_src ⟨Fin.addNat i j, (by omega)⟩
+    simp_rw [eq]
+    congr 1
+    apply Fin.eq_of_val_eq
+    simp only [Fin.coe_addNat, Fin.coe_castSucc, Fin.val_natCast]
+    have : i.1 + j < n + 1 := by omega
+    have : (↑i + j) % (n + 1) = i.1 + j := by exact Nat.mod_eq_of_lt this
+    rw [this]
+  arrow_tgt i := by
+    have eq := f.arrow_tgt ⟨Fin.addNat i j, (by omega)⟩
+    simp_rw [eq]
+    congr 1
+    apply Fin.eq_of_val_eq
+    simp only [Fin.coe_addNat, Fin.succ_mk, Fin.val_succ, Fin.val_natCast]
+    have : i.1 + 1 + j < n + 1 := by omega
+    have : (i.1 + 1 + j) % (n + 1) = i.1 + 1 + j := by exact Nat.mod_eq_of_lt this
+    rw [this, Nat.add_right_comm]
+
+/-- 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]
+
+
+
+end SSet