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.

StrictSegal simplicial sets have an important property of being 2-coskeletal which is proven in Mathlib/AlgebraicTopology/SimplicialSet/Coskeletal.lean.

structure SSet.Truncated.StrictSegal {n : ℕ} (X : Truncated (n + 1)) : Type u

An n + 1-truncated simplicial set satisfies the strict Segal condition if its m-simplices are uniquely determined by their spine for all m ≤ n + 1.

• spineToSimplex (m : ℕ) (h : m ≤ n + 1 := by omega) : X.Path m → X.obj (Opposite.op { obj := SimplexCategory.mk m, property := h })

  The inverse to spine X m.

• spine_spineToSimplex (m : ℕ) (h : m ≤ n + 1) : X.spine m h ∘ self.spineToSimplex m h = id

  spineToSimplex is a right inverse to spine X m.

• spineToSimplex_spine (m : ℕ) (h : m ≤ n + 1) : self.spineToSimplex m h ∘ X.spine m h = id

  spineToSimplex is a left inverse to spine X m.

class SSet.Truncated.IsStrictSegal {n : ℕ} (X : Truncated (n + 1)) : Prop

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.

• segal (m : ℕ) (h : m ≤ n + 1 := by omega) : Function.Bijective (X.spine m h)

noncomputable def SSet.Truncated.StrictSegal.ofIsStrictSegal {n : ℕ} (X : Truncated (n + 1)) [X.IsStrictSegal] : X.StrictSegal

Given IsStrictSegal X, a choice of inverse to spine X m for all m ≤ n + 1 determines an inhabitant of StrictSegal X.

@[simp]

theorem SSet.Truncated.StrictSegal.spine_spineToSimplex_apply {n : ℕ} {X : Truncated (n + 1)} (sx : X.StrictSegal) (m : ℕ) (h : m ≤ n + 1) (f : X.Path m) : X.spine m h (sx.spineToSimplex m h f) = f

@[simp]

theorem SSet.Truncated.StrictSegal.spineToSimplex_spine_apply {n : ℕ} {X : Truncated (n + 1)} (sx : X.StrictSegal) (m : ℕ) (h : m ≤ n + 1) (Δ : X.obj (Opposite.op { obj := SimplexCategory.mk m, property := h })) : sx.spineToSimplex m h (X.spine m h Δ) = Δ

def SSet.Truncated.StrictSegal.spineEquiv {n : ℕ} {X : Truncated (n + 1)} (sx : X.StrictSegal) (m : ℕ) (h : m ≤ n + 1 := by omega) : X.obj (Opposite.op { obj := SimplexCategory.mk m, property := h }) ≃ X.Path m

The fields of StrictSegal define an equivalence between X _⦋m⦌ₙ₊₁ and Path X m.

theorem SSet.Truncated.StrictSegal.spineInjective {n : ℕ} {X : Truncated (n + 1)} (sx : X.StrictSegal) (m : ℕ) (h : m ≤ n + 1 := by omega) : Function.Injective ⇑(sx.spineEquiv m h)

def SSet.Truncated.StrictSegal.spineToDiagonal {n : ℕ} {X : Truncated (n + 1)} (sx : X.StrictSegal) (m : ℕ) (h : m ≤ n + 1 := by omega) : X.Path m → X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := ⋯ })

In the presence of the strict Segal condition, a path of length m can be "composed" by taking the diagonal edge of the resulting m-simplex.

theorem SSet.Truncated.StrictSegal.isStrictSegal {n : ℕ} {X : Truncated (n + 1)} (sx : X.StrictSegal) : X.IsStrictSegal

The unique existence of an inverse to spine X m for all m ≤ n + 1 implies the mere existence of such an inverse.

@[simp]

theorem SSet.Truncated.StrictSegal.spineToSimplex_vertex {n : ℕ} {X : Truncated (n + 1)} (sx : X.StrictSegal) (m : ℕ) (h : m ≤ n + 1) (i : Fin (m + 1)) (f : X.Path m) : X.map (SimplexCategory.Truncated.Hom.tr ((SimplexCategory.mk 0).const (SimplexCategory.mk m) i) ⋯ h).op (sx.spineToSimplex m h f) = f.vertex i

@[simp]

theorem SSet.Truncated.StrictSegal.spineToSimplex_arrow {n : ℕ} {X : Truncated (n + 1)} (sx : X.StrictSegal) (m : ℕ) (h : m ≤ n + 1) (i : Fin m) (f : X.Path m) : X.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.mkOfSucc i) ⋯ h).op (sx.spineToSimplex m h f) = f.arrow i

