feat(AlgebraicTopology): inductive construction of StrictSegal structures (#31250)

We obtain a computable `StrictSegal (nerve C)` structure by using an inductive construction based on a new `StrictSegalCore` structure which provides a way to construct a `n + 1`-simplex by from a `1`-simplex and a `n`-simplex satisfying a compatibility.

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

Author: joelriou

Mathlib/AlgebraicTopology/SimplicialSet/Coskeletal.lean

@@ -243,6 +243,10 @@ instance (C : Type u) [Category.{v} C] :
 recorded by the composite functor `nerveFunctor₂`. -/
 def nerveFunctor₂ : Cat.{v, u} ⥤ SSet.Truncated 2 := nerveFunctor ⋙ truncation 2
 
+instance (X : Cat.{v, u}) : (nerveFunctor₂.obj X).IsStrictSegal := by
+  dsimp [nerveFunctor₂]
+  infer_instance
+
 /-- The natural isomorphism between `nerveFunctor` and `nerveFunctor₂ ⋙ Truncated.cosk 2` whose
 components `nerve C ≅ (Truncated.cosk 2).obj (nerveFunctor₂.obj C)` shows that nerves of categories
 are 2-coskeletal. -/

Mathlib/AlgebraicTopology/SimplicialSet/Path.lean

@@ -198,14 +198,20 @@ abbrev vertex (f : Path X n) (i : Fin (n + 1)) : X _⦋0⦌ :=
 abbrev arrow (f : Path X n) (i : Fin n) : X _⦋1⦌ :=
   Truncated.Path.arrow f i
 
+lemma congr_vertex {f g : Path X n} (h : f = g) (i : Fin (n + 1)) :
+    f.vertex i = g.vertex i := by rw [h]
+
+lemma congr_arrow {f g : Path X n} (h : f = g) (i : Fin n) :
+    f.arrow i = g.arrow i := by rw [h]
+
 /-- The source of a 1-simplex in a path is identified with the source vertex. -/
 lemma arrow_src (f : Path X n) (i : Fin n) :
-    X.map (δ 1).op (f.arrow i) = f.vertex i.castSucc :=
+    X.δ 1 (f.arrow i) = f.vertex i.castSucc :=
   Truncated.Path.arrow_src f i
 
 /-- The target of a 1-simplex in a path is identified with the target vertex. -/
 lemma arrow_tgt (f : Path X n) (i : Fin n) :
-    X.map (δ 0).op (f.arrow i) = f.vertex i.succ :=
+    X.δ 0 (f.arrow i) = f.vertex i.succ :=
   Truncated.Path.arrow_tgt f i
 
 @[ext]
@@ -218,11 +224,23 @@ lemma ext {f g : Path X n} (hᵥ : f.vertex = g.vertex) (hₐ : f.arrow = g.arro
 lemma ext' {f g : Path X (n + 1)} (h : ∀ i, f.arrow i = g.arrow i) : f = g :=
   Truncated.Path.ext' h
 
+@[ext]
+lemma ext₀ {f g : Path X 0} (h : f.vertex 0 = g.vertex 0) : f = g := by
+  ext i
+  · fin_cases i; exact h
+  · fin_cases i
+
 /-- 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 interval (f : Path X n) (j l : ℕ) (h : j + l ≤ n := by omega) : Path X l :=
+def interval (f : Path X n) (j l : ℕ) (h : j + l ≤ n := by grind) : Path X l :=
   Truncated.Path.interval f j l h
 
+lemma arrow_interval (f : Path X n) (j l : ℕ) (k' : Fin l) (k : Fin n)
+    (h : j + l ≤ n := by omega) (hkk' : j + k' = k := by grind) :
+    (f.interval j l h).arrow k' = f.arrow k := by
+  dsimp [interval, arrow, Truncated.Path.interval, Truncated.Path.arrow]
+  congr
+
 variable {X Y : SSet.{u}} {n : ℕ}
 
 /-- Maps of simplicial sets induce maps of paths in a simplicial set. -/
@@ -265,6 +283,20 @@ lemma spine_arrow (Δ : X _⦋n⦌) (i : Fin n) :
     (X.spine n Δ).arrow i = X.map (mkOfSucc i).op Δ :=
   rfl
 
+lemma spine_δ₀ {m : ℕ} (x : X _⦋m + 1⦌) :
+    X.spine m (X.δ 0 x) = (X.spine (m + 1) x).interval 1 m := by
+  obtain _ | m := m
+  · ext
+    simp [spine, Path.vertex, Truncated.Path.vertex, SimplicialObject.truncation,
+      Truncated.spine, Path.interval, Truncated.Path.interval, Truncated.inclusion,
+      Truncated.Hom.tr, ← SimplexCategory.δ_zero_eq_const, ← SimplicialObject.δ_def]
+  · ext i
+    dsimp
+    rw [SimplicialObject.δ_def, ← FunctorToTypes.map_comp_apply, ← op_comp,
+      SimplexCategory.mkOfSucc_δ_gt (j := 0) (i := i) (by simp)]
+    symm
+    exact Path.arrow_interval _ _ _ _ _ _ (by rw [Fin.val_succ, add_comm])
+
 /-- For `m ≤ n + 1`, the `m`-spine of `X` factors through the `n + 1`-truncation
 of `X`. -/
 lemma truncation_spine (m : ℕ) (h : m ≤ n + 1) :

Mathlib/AlgebraicTopology/SimplicialSet/StrictSegal.lean

@@ -48,16 +48,53 @@ structure StrictSegal where
 
 /-- For an `n + 1`-truncated simplicial set `X`, `IsStrictSegal X` asserts the
 mere existence of an inverse to `spine X m` for all `m ≤ n + 1`. -/
-class IsStrictSegal : Prop where
-  segal (m : ℕ) (h : m ≤ n + 1 := by omega) : Function.Bijective (X.spine m)
+class IsStrictSegal (X : SSet.Truncated.{u} (n + 1)) : Prop where
+  spine_bijective (X) (m : ℕ) (h : m ≤ n + 1 := by grind) : Function.Bijective (X.spine m)
+
+export IsStrictSegal (spine_bijective)
+
+@[deprecated (since := "2025-11-04")] alias IsStrictSegal.segal := spine_bijective
+
+lemma spine_injective (X : SSet.Truncated.{u} (n + 1)) [X.IsStrictSegal]
+    {m : ℕ} {h : m ≤ n + 1} :
+    Function.Injective (X.spine m) :=
+  (spine_bijective X m).injective
+
+lemma spine_surjective (X : SSet.Truncated.{u} (n + 1)) [X.IsStrictSegal]
+    {m : ℕ} (p : X.Path m) (h : m ≤ n + 1 := by grind) :
+    ∃ (x : X _⦋m⦌ₙ₊₁), X.spine m _ x = p :=
+  (spine_bijective X m).surjective p
+
+variable {X} in
+lemma IsStrictSegal.ext [X.IsStrictSegal] {d : ℕ} {hd} {x y : X _⦋d + 1⦌ₙ₊₁}
+    (h : ∀ (i : Fin (d + 1)),
+      X.map (SimplexCategory.Truncated.Hom.tr (mkOfSucc i)).op x =
+        X.map (SimplexCategory.Truncated.Hom.tr (mkOfSucc i)).op y) :
+    x = y :=
+  X.spine_injective (by ext i; apply h)
+
+variable {X} in
+lemma IsStrictSegal.hom_ext {Y : SSet.Truncated.{u} (n + 1)} [Y.IsStrictSegal]
+    {f g : X ⟶ Y} (h : ∀ (x : X _⦋1⦌ₙ₊₁), f.app _ x = g.app _ x) : f = g := by
+  ext ⟨⟨m, hm⟩⟩ x
+  induction m using SimplexCategory.rec with | _ m
+  obtain _ | m := m
+  · have fac := δ_comp_σ_self (i := (0 : Fin 1))
+    dsimp at fac
+    simpa [← FunctorToTypes.naturality,
+      ← FunctorToTypes.map_comp_apply, ← op_comp,
+      ← SimplexCategory.Truncated.Hom.tr_comp, fac] using
+      congr_arg (Y.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ 0)).op)
+        (h (X.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.σ 0)).op x))
+  · exact IsStrictSegal.ext (fun i ↦ by simp only [← FunctorToTypes.naturality, h])
 
 namespace StrictSegal
 
 /-- Given `IsStrictSegal X`, a choice of inverse to `spine X m` for all
 `m ≤ n + 1` determines an inhabitant of `StrictSegal X`. -/
 noncomputable def ofIsStrictSegal [IsStrictSegal X] : StrictSegal X where
   spineToSimplex m h :=
