refactor(AlgebraicTopology/SimplicialSet): truncated paths (#20668)

We refactor the `StrictSegal` infrastructure, making two notable changes:
- The `StrictSegal` class is redefined as a structure, and the class `IsStrictSegal X : Prop` is added in its place.
- `Path`, `StrictSegal`, and related constructions are defined for truncated simplicial sets. A path in a simplicial set `X` is then defined as a 1-truncated path in the 1-truncation of `X`. 



Co-authored-by: gio256 <102917377+gio256@users.noreply.github.com>
Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>

Author: gio256

Mathlib/AlgebraicTopology/Quasicategory/StrictSegal.lean

@@ -25,28 +25,28 @@ open Simplicial SimplicialObject SimplexCategory
 namespace SSet.StrictSegal
 
 /-- Any `StrictSegal` simplicial set is a `Quasicategory`. -/
-instance quasicategory {X : SSet.{u}} [StrictSegal X] : Quasicategory X := by
+theorem quasicategory {X : SSet.{u}} (sx : StrictSegal X) : Quasicategory X := by
   apply quasicategory_of_filler X
   intro n i σ₀ h₀ hₙ
-  use spineToSimplex <| Path.map (horn.spineId i h₀ hₙ) σ₀
+  use sx.spineToSimplex <| Path.map (horn.spineId i h₀ hₙ) σ₀
   intro j hj
-  apply spineInjective
+  apply sx.spineInjective
   ext k
   dsimp only [spineEquiv, spine_arrow, Function.comp_apply, Equiv.coe_fn_mk]
   rw [← types_comp_apply (σ₀.app _) (X.map _), ← σ₀.naturality]
   let ksucc := k.succ.castSucc
   obtain hlt | hgt | heq : ksucc < j ∨ j < ksucc ∨ j = ksucc := by omega
-  · rw [← spine_arrow, spine_δ_arrow_lt _ hlt]
-    dsimp only [Path.map, spine_arrow, Fin.coe_eq_castSucc]
+  · rw [← spine_arrow, spine_δ_arrow_lt sx _ hlt]
+    dsimp only [Path.map_arrow, spine_arrow, Fin.coe_eq_castSucc]
     apply congr_arg
     apply Subtype.ext
     dsimp [horn.face, CosimplicialObject.δ]
     rw [Subcomplex.yonedaEquiv_coe, Subpresheaf.lift_ι, stdSimplex.map_apply,
       Quiver.Hom.unop_op, stdSimplex.yonedaEquiv_map, Equiv.apply_symm_apply,
       mkOfSucc_δ_lt hlt]
     rfl
-  · rw [← spine_arrow, spine_δ_arrow_gt _ hgt]
-    dsimp only [Path.map, spine_arrow, Fin.coe_eq_castSucc]
+  · rw [← spine_arrow, spine_δ_arrow_gt sx _ hgt]
+    dsimp only [Path.map_arrow, spine_arrow, Fin.coe_eq_castSucc]
     apply congr_arg
     apply Subtype.ext
     dsimp [horn.face, CosimplicialObject.δ]
@@ -68,14 +68,14 @@ instance quasicategory {X : SSet.{u}} [StrictSegal X] : Quasicategory X := by
       have hi : ((horn.spineId i h₀ hₙ).map σ₀).interval k 2 (by omega) =
           X.spine 2 (σ₀.app _ triangle) := by
         ext m
-        dsimp [spine_arrow, Path.interval, Path.map]
+        dsimp [spine_arrow, Path.map_interval, Path.map_arrow]
         rw [← types_comp_apply (σ₀.app _) (X.map _), ← σ₀.naturality]
         apply congr_arg
         apply Subtype.ext
         ext a : 1
         fin_cases a <;> fin_cases m <;> rfl
-      rw [← spine_arrow, spine_δ_arrow_eq _ heq, hi]
-      simp only [spineToDiagonal, diagonal, spineToSimplex_spine]
+      rw [← spine_arrow, spine_δ_arrow_eq sx _ heq, hi]
+      simp only [spineToDiagonal, diagonal, spineToSimplex_spine_apply]
       rw [← types_comp_apply (σ₀.app _) (X.map _), ← σ₀.naturality, types_comp_apply]
       apply congr_arg
       apply Subtype.ext
@@ -89,4 +89,8 @@ instance quasicategory {X : SSet.{u}} [StrictSegal X] : Quasicategory X := by
       rw [mkOfSucc_δ_eq heq]
       fin_cases z <;> rfl
 
+/-- Any simplicial set satisfying `IsStrictSegal` is a `Quasicategory`. -/
+instance quasicategory' (X : SSet.{u}) [IsStrictSegal X] : Quasicategory X :=
+  quasicategory <| ofIsStrictSegal X
+
 end SSet.StrictSegal

Mathlib/AlgebraicTopology/SimplexCategory/Defs.lean

@@ -176,19 +176,46 @@ noncomputable def inclusion.fullyFaithful (n : ℕ) :
 theorem Hom.ext {n} {a b : Truncated n} (f g : a ⟶ b) :
     f.toOrderHom = g.toOrderHom → f = g := SimplexCategory.Hom.ext _ _
 
+/-- A quick attempt to prove that `⦋m⦌` is `n`-truncated (`⦋m⦌.len ≤ n`). -/
+scoped macro "trunc" : tactic =>
+  `(tactic| first | assumption | dsimp only [SimplexCategory.len_mk] <;> omega)
+
 open Mathlib.Tactic (subscriptTerm) in
 /-- For `m ≤ n`, `⦋m⦌ₙ` is the `m`-dimensional simplex in `Truncated n`. The
 proof `p : m ≤ n` can also be provided using the syntax `⦋m, p⦌ₙ`. -/
 scoped syntax:max (name := mkNotation)
   "⦋" term ("," term)? "⦌" noWs subscriptTerm : term
 scoped macro_rules
   | `(⦋$m:term⦌$n:subscript) =>
-    `((⟨SimplexCategory.mk $m, by first | get_elem_tactic |
+    `((⟨SimplexCategory.mk $m, by first | trunc |
       fail "Failed to prove truncation property. Try writing `⦋m, by ...⦌ₙ`."⟩ :
       SimplexCategory.Truncated $n))
   | `(⦋$m:term, $p:term⦌$n:subscript) =>
     `((⟨SimplexCategory.mk $m, $p⟩ : SimplexCategory.Truncated $n))
 
+/-- Make a morphism in `Truncated n` from a morphism in `SimplexCategory`. This
+is equivalent to `@id (⦋a⦌ₙ ⟶ ⦋b⦌ₙ) f`. -/
+abbrev Hom.tr {n : ℕ} {a b : SimplexCategory} (f : a ⟶ b)
+    (ha : a.len ≤ n := by trunc) (hb : b.len ≤ n := by trunc) :
+    (⟨a, ha⟩ : Truncated n) ⟶ ⟨b, hb⟩ :=
+  f
+
+lemma Hom.tr_comp {n : ℕ} {a b c : SimplexCategory} (f : a ⟶ b) (g : b ⟶ c)
+    (ha : a.len ≤ n := by trunc) (hb : b.len ≤ n := by trunc)
+    (hc : c.len ≤ n := by trunc) :
+    tr (f ≫ g) = tr f ≫ tr g :=
+  rfl
+
+/-- The inclusion of `Truncated n` into `Truncated m` when `n ≤ m`. -/
+def incl (n m : ℕ) (h : n ≤ m := by omega) : Truncated n ⥤ Truncated m where
+  obj a := ⟨a.1, a.2.trans h⟩
+  map := id
+
+/-- For all `n ≤ m`, `inclusion n` factors through `Truncated m`. -/
+def inclCompInclusion {n m : ℕ} (h : n ≤ m) :
+    incl n m ⋙ inclusion m ≅ inclusion n :=
+  Iso.refl _
+
 end Truncated
 
 end SimplexCategory

Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean

@@ -264,6 +264,12 @@ scoped macro_rules
     `(($X : CategoryTheory.SimplicialObject.Truncated _ $n).obj
       (Opposite.op ⟨SimplexCategory.mk $m, $p⟩))
 
+variable (C) in
+/-- Further truncation of truncated simplicial objects. -/
+@[simps!]
+def trunc (n m : ℕ) (h : m ≤ n := by omega) : Truncated C n ⥤ Truncated C m :=
+  (whiskeringLeft _ _ _).obj (SimplexCategory.Truncated.incl m n).op
+
 end Truncated
 
 section Truncation
@@ -272,6 +278,11 @@ section Truncation
 def truncation (n : ℕ) : SimplicialObject C ⥤ SimplicialObject.Truncated C n :=
   (whiskeringLeft _ _ _).obj (SimplexCategory.Truncated.inclusion n).op
 
+/-- For all `m ≤ n`, `truncation m` factors through `Truncated n`. -/
+def truncationCompTrunc {n m : ℕ} (h : m ≤ n) :
+    truncation n ⋙ Truncated.trunc C n m ≅ truncation m :=
+  Iso.refl _
+
 end Truncation
 
 
@@ -717,6 +728,11 @@ scoped macro_rules
     `(($X : CategoryTheory.CosimplicialObject.Truncated _ $n).obj
       ⟨SimplexCategory.mk $m, $p⟩)
 
+variable (C) in
+/-- Further truncation of truncated cosimplicial objects. -/
+def trunc (n m : ℕ) (h : m ≤ n := by omega) : Truncated C n ⥤ Truncated C m :=
+  (whiskeringLeft _ _ _).obj <| SimplexCategory.Truncated.incl m n
+
 end Truncated
 
 section Truncation
@@ -725,6 +741,11 @@ section Truncation
 def truncation (n : ℕ) : CosimplicialObject C ⥤ CosimplicialObject.Truncated C n :=
   (whiskeringLeft _ _ _).obj (SimplexCategory.Truncated.inclusion n)
 
+/-- For all `m ≤ n`, `truncation m` factors through `Truncated n`. -/
+def truncationCompTrunc {n m : ℕ} (h : m ≤ n) :
+    truncation n ⋙ Truncated.trunc C n m ≅ truncation m :=
+  Iso.refl _
+
 end Truncation
 
 variable (C)

Mathlib/AlgebraicTopology/SimplicialSet/Basic.lean

@@ -81,31 +81,45 @@ def uliftFunctor : SSet.{u} ⥤ SSet.{max u v} :=
 def Truncated (n : ℕ) :=
   SimplicialObject.Truncated (Type u) n
 
-instance Truncated.largeCategory (n : ℕ) : LargeCategory (Truncated n) := by
+namespace Truncated
+
+instance largeCategory (n : ℕ) : LargeCategory (Truncated n) := by
   dsimp only [Truncated]
   infer_instance
 
-instance Truncated.hasLimits {n : ℕ} : HasLimits (Truncated n) := by
+instance hasLimits {n : ℕ} : HasLimits (Truncated n) := by
   dsimp only [Truncated]
   infer_instance
 
-instance Truncated.hasColimits {n : ℕ} : HasColimits (Truncated n) := by
+instance hasColimits {n : ℕ} : HasColimits (Truncated n) := by
   dsimp only [Truncated]
   infer_instance
 
 /-- The ulift functor `SSet.Truncated.{u} ⥤ SSet.Truncated.{max u v}` on truncated
 simplicial sets. -/
-def Truncated.uliftFunctor (k : ℕ) : SSet.Truncated.{u} k ⥤ SSet.Truncated.{max u v} k :=
+def uliftFunctor (k : ℕ) : SSet.Truncated.{u} k ⥤ SSet.Truncated.{max u v} k :=
   (whiskeringRight _ _ _).obj CategoryTheory.uliftFunctor.{v, u}
 
 @[ext]
-lemma Truncated.hom_ext {n : ℕ} {X Y : Truncated n} {f g : X ⟶ Y} (w : ∀ n, f.app n = g.app n) :
+lemma hom_ext {n : ℕ} {X Y : Truncated n} {f g : X ⟶ Y} (w : ∀ n, f.app n = g.app n) :
     f = g :=
   NatTrans.ext (funext w)
 
+/-- Further truncation of truncated simplicial sets. -/
+abbrev trunc (n m : ℕ) (h : m ≤ n := by omega) :
+    SSet.Truncated n ⥤ SSet.Truncated m :=
+  SimplicialObject.Truncated.trunc (Type u) n m
+
+end Truncated
+
 /-- The truncation functor on simplicial sets. -/
 abbrev truncation (n : ℕ) : SSet ⥤ SSet.Truncated n := SimplicialObject.truncation n
 
+/-- For all `m ≤ n`, `truncation m` factors through `SSet.Truncated n`. -/
+def truncationCompTrunc {n m : ℕ} (h : m ≤ n) :
+    truncation n ⋙ Truncated.trunc n m ≅ truncation m :=
+  Iso.refl _
+
 open SimplexCategory
 
 noncomputable section

Mathlib/AlgebraicTopology/SimplicialSet/Coskeletal.lean

@@ -46,7 +46,7 @@ section
 open StructuredArrow
 
 namespace StrictSegal
-variable (X : SSet.{u}) [StrictSegal X]
+variable {X : SSet.{u}} (sx : StrictSegal X)
 
 namespace isPointwiseRightKanExtensionAt
 
@@ -60,10 +60,10 @@ abbrev strArrowMk₂ {i : ℕ} {n : ℕ} (φ : ⦋i⦌ ⟶ ⦋n⦌) (hi : i ≤
 `(proj (op ⦋n⦌) ((Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)` where `X` is
 Strict Segal, one can produce an `n`-simplex in `X`. -/
 @[simp]
-noncomputable def lift {X : SSet.{u}} [StrictSegal X] {n}
+noncomputable def lift {X : SSet.{u}} (sx : StrictSegal X) {n}
     (s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙
       (Truncated.inclusion 2).op ⋙ X)) (x : s.pt) : X _⦋n⦌ :=
-  StrictSegal.spineToSimplex {
+  sx.spineToSimplex {
     vertex := fun i ↦ s.π.app (.mk (Y := op ⦋0⦌₂) (.op (SimplexCategory.const _ _ i))) x
     arrow := fun i ↦ s.π.app (.mk (Y := op ⦋1⦌₂) (.op (mkOfLe _ _ (Fin.castSucc_le_succ i)))) x
     arrow_src := fun i ↦ by
@@ -83,7 +83,7 @@ noncomputable def lift {X : SSet.{u}} [StrictSegal X] {n}
 lemma fac_aux₁ {n : ℕ}
     (s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X))
     (x : s.pt) (i : ℕ) (hi : i < n) :
-    X.map (mkOfSucc ⟨i, hi⟩).op (lift s x) =
+    X.map (mkOfSucc ⟨i, hi⟩).op (lift sx s x) =
       s.π.app (strArrowMk₂ (mkOfSucc ⟨i, hi⟩)) x := by
   dsimp [lift]
   rw [spineToSimplex_arrow]
@@ -92,7 +92,7 @@ lemma fac_aux₁ {n : ℕ}
 lemma fac_aux₂ {n : ℕ}
     (s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X))
     (x : s.pt) (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n) :
-    X.map (mkOfLe ⟨i, by omega⟩ ⟨j, by omega⟩ hij).op (lift s x) =
+    X.map (mkOfLe ⟨i, by omega⟩ ⟨j, by omega⟩ hij).op (lift sx s x) =
       s.π.app (strArrowMk₂ (mkOfLe ⟨i, by omega⟩ ⟨j, by omega⟩ hij)) x := by
   obtain ⟨k, hk⟩ := Nat.le.dest hij
   revert i j
@@ -123,23 +123,22 @@ lemma fac_aux₂ {n : ℕ}
           ⟨j, by omega⟩ (by simp) (by simp only [Fin.mk_le_mk]; omega))
       let α₀ := strArrowMk₂ (mkOfLe (n := n) ⟨i + k, by omega⟩ ⟨j, by omega⟩
         (by simp only [Fin.mk_le_mk]; omega))
