eq_path_of_eq_image — Mathlib

English

As above, the equality of induced path images under f and g holds up to conjugation by the endpoints of the homotopy.

Русский

Как и выше, равенство индуцированных образов путей под f и g сохраняется с конъюгацией по концам однородности.

LaTeX

$$$$ (\\pi_m (TopCat.ofHom f)).map \\llbracket p \\rrbracket = hcast (start\\_path hfg) \\gg (\\pi_m (TopCat.ofHom g)).map \\llbracket q \\rrbracket \\gg hcast (end\\_path hfg).symm. $$$$

Lean4

theorem eq_path_of_eq_image :
    (πₘ (TopCat.ofHom f)).map ⟦p⟧ =
      hcast (start_path hfg) ≫ (πₘ (TopCat.ofHom g)).map ⟦q⟧ ≫ hcast (end_path hfg).symm :=
  by
  rw [conj_eqToHom_iff_heq ((πₘ (TopCat.ofHom f)).map ⟦p⟧) ((πₘ (TopCat.ofHom g)).map ⟦q⟧)
      (FundamentalGroupoid.ext <| start_path hfg) (FundamentalGroupoid.ext <| end_path hfg)]
  exact heq_path_of_eq_image hfg

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