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.

class 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 X.spine n.

• spine_spineToSimplex {n : ℕ} (f : X.Path n) : X.spine n (SSet.StrictSegal.spineToSimplex f) = f

  spineToSimplex is a right inverse to X.spine n.

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

  spineToSimplex is a left inverse to X.spine n.

def SSet.StrictSegal.spineEquiv {X : SSet} [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.

Equations

• SSet.StrictSegal.spineEquiv n = { toFun := X.spine n, invFun := SSet.StrictSegal.spineToSimplex, left_inv := ⋯, right_inv := ⋯ }

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

@[simp]

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

@[simp]

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

def SSet.StrictSegal.spineToDiagonal {X : SSet} [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.

Equations

• SSet.StrictSegal.spineToDiagonal f = CategoryTheory.SimplicialObject.diagonal X (SSet.StrictSegal.spineToSimplex f)

@[simp]

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

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

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

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

theorem SSet.StrictSegal.spine_δ_vertex_lt {X : SSet} [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 (SSet.StrictSegal.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} [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 (SSet.StrictSegal.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} [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 (SSet.StrictSegal.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} [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 (SSet.StrictSegal.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} [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 (SSet.StrictSegal.spineToSimplex f))).arrow i = SSet.StrictSegal.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 instance CategoryTheory.Nerve.strictSegal (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.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.

Equations

• One or more equations did not get rendered due to their size.