-      let α₁ := strArrowMk₂ (mkOfLe (n := n) ⟨i, by omega⟩ ⟨j, by omega⟩
-        (by simp only [Fin.mk_le_mk]; omega))
+      let α₁ := strArrowMk₂ (mkOfLe (n := n) ⟨i, by omega⟩ ⟨j, by omega⟩ hij)
       let α₂ := strArrowMk₂ (mkOfLe (n := n) ⟨i, by omega⟩ ⟨i + k, by omega⟩ (by simp))
       let β₀ : α ⟶ α₀ := StructuredArrow.homMk ((mkOfSucc 1).op) (Quiver.Hom.unop_inj
         (by ext x; fin_cases x <;> rfl))
       let β₁ : α ⟶ α₁ := StructuredArrow.homMk ((δ 1).op) (Quiver.Hom.unop_inj
         (by ext x; fin_cases x <;> rfl))
       let β₂ : α ⟶ α₂ := StructuredArrow.homMk ((mkOfSucc 0).op) (Quiver.Hom.unop_inj
         (by ext x; fin_cases x <;> rfl))
-      have h₀ : X.map α₀.hom (lift s x) = s.π.app α₀ x := by
+      have h₀ : X.map α₀.hom (lift sx s x) = s.π.app α₀ x := by
         subst hik
         exact fac_aux₁ _ _ _ _ hj
