Theorems · Theorem · algebraic topology

ContinuousMap.Homotopy.eq_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₃}
  (hfg : ∀ (t : ↑unitInterval), f (p t) = g (q t)),
  (FundamentalGroupoid.fundamentalGroupoidFunctor.map (TopCat.ofHom f)).map ⟦p⟧ =
    CategoryTheory.CategoryStruct.comp (ContinuousMap.Homotopy.hcast ⋯)
      (CategoryTheory.CategoryStruct.comp
        ((FundamentalGroupoid.fundamentalGroupoidFunctor.map (TopCat.ofHom g)).map ⟦q⟧)
        (ContinuousMap.Homotopy.hcast ⋯))

Defined in

Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Cited by

2 results in Mathlib

Foundations

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