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 (i : Fin (n + 1)) : X.obj (Opposite.op (SimplexCategory.mk 0))

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

• arrow (i : 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_vertex (X : SSet) {n : ℕ} (x : X.obj (Opposite.op (SimplexCategory.mk n))) {m : ℕ} (φ : SimplexCategory.mk m ⟶ SimplexCategory.mk n) (i : Fin (m + 1)) : (X.spine m (X.map φ.op x)).vertex i = (X.spine n x).vertex ((SimplexCategory.Hom.toOrderHom φ) i)

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.

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.

Equations

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

@[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.map_interval {X Y : SSet} {n : ℕ} (f : X.Path n) (σ : X ⟶ Y) (j l : ℕ) (hjl : j + l ≤ n) : (f.map σ).interval j l hjl = (f.interval j l hjl).map σ

Path.map respects subintervals of paths.

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

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

Equations

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

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

Equations

• A.liftPath p hp₀ hp₁ = { vertex := fun (j : Fin (n + 1)) => ⟨p.vertex j, ⋯⟩, arrow := fun (j : Fin n) => ⟨p.arrow j, ⋯⟩, arrow_src := ⋯, arrow_tgt := ⋯ }

@[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].

Equations

• SSet.horn.spineId i h₀ hₙ = (SSet.horn (n + 2) i).liftPath (SSet.stdSimplex.spineId (n + 2)) ⋯ ⋯

@[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_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_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)