-      have h₂ : X.map α₂.hom (lift s x) = s.π.app α₂ x :=
+      have h₂ : X.map α₂.hom (lift sx s x) = s.π.app α₂ x :=
         hk i (i + k) (by simp) (by omega) rfl
-      change X.map α₁.hom (lift s x) = s.π.app α₁ x
-      have : X.map α.hom (lift s x) = s.π.app α x := by
-        apply StrictSegal.spineInjective
+      change X.map α₁.hom (lift sx s x) = s.π.app α₁ x
+      have : X.map α.hom (lift sx s x) = s.π.app α x := by
+        apply sx.spineInjective
         apply Path.ext'
         intro t
         dsimp only [spineEquiv]
@@ -162,7 +161,7 @@ lemma fac_aux₂ {n : ℕ}
 lemma fac_aux₃ {n : ℕ}
     (s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X))
     (x : s.pt) (φ : ⦋1⦌ ⟶ ⦋n⦌) :
-    X.map φ.op (lift s x) = s.π.app (strArrowMk₂ φ) x := by
+    X.map φ.op (lift sx s x) = s.π.app (strArrowMk₂ φ) x := by
   obtain ⟨i, j, hij, rfl⟩ : ∃ i j hij, φ = mkOfLe i j hij :=
     ⟨φ.toOrderHom 0, φ.toOrderHom 1, φ.toOrderHom.monotone (by decide),
       Hom.ext_one_left _ _ rfl rfl⟩
