English
The image of a path under f equals the composition of casts and the image under the lifted homotopy, with a diagonal adjustment by a zero-end path.
Русский
Образ пути под действием f равен композиции приведения и образа под поднятой гомотопией с диагональным сдвигом нулевого конца.
LaTeX
$$$$ (\\pi_m (TopCat.ofHom f)).map p = hcast (H.apply_zero x_0)^{ -1} \\gg (\\pi_m TopCat.ofHom H.uliftMap).map (prodToProdTopI (id_{fromTop 0}) p) \\gg hcast (H.apply_zero x_1). $$$$
Lean4
/-- Proof that `f(p) = H(0 ⟶ 0, p)`, with the appropriate casts -/
theorem apply_zero_path :
(πₘ (TopCat.ofHom f)).map p =
hcast (H.apply_zero x₀).symm ≫
(πₘ (TopCat.ofHom H.uliftMap)).map (prodToProdTopI (𝟙 (@fromTop (TopCat.of _) (ULift.up 0))) p) ≫
hcast (H.apply_zero x₁) :=
Quotient.inductionOn p fun p' =>
by
apply @eq_path_of_eq_image _ _ _ _ H.uliftMap _ _ _ _ _ ((Path.refl (ULift.up _)).prod p')
intros
rw [Path.prod_coe, ulift_apply H]
simp
