heq_path_of_eq_image — Mathlib

English

If maps f,g satisfy f(p(t)) = g(q(t)) for all t, then the induced path classes match up to conjugation by start_path and end_path.

Русский

Если отображения f и g удовлетворяют f(p(t)) = g(q(t)) для всех t, то индуцированные классы путей совпадают до конъюгации StartPath и EndPath.

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

/-- 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 -/
theorem heq_path_of_eq_image : (πₘ (TopCat.ofHom f)).map ⟦p⟧ ≍ (πₘ (TopCat.ofHom g)).map ⟦q⟧ := by
  simp only [map_eq, ← Path.Homotopic.map_lift]; apply Path.Homotopic.hpath_hext; exact hfg

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