@@ -176,18 +175,18 @@ open isPointwiseRightKanExtensionAt in
 /-- A strict Segal simplicial set is 2-coskeletal. -/
 noncomputable def isPointwiseRightKanExtensionAt (n : ℕ) :
     (rightExtensionInclusion X 2).IsPointwiseRightKanExtensionAt ⟨⦋n⦌⟩ where
-  lift s x := lift (X := X) s x
+  lift s x := lift sx s x
   fac s j := by
     ext x
     obtain ⟨⟨i, hi⟩, ⟨f :  _ ⟶ _⟩, rfl⟩ := j.mk_surjective
     obtain ⟨i, rfl⟩ : ∃ j, SimplexCategory.mk j = i := ⟨_, i.mk_len⟩
     dsimp at hi ⊢
-    apply StrictSegal.spineInjective
+    apply sx.spineInjective
     dsimp
     ext k
     · dsimp only [spineEquiv, Equiv.coe_fn_mk]
       rw [show op f = f.op from rfl]
-      rw [spine_map_vertex, spine_spineToSimplex, spine_vertex]
+      rw [spine_map_vertex, spine_spineToSimplex_apply, spine_vertex]
       let α : strArrowMk₂ f hi ⟶ strArrowMk₂ (⦋0⦌.const ⦋n⦌ (f.toOrderHom k)) :=
         StructuredArrow.homMk ((⦋0⦌.const _ (by exact k)).op) (by simp; rfl)
       exact congr_fun (s.w α).symm x