@[simp]

theorem SSet.Truncated.StrictSegal.spineToSimplex_interval {n : ℕ} {X : Truncated (n + 1)} (sx : X.StrictSegal) (m : ℕ) (h : m ≤ n + 1) (f : X.Path m) (j l : ℕ) (hjl : j + l ≤ m) : X.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.subinterval j l hjl) ⋯ h).op (sx.spineToSimplex m h f) = sx.spineToSimplex l ⋯ (f.interval j l hjl)

theorem SSet.Truncated.StrictSegal.spineToSimplex_edge {n : ℕ} {X : Truncated (n + 1)} (sx : X.StrictSegal) (m : ℕ) (h : m ≤ n + 1) (f : X.Path m) (j l : ℕ) (hjl : j + l ≤ m) : X.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.intervalEdge j l hjl) ⋯ h).op (sx.spineToSimplex m h f) = sx.spineToDiagonal l ⋯ (f.interval j l hjl)

theorem SSet.Truncated.StrictSegal.spineToSimplex_map {n : ℕ} {X Y : Truncated (n + 1)} (sx : X.StrictSegal) (sy : Y.StrictSegal) (m : ℕ) (h : m ≤ n) (f : X.Path (m + 1)) (σ : X ⟶ Y) : sy.spineToSimplex (m + 1) ⋯ (f.map σ) = σ.app (Opposite.op { obj := SimplexCategory.mk (m + 1), property := ⋯ }) (sx.spineToSimplex (m + 1) ⋯ f)

For any σ : X ⟶ Y between n + 1-truncated StrictSegal simplicial sets, spineToSimplex commutes with Path.map.

theorem SSet.Truncated.StrictSegal.spine_δ_vertex_lt {n : ℕ} {X : Truncated (n + 1)} (sx : X.StrictSegal) (m : ℕ) (h : m ≤ n) (f : X.Path (m + 1)) {i : Fin (m + 1)} {j : Fin (m + 2)} (hij : i.castSucc < j) : (X.spine m ⋯ (X.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ j) ⋯ ⋯).op (sx.spineToSimplex (m + 1) ⋯ f))).vertex i = f.vertex i.castSucc

If we take the path along the spine of the jth face of a spineToSimplex, the common vertices will agree with those of the original path f. In particular, a vertex i with i < j can be identified with the same vertex in f.

theorem SSet.Truncated.StrictSegal.spine_δ_vertex_ge {n : ℕ} {X : Truncated (n + 1)} (sx : X.StrictSegal) (m : ℕ) (h : m ≤ n) (f : X.Path (m + 1)) {i : Fin (m + 1)} {j : Fin (m + 2)} (hij : j ≤ i.castSucc) : (X.spine m ⋯ (X.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ j) ⋯ ⋯).op (sx.spineToSimplex (m + 1) ⋯ f))).vertex i = f.vertex i.succ

If we take the path along the spine of the jth face of a spineToSimplex, a vertex i with j ≤ i can be identified with vertex i + 1 in the original path.

theorem SSet.Truncated.StrictSegal.spine_δ_arrow_lt {n : ℕ} {X : Truncated (n + 1)} (sx : X.StrictSegal) (m : ℕ) (h : m ≤ n) (f : X.Path (m + 1)) {i : Fin m} {j : Fin (m + 2)} (hij : i.succ.castSucc < j) : (X.spine m ⋯ (X.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ j) ⋯ ⋯).op (sx.spineToSimplex (m + 1) ⋯ f))).arrow i = f.arrow i.castSucc

If we take the path along the spine of the jth face of a spineToSimplex, the common arrows will agree with those of the original path f. In particular, an arrow i with i + 1 < j can be identified with the same arrow in f.

theorem SSet.Truncated.StrictSegal.spine_δ_arrow_gt {n : ℕ} {X : Truncated (n + 1)} (sx : X.StrictSegal) (m : ℕ) (h : m ≤ n) (f : X.Path (m + 1)) {i : Fin m} {j : Fin (m + 2)} (hij : j < i.succ.castSucc) : (X.spine m ⋯ (X.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ j) ⋯ ⋯).op (sx.spineToSimplex (m + 1) ⋯ f))).arrow i = f.arrow i.succ

