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.

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)

noncomputable instance 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.