@@ -198,9 +197,9 @@ noncomputable def isPointwiseRightKanExtensionAt (n : ℕ) :
       exact (isPointwiseRightKanExtensionAt.fac_aux₃ _ _ _ _).trans (congr_fun (s.w α).symm x)
   uniq s m hm := by
     ext x
-    apply StrictSegal.spineInjective (X := X)
+    apply sx.spineInjective (X := X)
     dsimp [spineEquiv]
-    rw [StrictSegal.spine_spineToSimplex]
+    rw [sx.spine_spineToSimplex_apply]
     ext i
     · exact congr_fun (hm (StructuredArrow.mk (Y := op ⦋0⦌₂) (⦋0⦌.const ⦋n⦌ i).op)) x
     · exact congr_fun (hm (.mk (Y := op ⦋1⦌₂) (.op (mkOfLe _ _ (Fin.castSucc_le_succ i))))) x
@@ -209,16 +208,21 @@ noncomputable def isPointwiseRightKanExtensionAt (n : ℕ) :
 cones are limit cones, `rightExtensionInclusion X 2` is a pointwise right Kan extension. -/
 noncomputable def isPointwiseRightKanExtension :
     (rightExtensionInclusion X 2).IsPointwiseRightKanExtension :=
-  fun Δ => isPointwiseRightKanExtensionAt X Δ.unop.len
+  fun Δ => sx.isPointwiseRightKanExtensionAt Δ.unop.len
 
