feat(AlgebraicTopology): inductive definition of StrictSegal

Mathlib/AlgebraicTopology/Quasicategory/StrictSegal.lean

@@ -71,7 +71,7 @@ theorem quasicategory {X : SSet.{u}} (sx : StrictSegal X) : Quasicategory X := b
     /- The interval spanning from `k` to `k + 2` is equivalently the spine
     of the triangle with vertices `k`, `k + 1`, and `k + 2`. -/
     have hi : ((horn.spineId i h₀ hₙ).map σ₀).interval k 2 =
-        X.spine 2 (σ₀.app _ triangle) := by
+        X.spine (σ₀.app _ triangle) := by
       ext m
       dsimp only [spine_arrow]
       rw [← types_comp_apply (σ₀.app _) (X.map _), ← σ₀.naturality]
@@ -81,13 +81,8 @@ theorem quasicategory {X : SSet.{u}} (sx : StrictSegal X) : Quasicategory X := b
       cases n with
       | zero => contradiction
       | succ _ => ext x; fin_cases x <;> fin_cases m <;> rfl
-    rw [spine_δ_arrow_eq sx _ heq, hi]
-    dsimp only [Truncated.StrictSegal.spineToDiagonal, Function.comp_apply]
-    rw [← truncation_spine X (n + 2) 2, (sx _).spineToSimplex_spine_apply 2]
-    dsimp only [truncation, SimplicialObject.truncation, inclusion,
-      whiskeringLeft_obj_obj, Functor.comp_obj, Functor.op_obj,
-      fullSubcategoryInclusion.obj, Functor.comp_map, Functor.op_map,
-      Quiver.Hom.unop_op, fullSubcategoryInclusion.map]
+    rw [spine_δ_arrow_eq sx _ heq, hi, spineToDiagonal_def]
+    simp only [Function.comp_apply, spineToSimplex_spine_apply]
     rw [← types_comp_apply (σ₀.app _) (X.map _), ← σ₀.naturality,
       types_comp_apply]
     apply congr_arg

Mathlib/AlgebraicTopology/SimplexCategory.lean

