equivOfHomotopyEquiv — Mathlib

Lean4

/-- Homotopy equivalent topological spaces have equivalent fundamental groupoids. -/
def equivOfHomotopyEquiv (hequiv : X ≃ₕ Y) : πₓ X ≌ πₓ Y :=
  by
  apply
      CategoryTheory.Equivalence.mk (πₘ (TopCat.ofHom hequiv.toFun) : πₓ X ⥤ πₓ Y)
        (πₘ (TopCat.ofHom hequiv.invFun) : πₓ Y ⥤ πₓ X) <;>
    simp only [← Grpd.id_eq_id]
  · convert (asIso (homotopicMapsNatIso hequiv.left_inv.some)).symm
    exacts [((π).map_id X).symm, ((π).map_comp _ _).symm]
  · convert asIso (homotopicMapsNatIso hequiv.right_inv.some)
    exacts [((π).map_comp _ _).symm, ((π).map_id Y).symm]

Похожие утверждения