If we take the path along the spine of the jth face of a spineToSimplex, an arrow i with i + 1 > j can be identified with arrow i + 1 in the original path.

theorem SSet.Truncated.StrictSegal.spine_δ_arrow_eq {n : ℕ} {X : Truncated (n + 2)} (sx : X.StrictSegal) (m : ℕ) (h : m ≤ n + 1) (f : X.Path (m + 1)) {i : Fin m} {j : Fin (m + 2)} (hij : j = i.succ.castSucc) : (X.spine m ⋯ (X.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ j) ⋯ ⋯).op (sx.spineToSimplex (m + 1) ⋯ f))).arrow i = sx.spineToDiagonal 2 ⋯ (f.interval (↑i) 2 ⋯)

structure SSet.StrictSegal (X : SSet) : Type u

A simplicial set X satisfies the strict Segal condition if its simplices are uniquely determined by their spine.

• spineToSimplex {n : ℕ} : X.Path n → X.obj (Opposite.op (SimplexCategory.mk n))

  The inverse to spine X n.

• spine_spineToSimplex (n : ℕ) : X.spine n ∘ self.spineToSimplex = id

  spineToSimplex is a right inverse to spine X n.

• spineToSimplex_spine (n : ℕ) : self.spineToSimplex ∘ X.spine n = id

  spineToSimplex is a left inverse to spine X n.

class SSet.IsStrictSegal (X : SSet) : Prop

For X a simplicial set, IsStrictSegal X asserts the mere existence of an inverse to spine X n for all n : ℕ.

• segal (n : ℕ) : Function.Bijective (X.spine n)

noncomputable def SSet.StrictSegal.ofIsStrictSegal (X : SSet) [X.IsStrictSegal] : X.StrictSegal

Given IsStrictSegal X, a choice of inverse to spine X n for all n : ℕ determines an inhabitant of StrictSegal X.

def SSet.StrictSegal.truncation {X : SSet} (sx : X.StrictSegal) (n : ℕ) : ((SSet.truncation (n + 1)).obj X).StrictSegal

A StrictSegal structure on a simplicial set X restricts to a Truncated.StrictSegal structure on the n + 1-truncation of X.

@[simp]

theorem SSet.StrictSegal.spine_spineToSimplex_apply {X : SSet} (sx : X.StrictSegal) {n : ℕ} (f : X.Path n) : X.spine n (sx.spineToSimplex f) = f

@[simp]

theorem SSet.StrictSegal.spineToSimplex_spine_apply {X : SSet} (sx : X.StrictSegal) {n : ℕ} (Δ : X.obj (Opposite.op (SimplexCategory.mk n))) : sx.spineToSimplex (X.spine n Δ) = Δ

def SSet.StrictSegal.spineEquiv {X : SSet} (sx : X.StrictSegal) (n : ℕ) : X.obj (Opposite.op (SimplexCategory.mk n)) ≃ X.Path n

The fields of StrictSegal define an equivalence between X _⦋n⦌ and Path X n.

theorem SSet.StrictSegal.spineInjective {X : SSet} (sx : X.StrictSegal) {n : ℕ} : Function.Injective ⇑(sx.spineEquiv n)

theorem SSet.StrictSegal.isStrictSegal {X : SSet} (sx : X.StrictSegal) : X.IsStrictSegal

The unique existence of an inverse to spine X n forall n : ℕ implies the mere existence of such an inverse.

@[simp]

theorem SSet.StrictSegal.spineToSimplex_vertex {X : SSet} (sx : X.StrictSegal) {n : ℕ} (i : Fin (n + 1)) (f : X.Path n) : X.map ((SimplexCategory.mk 0).const (SimplexCategory.mk n) i).op (sx.spineToSimplex f) = f.vertex i

@[simp]

theorem SSet.StrictSegal.spineToSimplex_arrow {X : SSet} (sx : X.StrictSegal) {n : ℕ} (i : Fin n) (f : X.Path n) : X.map (SimplexCategory.mkOfSucc i).op (sx.spineToSimplex f) = f.arrow i

def SSet.StrictSegal.spineToDiagonal {X : SSet} (sx : X.StrictSegal) {n : ℕ} (f : X.Path n) : X.obj (Opposite.op (SimplexCategory.mk 1))

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.

@[simp]

