Theorems · Definition · algebraic topology

SSet.Subcomplex.liftPath

{X : SSet} →
  (A : X.Subcomplex) →
    {n : ℕ} →
      (p : X.Path n) →
        (∀ (j : Fin (n + 1)), p.vertex j ∈ A.obj (Opposite.op { len := 0 })) →
          (∀ (j : Fin n), p.arrow j ∈ A.obj (Opposite.op { len := 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.

Defined in

Mathlib.AlgebraicTopology.SimplicialSet.Path

Cited by

3 results in Mathlib

Foundations

Depth 59 from the axioms · uses propext, Classical.choice, Quot.sound