English
A path in X can be lifted to a path in a subcomplex A as long as all vertices lie in A and all edges lie in A.
Русский
Путь в X может быть возведён в путь в подсложном A, если все вершины лежат в A и все ребра лежат в A.
LaTeX
$$$\text{liftPath}(A,p,hp_0,hp_1) \in \mathrm{Path}(A,n)$ with\ vert_j = (p.vertex j, hp_0 j)\ and\ arrow_j = (p.arrow j, hp_1 j)$$$
Lean4
/-- A path of a simplicial set can be lifted to a subcomplex if the vertices
and arrows belong to this subcomplex. -/
@[simps]
def liftPath {X : SSet.{u}} (A : X.Subcomplex) {n : ℕ} (p : Path X n) (hp₀ : ∀ j, p.vertex j ∈ A.obj _)
(hp₁ : ∀ j, p.arrow j ∈ A.obj _) : Path A n
where
vertex j := ⟨p.vertex j, hp₀ _⟩
arrow j := ⟨p.arrow j, hp₁ _⟩
arrow_src j := Subtype.ext <| p.arrow_src j
arrow_tgt j := Subtype.ext <| p.arrow_tgt j
