Paths in simplicial sets

A path in a simplicial set X of length n is a directed path comprised of n + 1 0-simplices and n 1-simplices, together with identifications between 0-simplices and the sources and targets of the 1-simplices.

An n-simplex has a maximal path, the spine of the simplex, which is a path of length n.

structure SSet.Path (X : SSet) (n : ℕ) : Type u

A path in a simplicial set X of length n is a directed path of n edges.

• vertex : Fin (n + 1) → X.obj (Opposite.op (SimplexCategory.mk 0))

  A path includes the data of n+1 0-simplices in X.

• arrow : Fin n → X.obj (Opposite.op (SimplexCategory.mk 1))

  A path includes the data of n 1-simplices in X.

• arrow_src : ∀ (i : Fin n), CategoryTheory.SimplicialObject.δ X 1 (self.arrow i) = self.vertex i.castSucc

  The sources of the 1-simplices in a path are identified with appropriate 0-simplices.

• arrow_tgt : ∀ (i : Fin n), CategoryTheory.SimplicialObject.δ X 0 (self.arrow i) = self.vertex i.succ

  The targets of the 1-simplices in a path are identified with appropriate 0-simplices.

theorem SSet.Path.ext {X : SSet} {n : ℕ} {x y : X.Path n} (vertex : x.vertex = y.vertex) (arrow : x.arrow = y.arrow) : x = y

def SSet.Path.interval {X : SSet} {n : ℕ} (f : X.Path n) (j l : ℕ) (hjl : j + l ≤ n) : X.Path l

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.

Equations

• f.interval j l hjl = { vertex := fun (i : Fin (l + 1)) => f.vertex ⟨j + ↑i, ⋯⟩, arrow := fun (i : Fin l) => f.arrow ⟨j + ↑i, ⋯⟩, arrow_src := ⋯, arrow_tgt := ⋯ }

def SSet.spine (X : SSet) (n : ℕ) (Δ : X.obj (Opposite.op (SimplexCategory.mk n))) : X.Path n

The spine of an n-simplex in X is the path of edges of length n formed by traversing through its vertices in order.

Equations

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

@[simp]

theorem SSet.spine_arrow (X : SSet) (n : ℕ) (Δ : X.obj (Opposite.op (SimplexCategory.mk n))) (i : Fin n) : (X.spine n Δ).arrow i = X.map (SimplexCategory.mkOfSucc i).op Δ

@[simp]

theorem SSet.spine_vertex (X : SSet) (n : ℕ) (Δ : X.obj (Opposite.op (SimplexCategory.mk n))) (i : Fin (n + 1)) : (X.spine n Δ).vertex i = X.map ((SimplexCategory.mk 0).const (SimplexCategory.mk n) i).op Δ

theorem SSet.spine_map_subinterval (X : SSet) {n : ℕ} (j l : ℕ) (hjl : j + l ≤ n) (Δ : X.obj (Opposite.op (SimplexCategory.mk n))) : X.spine l (X.map (SimplexCategory.subinterval j l ⋯).op Δ) = (X.spine n Δ).interval j l ⋯

theorem SSet.Path.ext' (X : SSet) {n : ℕ} {f g : X.Path (n + 1)} (h : ∀ (i : Fin (n + 1)), f.arrow i = g.arrow i) : f = g

Two paths of the same nonzero length are equal if all of their arrows are equal.