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 := _proof_1 })

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

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

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

• arrow_src (i : Fin n) : X.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ 1) _proof_1 _proof_5).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) _proof_1 _proof_5).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.

Equations

• X.Path m = ((SSet.Truncated.trunc (n + 1) 1 ⋯).obj X).Path₁ m

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

Equations

• f.vertex i = f.vertex i

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

Equations

• f.arrow i = f.arrow i

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.mk₂ {n : ℕ} {X : Truncated (n + 1)} (p q : X.Path 1) (h : p.vertex 1 = q.vertex 0) : X.Path 2

Constructor for paths of length 2 from two paths of length 1.

Equations

• p.mk₂ q h = { vertex := ![p.vertex 0, p.vertex 1, q.vertex 1], arrow := ![p.arrow 0, q.arrow 0], arrow_src := ⋯, arrow_tgt := ⋯ }

@[simp]

theorem SSet.Truncated.Path.mk₂_arrow {n : ℕ} {X : Truncated (n + 1)} (p q : X.Path 1) (h : p.vertex 1 = q.vertex 0) (a✝ : Fin (Nat.succ 1)) : (p.mk₂ q h).arrow a✝ = ![p.arrow 0, q.arrow 0] a✝

@[simp]

theorem SSet.Truncated.Path.mk₂_vertex {n : ℕ} {X : Truncated (n + 1)} (p q : X.Path 1) (h : p.vertex 1 = q.vertex 0) (a✝ : Fin (Nat.succ 2)) : (p.mk₂ q h).vertex a✝ = ![p.vertex 0, p.vertex 1, q.vertex 1] a✝

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.

Equations

• f.interval j l h = { 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.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.

Equations

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

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

Equations

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

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 φ.hom) 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.

Equations

• X.Path n = ((SSet.truncation 1).obj X).Path n

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

Equations

• f.vertex i = SSet.Truncated.Path.vertex f i

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

Equations

• f.arrow i = SSet.Truncated.Path.arrow f i

theorem SSet.Path.congr_vertex {X : SSet} {n : ℕ} {f g : X.Path n} (h : f = g) (i : Fin (n + 1)) : f.vertex i = g.vertex i

theorem SSet.Path.congr_arrow {X : SSet} {n : ℕ} {f g : X.Path n} (h : f = g) (i : Fin n) : f.arrow i = g.arrow i

theorem SSet.Path.arrow_src {X : SSet} {n : ℕ} (f : X.Path n) (i : Fin n) : CategoryTheory.SimplicialObject.δ X 1 (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) : CategoryTheory.SimplicialObject.δ X 0 (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

theorem SSet.Path.ext₀ {X : SSet} {f g : X.Path 0} (h : f.vertex 0 = g.vertex 0) : f = g

theorem SSet.Path.ext₀_iff {X : SSet} {f g : X.Path 0} : f = g ↔ f.vertex 0 = g.vertex 0

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

theorem SSet.Path.arrow_interval {X : SSet} {n : ℕ} (f : X.Path n) (j l : ℕ) (k' : Fin l) (k : Fin n) (h : j + l ≤ n := by lia) (hkk' : j + ↑k' = ↑k := by grind) : (f.interval j l h).arrow k' = f.arrow k

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

• f.map σ = SSet.Truncated.Path.map f ((SSet.truncation 1).map σ)

@[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⦌ₙ₊₁.

Equations

• X.spine n = ((SSet.truncation (n + 1)).obj X).spine 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.spine_δ₀ (X : SSet) {m : ℕ} (x : X.obj (Opposite.op (SimplexCategory.mk (m + 1)))) : X.spine m (CategoryTheory.SimplicialObject.δ X 0 x) = (X.spine (m + 1) x).interval 1 m ⋯

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

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)