theorem SSet.StrictSegal.spineToSimplex_interval {X : SSet} (sx : X.StrictSegal) {n : ℕ} (f : X.Path n) (j l : ℕ) (hjl : j + l ≤ n) : X.map (SimplexCategory.subinterval j l hjl).op (sx.spineToSimplex f) = sx.spineToSimplex (f.interval j l hjl)

theorem SSet.StrictSegal.spineToSimplex_edge {X : SSet} (sx : X.StrictSegal) {n : ℕ} (f : X.Path n) (j l : ℕ) (hjl : j + l ≤ n) : X.map (SimplexCategory.intervalEdge j l hjl).op (sx.spineToSimplex f) = sx.spineToDiagonal (f.interval j l hjl)

theorem SSet.StrictSegal.spineToSimplex_map {X Y : SSet} (sx : X.StrictSegal) (sy : Y.StrictSegal) {n : ℕ} (f : X.Path (n + 1)) (σ : X ⟶ Y) : sy.spineToSimplex (f.map σ) = σ.app (Opposite.op (SimplexCategory.mk (n + 1))) (sx.spineToSimplex f)

For any σ : X ⟶ Y between StrictSegal simplicial sets, spineToSimplex commutes with Path.map.

theorem SSet.StrictSegal.spine_δ_vertex_lt {X : SSet} (sx : X.StrictSegal) {n : ℕ} (f : X.Path (n + 1)) {i : Fin (n + 1)} {j : Fin (n + 2)} (h : i.castSucc < j) : (X.spine n (CategoryTheory.SimplicialObject.δ X j (sx.spineToSimplex f))).vertex i = f.vertex i.castSucc

If we take the path along the spine of the jth face of a spineToSimplex, the common vertices will agree with those of the original path f. In particular, a vertex i with i < j can be identified with the same vertex in f.

theorem SSet.StrictSegal.spine_δ_vertex_ge {X : SSet} (sx : X.StrictSegal) {n : ℕ} (f : X.Path (n + 1)) {i : Fin (n + 1)} {j : Fin (n + 2)} (h : j ≤ i.castSucc) : (X.spine n (CategoryTheory.SimplicialObject.δ X j (sx.spineToSimplex f))).vertex i = f.vertex i.succ

If we take the path along the spine of the jth face of a spineToSimplex, a vertex i with i ≥ j can be identified with vertex i + 1 in the original path.

theorem SSet.StrictSegal.spine_δ_arrow_lt {X : SSet} (sx : X.StrictSegal) {n : ℕ} (f : X.Path (n + 1)) {i : Fin n} {j : Fin (n + 2)} (h : i.succ.castSucc < j) : (X.spine n (CategoryTheory.SimplicialObject.δ X j (sx.spineToSimplex f))).arrow i = f.arrow i.castSucc

If we take the path along the spine of the jth face of a spineToSimplex, the common arrows will agree with those of the original path f. In particular, an arrow i with i + 1 < j can be identified with the same arrow in f.

theorem SSet.StrictSegal.spine_δ_arrow_gt {X : SSet} (sx : X.StrictSegal) {n : ℕ} (f : X.Path (n + 1)) {i : Fin n} {j : Fin (n + 2)} (h : j < i.succ.castSucc) : (X.spine n (CategoryTheory.SimplicialObject.δ X j (sx.spineToSimplex f))).arrow i = f.arrow i.succ

If we take the path along the spine of the jth face of a spineToSimplex, an arrow i with i + 1 > j can be identified with arrow i + 1 in the original path.

theorem SSet.StrictSegal.spine_δ_arrow_eq {X : SSet} (sx : X.StrictSegal) {n : ℕ} (f : X.Path (n + 1)) {i : Fin n} {j : Fin (n + 2)} (h : j = i.succ.castSucc) : (X.spine n (CategoryTheory.SimplicialObject.δ X j (sx.spineToSimplex f))).arrow i = sx.spineToDiagonal (f.interval (↑i) 2 ⋯)

If we take the path along the spine of a face of a spineToSimplex, the arrows not contained in the original path can be recovered as the diagonal edge of the spineToSimplex that "composes" arrows i and i + 1.

noncomputable def CategoryTheory.Nerve.strictSegal (C : Type u) [Category.{v, u} C] : (nerve C).StrictSegal

Simplices in the nerve of categories are uniquely determined by their spine. Indeed, this property describes the essential image of the nerve functor.

instance CategoryTheory.Nerve.isStrictSegal (C : Type u) [Category.{v, u} C] : (nerve C).IsStrictSegal