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. We define this construction first for truncated simplicial sets in SSet.Truncated.Path. A path in a simplicial set X is then defined as a 1-truncated path in the 1-truncation of X.

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

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

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

• vertex : Fin (n + 1) → X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })

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

• arrow : Fin n → X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := ⋯ })

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

• arrow_src (i : Fin n) : X.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op (self.arrow i) = self.vertex i.castSucc

  The source of a 1-simplex in a path is identified with the source vertex.

• arrow_tgt (i : Fin n) : X.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ 0) ⋯ ⋯).op (self.arrow i) = self.vertex i.succ

  The target of a 1-simplex in a path is identified with the target vertex.

theorem SSet.Truncated.Path₁.ext_iff {X : Truncated 1} {n : ℕ} {x y : X.Path₁ n} : x = y ↔ x.vertex = y.vertex ∧ x.arrow = y.arrow

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

def SSet.Truncated.Path {n : ℕ} (X : Truncated (n + 1)) (m : ℕ) : Type u

A path of length m in an n + 1-truncated simplicial set X is given by the data of a Path₁ structure on the further 1-truncation of X.

@[reducible, inline]

abbrev SSet.Truncated.Path.vertex {n : ℕ} {X : Truncated (n + 1)} {m : ℕ} (f : X.Path m) (i : Fin (m + 1)) : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ })

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

@[reducible, inline]

abbrev SSet.Truncated.Path.arrow {n : ℕ} {X : Truncated (n + 1)} {m : ℕ} (f : X.Path m) (i : Fin m) : X.obj (Opposite.op { obj := SimplexCategory.mk 1, property := ⋯ })

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

theorem SSet.Truncated.Path.arrow_src {n : ℕ} {X : Truncated (n + 1)} {m : ℕ} (f : X.Path m) (i : Fin m) : X.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op (f.arrow i) = f.vertex i.castSucc

The source of a 1-simplex in a path is identified with the source vertex.

theorem SSet.Truncated.Path.arrow_tgt {n : ℕ} {X : Truncated (n + 1)} {m : ℕ} (f : X.Path m) (i : Fin m) : X.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ 0) ⋯ ⋯).op (f.arrow i) = f.vertex i.succ

The target of a 1-simplex in a path is identified with the target vertex.

theorem SSet.Truncated.Path.ext {n : ℕ} {X : Truncated (n + 1)} {m : ℕ} {f g : X.Path m} (hᵥ : f.vertex = g.vertex) (hₐ : f.arrow = g.arrow) : f = g

theorem SSet.Truncated.Path.ext_iff {n : ℕ} {X : Truncated (n + 1)} {m : ℕ} {f g : X.Path m} : f = g ↔ f.vertex = g.vertex ∧ f.arrow = g.arrow

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

To show two paths equal it suffices to show that they have the same edges.

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

def SSet.Truncated.Path.interval {n : ℕ} {X : Truncated (n + 1)} {m : ℕ} (f : X.Path m) (j l : ℕ) (h : j + l ≤ m := by omega) : X.Path l

For j + l ≤ m, a path of length m 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 SSet.Truncated.Path.map {n : ℕ} {X Y : Truncated (n + 1)} {m : ℕ} (f : X.Path m) (σ : X ⟶ Y) : Y.Path m

Maps of n + 1-truncated simplicial sets induce maps of paths.

@[simp]

theorem SSet.Truncated.Path.map_vertex {n : ℕ} {X Y : Truncated (n + 1)} {m : ℕ} (f : X.Path m) (σ : X ⟶ Y) (i : Fin (m + 1)) : (f.map σ).vertex i = σ.app (Opposite.op { obj := SimplexCategory.mk 0, property := ⋯ }) (f.vertex i)

@[simp]

theorem SSet.Truncated.Path.map_arrow {n : ℕ} {X Y : Truncated (n + 1)} {m : ℕ} (f : X.Path m) (σ : X ⟶ Y) (i : Fin m) : (f.map σ).arrow i = σ.app (Opposite.op { obj := SimplexCategory.mk 1, property := ⋯ }) (f.arrow i)

theorem SSet.Truncated.Path.map_interval {n : ℕ} {X Y : Truncated (n + 1)} {m : ℕ} (f : X.Path m) (σ : X ⟶ Y) (j l : ℕ) (h : j + l ≤ m) : (f.map σ).interval j l h = (f.interval j l h).map σ

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

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

theorem SSet.Truncated.trunc_spine {n : ℕ} (X : Truncated (n + 1)) (k m : ℕ) (h : m ≤ k + 1) (hₙ : k ≤ n) : ((trunc (n + 1) (k + 1) ⋯).obj X).spine m h = X.spine m ⋯

Further truncating X above m does not change the m-spine.

@[simp]