-    Equiv.ofBijective (X.spine m) (IsStrictSegal.segal m h) |>.invFun
+    Equiv.ofBijective (X.spine m) (X.spine_bijective m h) |>.invFun
   spine_spineToSimplex m _ :=
     funext <| Equiv.ofBijective (X.spine m) _ |>.right_inv
   spineToSimplex_spine m _ :=
@@ -102,7 +139,7 @@ end autoParam
 /-- The unique existence of an inverse to `spine X m` for all `m ≤ n + 1`
 implies the mere existence of such an inverse. -/
 lemma isStrictSegal (sx : StrictSegal X) : IsStrictSegal X where
-  segal m h := sx.spineEquiv m h |>.bijective
+  spine_bijective m h := sx.spineEquiv m h |>.bijective
 
 variable (m : ℕ) (h : m ≤ n + 1)
 
@@ -245,11 +282,15 @@ variable {X} (sx : StrictSegal X)
 
 /-- A `StrictSegal` structure on a simplicial set `X` restricts to a
 `Truncated.StrictSegal` structure on the `n + 1`-truncation of `X`. -/
-def truncation (n : ℕ) : truncation (n + 1) |>.obj X |>.StrictSegal where
+protected def truncation (n : ℕ) : truncation (n + 1) |>.obj X |>.StrictSegal where
   spineToSimplex _ _ := sx.spineToSimplex
   spine_spineToSimplex m _ := sx.spine_spineToSimplex m
   spineToSimplex_spine m _ := sx.spineToSimplex_spine m
 