-theorem isRightKanExtension :
+theorem isRightKanExtension (sx : StrictSegal X) :
     X.IsRightKanExtension (𝟙 ((inclusion 2).op ⋙ X)) :=
   RightExtension.IsPointwiseRightKanExtension.isRightKanExtension
-    (isPointwiseRightKanExtension X)
+    sx.isPointwiseRightKanExtension
 
 /-- When `X` is `StrictSegal`, `X` is 2-coskeletal. -/
-instance isCoskeletal : SimplicialObject.IsCoskeletal X 2 where
-  isRightKanExtension := isRightKanExtension X
+theorem isCoskeletal (sx : StrictSegal X) :
+    SimplicialObject.IsCoskeletal X 2 where
+  isRightKanExtension := sx.isRightKanExtension
+
+/-- When `X` satisfies `IsStrictSegal`, `X` is 2-coskeletal. -/
+instance isCoskeletal' [IsStrictSegal X] : SimplicialObject.IsCoskeletal X 2 :=
+  isCoskeletal <| ofIsStrictSegal X
 
 end StrictSegal
 
@@ -232,8 +236,8 @@ namespace Nerve
 
 open SSet
 
-example (C : Type u) [Category.{v} C] :
-    SimplicialObject.IsCoskeletal (nerve C) 2 := by infer_instance
+instance (C : Type u) [Category.{v} C] :
+    SimplicialObject.IsCoskeletal (nerve C) 2 := inferInstance
 
 /-- The essential data of the nerve functor is contained in the 2-truncation, which is
 recorded by the composite functor `nerveFunctor₂`. -/