theorem SSet.Truncated.spine_vertex {n : ℕ} (X : Truncated (n + 1)) (m : ℕ) (hₘ : m ≤ n + 1) (Δ : X.obj (Opposite.op { obj := SimplexCategory.mk m, property := hₘ })) (i : Fin (m + 1)) : (X.spine m hₘ Δ).vertex i = X.map (SimplexCategory.Truncated.Hom.tr ((SimplexCategory.mk 0).const (SimplexCategory.mk m) i) ⋯ hₘ).op Δ

@[simp]

theorem SSet.Truncated.spine_arrow {n : ℕ} (X : Truncated (n + 1)) (m : ℕ) (hₘ : m ≤ n + 1) (Δ : X.obj (Opposite.op { obj := SimplexCategory.mk m, property := hₘ })) (i : Fin m) : (X.spine m hₘ Δ).arrow i = X.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.mkOfSucc i) ⋯ hₘ).op Δ

theorem SSet.Truncated.spine_map_vertex {n : ℕ} (X : Truncated (n + 1)) (m : ℕ) (hₘ : m ≤ n + 1) (Δ : X.obj (Opposite.op { obj := SimplexCategory.mk m, property := hₘ })) (a : ℕ) (hₐ : a ≤ n + 1) (φ : { obj := SimplexCategory.mk a, property := hₐ } ⟶ { obj := SimplexCategory.mk m, property := hₘ }) (i : Fin (a + 1)) : (X.spine a hₐ (X.map φ.op Δ)).vertex i = (X.spine m hₘ Δ).vertex ((SimplexCategory.Hom.toOrderHom φ) i)

theorem SSet.Truncated.spine_map_subinterval {n : ℕ} (X : Truncated (n + 1)) (m : ℕ) (hₘ : m ≤ n + 1) (j l : ℕ) (h : j + l ≤ m) (Δ : X.obj (Opposite.op { obj := SimplexCategory.mk m, property := hₘ })) : X.spine l ⋯ (X.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.subinterval j l h) ⋯ hₘ).op Δ) = (X.spine m hₘ Δ).interval j l h

@[reducible, inline]

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

A path of length n in a simplicial set X is defined as a 1-truncated path in the 1-truncation of X.

@[reducible, inline]

abbrev SSet.Path.vertex {X : SSet} {n : ℕ} (f : X.Path n) (i : Fin (n + 1)) : X.obj (Opposite.op (SimplexCategory.mk 0))

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

@[reducible, inline]

abbrev SSet.Path.arrow {X : SSet} {n : ℕ} (f : X.Path n) (i : Fin n) : X.obj (Opposite.op (SimplexCategory.mk 1))

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

theorem SSet.Path.arrow_src {X : SSet} {n : ℕ} (f : X.Path n) (i : Fin n) : X.map (SimplexCategory.δ 1).op (f.arrow i) = f.vertex i.castSucc

The source of a 1-simplex in a path is identified with the source vertex.

theorem SSet.Path.arrow_tgt {X : SSet} {n : ℕ} (f : X.Path n) (i : Fin n) : X.map (SimplexCategory.δ 0).op (f.arrow i) = f.vertex i.succ

The target of a 1-simplex in a path is identified with the target vertex.

theorem SSet.Path.ext {X : SSet} {n : ℕ} {f g : X.Path n} (hᵥ : f.vertex = g.vertex) (hₐ : f.arrow = g.arrow) : f = g

theorem SSet.Path.ext_iff {X : SSet} {n : ℕ} {f g : X.Path n} : f = g ↔ f.vertex = g.vertex ∧ f.arrow = g.arrow

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

To show two paths equal it suffices to show that they have the same edges.

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

def SSet.Path.interval {X : SSet} {n : ℕ} (f : X.Path n) (j l : ℕ) (h : j + l ≤ n := by omega) : 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.

def SSet.Path.map {X Y : SSet} {n : ℕ} (f : X.Path n) (σ : X ⟶ Y) : Y.Path n

Maps of simplicial sets induce maps of paths in a simplicial set.

@[simp]

theorem SSet.Path.map_vertex {X Y : SSet} {n : ℕ} (f : X.Path n) (σ : X ⟶ Y) (i : Fin (n + 1)) : (f.map σ).vertex i = σ.app (Opposite.op (SimplexCategory.mk 0)) (f.vertex i)

@[simp]

theorem SSet.Path.map_arrow {X Y : SSet} {n : ℕ} (f : X.Path n) (σ : X ⟶ Y) (i : Fin n) : (f.map σ).arrow i = σ.app (Opposite.op (SimplexCategory.mk 1)) (f.arrow i)

theorem SSet.Path.map_interval {X Y : SSet} {n : ℕ} (f : X.Path n) (σ : X ⟶ Y) (j l : ℕ) (h : j + l ≤ n) : (f.map σ).interval j l h = (f.interval j l h).map σ

Path.map respects subintervals of paths.

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 in order through the vertices of X _⦋n⦌ₙ₊₁.

