Theorems · Theorem · algebraic topology

ContinuousMap.Homotopy.heq_path_of_eq_image

∀ {X₁ X₂ Y : TopCat} {f : C(↑X₁, ↑Y)} {g : C(↑X₂, ↑Y)} {x₀ x₁ : ↑X₁} {x₂ x₃ : ↑X₂} {p : Path x₀ x₁} {q : Path x₂ x₃},
  (∀ (t : ↑unitInterval), f (p t) = g (q t)) →
    (FundamentalGroupoid.fundamentalGroupoidFunctor.map (TopCat.ofHom f)).map ⟦p⟧ ≍
      (FundamentalGroupoid.fundamentalGroupoidFunctor.map (TopCat.ofHom g)).map ⟦q⟧

If f(p(t) = g(q(t)) for two paths p and q, then the induced path homotopy classes f(p) and g(p) are the same as well, despite having a priori different types

Defined in

Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Cited by

1 results in Mathlib

Foundations

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