@@ -755,17 +755,17 @@ section Meta
 /-- Some quick attempts to prove that `[m]` is `n`-truncated (`[m].len ≤ n`). -/
 macro "trunc" : tactic =>
   `(tactic| first | decide | assumption |
-    dsimp only [SimplexCategory.len_mk]; omega |
-    fail "Failed to prove truncation property.")
+    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) (priority := high)
   "[" term ("," term)? "]" noWs subscriptTerm : term
 scoped macro_rules
-  | `([$m:term]$n:subscript) =>
-    `((⟨SimplexCategory.mk $m, by trunc⟩ : SimplexCategory.Truncated $n))
+  | `([$m:term]$n:subscript) => `((⟨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))
 

Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean

@@ -254,14 +254,15 @@ variable {C}
 section Meta
 
 open Mathlib.Tactic (subscriptTerm) in
-/-- For `X : Truncated n` and `m ≤ n`, `X _[m]ₙ` is the `m`-th term of X. The
+/-- For `X : Truncated C n` and `m ≤ n`, `X _[m]ₙ` is the `m`-th term of X. The
 proof `p : m ≤ n` can also be provided using the syntax `X _[m, p]ₙ`. -/
 scoped syntax:max (name := mkNotation) (priority := high)
   term " _[" term ("," term)? "]" noWs subscriptTerm : term
 scoped macro_rules
   | `($X:term _[$m:term]$n:subscript) =>
     `(($X : CategoryTheory.SimplicialObject.Truncated _ $n).obj
-      (Opposite.op ⟨SimplexCategory.mk $m, by trunc⟩))
+      (Opposite.op ⟨SimplexCategory.mk $m, by first | trunc |
+      fail "Failed to prove truncation property. Try writing `X _[m, by ...]ₙ`."⟩))
   | `($X:term _[$m:term, $p:term]$n:subscript) =>
     `(($X : CategoryTheory.SimplicialObject.Truncated _ $n).obj
       (Opposite.op ⟨SimplexCategory.mk $m, $p⟩))
@@ -733,14 +734,15 @@ variable {C}
 section Meta
 
 open Mathlib.Tactic (subscriptTerm) in
-/-- For `X : Truncated n` and `m ≤ n`, `X _[m]ₙ` is the `m`-th term of X. The
+/-- For `X : Truncated C n` and `m ≤ n`, `X _[m]ₙ` is the `m`-th term of X. The
 proof `p : m ≤ n` can also be provided using the syntax `X _[m, p]ₙ`. -/
 scoped syntax:max (name := mkNotation) (priority := high)
   term " _[" term ("," term)? "]" noWs subscriptTerm : term
 scoped macro_rules
   | `($X:term _[$m:term]$n:subscript) =>
     `(($X : CategoryTheory.CosimplicialObject.Truncated _ $n).obj
-      ⟨SimplexCategory.mk $m, by trunc⟩)
+      ⟨SimplexCategory.mk $m, by first | trunc |
+      fail "Failed to prove truncation property. Try writing `X _[m, by ...]ₙ`."⟩)
   | `($X:term _[$m:term, $p:term]$n:subscript) =>
     `(($X : CategoryTheory.CosimplicialObject.Truncated _ $n).obj
       ⟨SimplexCategory.mk $m, $p⟩)

Mathlib/AlgebraicTopology/SimplicialSet/Path.lean

@@ -205,34 +205,37 @@ lemma map_interval (j l : ℕ) (h : j + l ≤ n) :
 
 end Path
 
-/-- The spine of an `n`-simplex in `X` is the path of edges of length `n` formed
-by traversing in order through the vertices of `X _[n]ₙ₊₁`. -/
-abbrev spine (n : ℕ) : X _[n] → Path X n :=
-  truncation (n + 1) |>.obj X |>.spine n
+/-- The spine of an `n + 1`-simplex in `X` is the path of edges of length
+`n + 1` formed by traversing in order through the vertices of `X _[n + 1]ₙ₊₁`. -/
+abbrev spine {n : ℕ} : X _[n + 1] → Path X (n + 1) :=
+  truncation (n + 1) |>.obj X |>.spine (n + 1)
 
-lemma spine_vertex {n : ℕ} (Δ : X _[n]) (i : Fin (n + 1)) :
-    (X.spine n Δ).vertex i = X.map (const [0] [n] i).op Δ := rfl
+lemma spine_vertex {n : ℕ} (Δ : X _[n + 1]) (i : Fin (n + 2)) :
+    (X.spine Δ).vertex i = X.map (const [0] [n + 1] i).op Δ := rfl
 
-lemma spine_arrow {n : ℕ} (Δ : X _[n]) (i : Fin n) :
-    (X.spine n Δ).arrow i = X.map (mkOfSucc i).op Δ := rfl
+lemma spine_arrow {n : ℕ} (Δ : X _[n + 1]) (i : Fin (n + 1)) :
+    (X.spine Δ).arrow i = X.map (mkOfSucc i).op Δ := rfl
 
-/-- For `m ≤ n + 1`, the `m`-spine of `X` factors through the `n + 1`-truncation. -/
-lemma truncation_spine (n m : ℕ) (h : m ≤ n + 1 := by omega) :
-    ((truncation (n + 1)).obj X).spine m = X.spine m := rfl
+/-- For `m ≤ n`, the `m`-spine of `X` factors through the `n + 1`-truncation. -/
+lemma truncation_spine (n m : ℕ) (h : m ≤ n := by omega) :
+    ((truncation (n + 1)).obj X).spine (m + 1) = X.spine := rfl
 
-lemma spine_map_vertex {n : ℕ} (Δ : X _[n]) {m : ℕ} (φ : [m] ⟶ [n])
+lemma spine_map_vertex {n : ℕ} (Δ : X _[n + 1]) {m : ℕ} (φ : [m + 1] ⟶ [n + 1])
     (i : Fin (m + 1)) :
-    (spine X m (X.map φ.op Δ)).vertex i =
-      (spine X n Δ).vertex (φ.toOrderHom i) :=
+    (spine X (X.map φ.op Δ)).vertex i =
+      (spine X Δ).vertex (φ.toOrderHom i) :=
   truncation (max m n + 1) |>.obj X
-    |>.spine_map_vertex n (by omega) Δ m (by omega) φ i
+    |>.spine_map_vertex (n + 1) (by omega) Δ (m + 1) (by omega) φ i
 
-lemma spine_map_subinterval {n : ℕ} (j l : ℕ) (h : j + l ≤ n) (Δ : X _[n]) :
-    X.spine l (X.map (subinterval j l h).op Δ) = (X.spine n Δ).interval j l h :=
-  truncation (n + 1) |>.obj X |>.spine_map_subinterval n _ j l h Δ
+lemma spine_map_subinterval {n : ℕ} (j l : ℕ) (h : j + l ≤ n) (Δ : X _[n + 1]) :
+    X.spine (X.map (subinterval j (l + 1) (by omega)).op Δ) =
+      (X.spine Δ).interval j (l + 1) (by omega) :=
+  truncation (n + 1) |>.obj X
+    |>.spine_map_subinterval (n + 1) _ j (l + 1) _ Δ
 
 /-- The spine of the unique non-degenerate `n`-simplex in `Δ[n]`. -/
-def stdSimplex.spineId (n : ℕ) : Path Δ[n] n := spine Δ[n] n (id n)
+def stdSimplex.spineId (n : ℕ) : Path Δ[n + 1] (n + 1) :=
+  spine Δ[n + 1] (id (n + 1))
 
 /-- Any inner horn contains `stdSimplex.spineId`. -/
 @[simps]
@@ -251,16 +254,16 @@ def horn.spineId {n : ℕ} (i : Fin (n + 3))
   arrow_src := by
     simp only [SimplicialObject.truncation, horn, whiskeringLeft_obj_obj,
       Functor.comp_obj, Functor.comp_map, Subtype.mk.injEq]
-    exact stdSimplex.spineId (n + 2) |>.arrow_src
+    exact stdSimplex.spineId (n + 1) |>.arrow_src
   arrow_tgt := by
     simp only [SimplicialObject.truncation, horn, whiskeringLeft_obj_obj,
       Functor.comp_obj, Functor.comp_map, Subtype.mk.injEq]
-    exact stdSimplex.spineId (n + 2) |>.arrow_tgt
+    exact stdSimplex.spineId (n + 1) |>.arrow_tgt
 
 @[simp]
 lemma horn.spineId_map_hornInclusion {n : ℕ} (i : Fin (n + 3))
     (h₀ : 0 < i) (hₙ : i < Fin.last (n + 2)) :
     Path.map (horn.spineId i h₀ hₙ) (hornInclusion (n + 2) i) =
-      stdSimplex.spineId (n + 2) := rfl
+      stdSimplex.spineId (n + 1) := rfl
 
 end SSet