@[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 Δ

@[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 Δ

theorem SSet.truncation_spine (X : SSet) (n m : ℕ) (h : m ≤ n + 1) : ((truncation (n + 1)).obj X).spine m h = X.spine m

For m ≤ n + 1, the m-spine of X factors through the n + 1-truncation of X.

theorem SSet.spine_map_vertex (X : SSet) (n : ℕ) (Δ : X.obj (Opposite.op (SimplexCategory.mk n))) {m : ℕ} (φ : SimplexCategory.mk m ⟶ SimplexCategory.mk n) (i : Fin (m + 1)) : (X.spine m (X.map φ.op Δ)).vertex i = (X.spine n Δ).vertex ((SimplexCategory.Hom.toOrderHom φ) i)

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

def SSet.stdSimplex.spineId (n : ℕ) : (stdSimplex.obj (SimplexCategory.mk n)).Path n

The spine of the unique non-degenerate n-simplex in Δ[n].

@[simp]

theorem SSet.stdSimplex.spineId_vertex (n : ℕ) (i : Fin (n + 1)) : (spineId n).vertex i = obj₀Equiv.symm i

@[simp]

theorem SSet.stdSimplex.spineId_arrow_apply_zero (n : ℕ) (i : Fin n) : ((spineId n).arrow i) 0 = i.castSucc

@[simp]

theorem SSet.stdSimplex.spineId_arrow_apply_one (n : ℕ) (i : Fin n) : ((spineId n).arrow i) 1 = i.succ

def SSet.Subcomplex.liftPath {X : SSet} (A : X.Subcomplex) {n : ℕ} (p : X.Path n) (hp₀ : ∀ (j : Fin (n + 1)), p.vertex j ∈ A.obj (Opposite.op (SimplexCategory.mk 0))) (hp₁ : ∀ (j : Fin n), p.arrow j ∈ A.obj (Opposite.op (SimplexCategory.mk 1))) : A.toSSet.Path n

A path of a simplicial set can be lifted to a subcomplex if the vertices and arrows belong to this subcomplex.

@[simp]

theorem SSet.Subcomplex.liftPath_vertex_coe {X : SSet} (A : X.Subcomplex) {n : ℕ} (p : X.Path n) (hp₀ : ∀ (j : Fin (n + 1)), p.vertex j ∈ A.obj (Opposite.op (SimplexCategory.mk 0))) (hp₁ : ∀ (j : Fin n), p.arrow j ∈ A.obj (Opposite.op (SimplexCategory.mk 1))) (j : Fin (n + 1)) : ↑((A.liftPath p hp₀ hp₁).vertex j) = p.vertex j

@[simp]

theorem SSet.Subcomplex.liftPath_arrow_coe {X : SSet} (A : X.Subcomplex) {n : ℕ} (p : X.Path n) (hp₀ : ∀ (j : Fin (n + 1)), p.vertex j ∈ A.obj (Opposite.op (SimplexCategory.mk 0))) (hp₁ : ∀ (j : Fin n), p.arrow j ∈ A.obj (Opposite.op (SimplexCategory.mk 1))) (j : Fin n) : ↑((A.liftPath p hp₀ hp₁).arrow j) = p.arrow j

@[simp]

theorem SSet.Subcomplex.map_ι_liftPath {X : SSet} (A : X.Subcomplex) {n : ℕ} (p : X.Path n) (hp₀ : ∀ (j : Fin (n + 1)), p.vertex j ∈ A.obj (Opposite.op (SimplexCategory.mk 0))) (hp₁ : ∀ (j : Fin n), p.arrow j ∈ A.obj (Opposite.op (SimplexCategory.mk 1))) : (A.liftPath p hp₀ hp₁).map A.ι = p

def SSet.horn.spineId {n : ℕ} (i : Fin (n + 3)) (h₀ : 0 < i) (hₙ : i < Fin.last (n + 2)) : (horn (n + 2) i).toSSet.Path (n + 2)

Any inner horn contains the spine of the unique non-degenerate n-simplex in Δ[n].

@[simp]

theorem SSet.horn.spineId_arrow_coe {n : ℕ} (i : Fin (n + 3)) (h₀ : 0 < i) (hₙ : i < Fin.last (n + 2)) (j : Fin (n + 2)) : ↑((spineId i h₀ hₙ).arrow j) = (stdSimplex.spineId (n + 2)).arrow j

@[simp]

theorem SSet.horn.spineId_vertex_coe {n : ℕ} (i : Fin (n + 3)) (h₀ : 0 < i) (hₙ : i < Fin.last (n + 2)) (j : Fin (n + 2 + 1)) : ↑((spineId i h₀ hₙ).vertex j) = stdSimplex.const (n + 2) j (Opposite.op (SimplexCategory.mk 0))

@[simp]

theorem SSet.horn.spineId_map_hornInclusion {n : ℕ} (i : Fin (n + 3)) (h₀ : 0 < i) (hₙ : i < Fin.last (n + 2)) : (spineId i h₀ hₙ).map (horn (n + 2) i).ι = stdSimplex.spineId (n + 2)