+instance [X.IsStrictSegal] (n : ℕ) :
+    ((truncation (n + 1)).obj X).IsStrictSegal :=
+  ((ofIsStrictSegal X).truncation n).isStrictSegal
+
 @[simp]
 lemma spine_spineToSimplex_apply {n : ℕ} (f : Path X n) :
     X.spine n (sx.spineToSimplex f) = f :=
@@ -386,6 +427,79 @@ lemma spine_δ_arrow_eq (h : j = i.succ.castSucc) :
   rw [mkOfSucc_δ_eq h, spineToSimplex_edge]
 
 end StrictSegal
+
+/-- Helper structure in order to show that a simplicial set is strict Segal. -/
+structure StrictSegalCore (n : ℕ) where
+  /-- Map which produces a `n + 1`-simplex from a `1`-simplex and a `n`-simplex when
+  the target vertex of the `1`-simplex equals the zeroth simplex of the `n`-simplex. -/
+  concat (x : X _⦋1⦌) (s : X _⦋n⦌) (h : X.δ 0 x = X.map (SimplexCategory.const _ _ 0).op s) :
+    X _⦋n + 1⦌
+  map_mkOfSucc_zero_concat x s h : X.map (mkOfSucc 0).op (concat x s h) = x
+  δ₀_concat x s h : X.δ 0 (concat x s h) = s
+  injective {x y : X _⦋n + 1⦌} (h : X.map (mkOfSucc 0).op x = X.map (mkOfSucc 0).op y)
+    (h₀ : X.δ 0 x = X.δ 0 y) : x = y
+
+namespace StrictSegalCore
+
+variable {X} (h : ∀ n, X.StrictSegalCore n) {n : ℕ} (p : X.Path n)
+
+/-- Auxiliary definition for `StrictSegalCore.spineToSimplex`. -/
+def spineToSimplexAux : { s : X _⦋n⦌ // X.spine _ s = p } := by
+  induction n with
+  | zero => exact ⟨p.vertex 0, by aesop⟩
+  | succ n hn =>
+    refine ⟨(h n).concat (p.arrow 0) (hn (p.interval 1 n)).val ?_, ?_⟩
+    · rw [p.arrow_tgt 0]
+      exact Path.congr_vertex (hn (p.interval 1 n)).prop.symm 0
+    · ext i
+      obtain rfl | ⟨i, rfl⟩ := i.eq_zero_or_eq_succ
+      · dsimp
+        rw [map_mkOfSucc_zero_concat]
+      · simpa [spine_arrow, ← SimplexCategory.mkOfSucc_δ_gt (j := 0) (i := i) (by simp),
+          op_comp, FunctorToTypes.map_comp_apply, ← SimplicialObject.δ_def, δ₀_concat,
+          ← p.arrow_interval 1 n i i.succ (by grind) (by grind [Fin.val_succ])] using
+            Path.congr_arrow (hn (p.interval 1 n)).prop i
+
+/-- Auxiliary definition for `StrictSegal.ofCore`. -/
+def spineToSimplex : X _⦋n⦌ := (spineToSimplexAux h p).val
+
+@[simp]
+lemma spine_spineToSimplex : X.spine n (spineToSimplex h p) = p := (spineToSimplexAux h p).prop
+
+lemma spineToSimplex_zero (p : X.Path 0) : spineToSimplex h p = p.vertex 0 := rfl
+
+lemma spineToSimplex_succ (p : X.Path (n + 1)) :
+    spineToSimplex h p = (h n).concat (p.arrow 0) (spineToSimplex h (p.interval 1 n)) (by
+      rw [p.arrow_tgt 0]
+      exact Path.congr_vertex (spine_spineToSimplex h (p.interval 1 n)).symm 0) :=
+  rfl
+
+lemma map_mkOfSucc_zero_spineToSimplex (p : X.Path (n + 1)) :
+    X.map (mkOfSucc 0).op (spineToSimplex h p) = p.arrow 0 := by
+  rw [spineToSimplex_succ, map_mkOfSucc_zero_concat]
+
+lemma δ₀_spineToSimplex (p : X.Path (n + 1)) :
+    X.δ 0 (spineToSimplex h p) = spineToSimplex h (p.interval 1 n) := by
+  rw [spineToSimplex_succ, δ₀_concat]
+
+@[simp]
+lemma spineToSimplex_spine (s : X _⦋n⦌) : spineToSimplex h (X.spine _ s) = s := by
+  induction n with
+  | zero => simp [spineToSimplex_zero]
+  | succ n hn =>
+    exact (h n).injective (map_mkOfSucc_zero_spineToSimplex _ _)
+      (by rw [δ₀_spineToSimplex, ← hn (X.δ 0 s), spine_δ₀])
+
+end StrictSegalCore
+
+variable {X} in
+/-- Given a simplicial set `X`, this constructs a `StrictSegal` structure for `X` from
+`StrictSegalCore` structures for all `n : ℕ`. -/
+def StrictSegal.ofCore (h : ∀ n, X.StrictSegalCore n) : X.StrictSegal where
+  spineToSimplex := StrictSegalCore.spineToSimplex h
+  spine_spineToSimplex := by aesop
+  spineToSimplex_spine n := by aesop
+
 end SSet
 
 namespace CategoryTheory.Nerve
@@ -396,27 +510,16 @@ variable (C : Type u) [Category.{v} C]
 
 /-- Simplices in the nerve of categories are uniquely determined by their spine.
 Indeed, this property describes the essential image of the nerve functor. -/
-noncomputable def strictSegal : 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 := by
-    ext F 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 := by
-    ext F
-    fapply ComposableArrows.ext
-    · intro i
-      rfl
-    · intro i hi
-      dsimp
-      exact ComposableArrows.mkOfObjOfMapSucc_map_succ _ _ i hi
+def strictSegal : StrictSegal (nerve C) :=
+  StrictSegal.ofCore (fun n ↦
+    { concat f s h := s.precomp (f.hom ≫ eqToHom (Functor.congr_obj h 0))
+      map_mkOfSucc_zero_concat f s h :=
+        ComposableArrows.ext₁ rfl (Functor.congr_obj h 0).symm (by cat_disch)
+      δ₀_concat f s h := rfl
+      injective {f g} h h₀ :=
+        ComposableArrows.ext_succ (Functor.congr_obj h 0) h₀
+          ((Arrow.mk_eq_mk_iff _ _).1
+            (DFunLike.congr_arg ComposableArrows.arrowEquiv h)).2.2 })
 
 instance isStrictSegal : IsStrictSegal (nerve C) :=
   strictSegal C |>.isStrictSegal

Mathlib/CategoryTheory/ComposableArrows/Basic.lean

@@ -5,6 +5,7 @@ Authors: Joël Riou
 -/
 import Mathlib.Algebra.Group.Nat.Defs
 import Mathlib.CategoryTheory.Category.Preorder
+import Mathlib.CategoryTheory.Comma.Arrow
 import Mathlib.CategoryTheory.EpiMono
 import Mathlib.Data.Fintype.Basic
 import Mathlib.Tactic.FinCases
@@ -275,6 +276,14 @@ lemma ext₁ {F G : ComposableArrows C 1}
 lemma mk₁_surjective (X : ComposableArrows C 1) : ∃ (X₀ X₁ : C) (f : X₀ ⟶ X₁), X = mk₁ f :=
   ⟨_, _, X.map' 0 1, ext₁ rfl rfl (by simp)⟩
 
+/-- The bijection between `ComposableArrows C 1` and `Arrow C`. -/
+@[simps]
+def arrowEquiv : ComposableArrows C 1 ≃ Arrow C where
+  toFun F := Arrow.mk F.hom
+  invFun f := mk₁ f.hom
+  left_inv F := ComposableArrows.ext₁ rfl rfl (by simp)
+  right_inv _ := rfl
+
 variable (F)
 
 namespace Precomp