English
A lifting of a homotopy H of maps X into E exists, respecting a base lift f and initial data H0, giving a liftHomotopy: I × A → E that lifts H.
Русский
Существование подъёма гомотопии H из X в E через покрывающую карту, сохраняющее базовую подъемную карту f и начальные данные, образуя liftHomotopy: I × A → E.
LaTeX
$$$$\text{liftHomotopy}: C(I \times A,E)$$ with properties that p ∘ (liftHomotopy) = H and (liftHomotopy)(0,a) = f(a).$$
Lean4
/-- The existence of `liftHomotopy` satisfying `liftHomotopy_lifts` and `liftHomotopy_zero` is
the homotopy lifting property for covering maps.
In other words, a covering map is a Hurewicz fibration. -/
@[simps]
noncomputable def liftHomotopy : C(I × A, E)
where
toFun ta := cov.liftPath (H.comp <| (ContinuousMap.id I).prodMk <| .const I ta.2) (f ta.2) (H_0 ta.2) ta.1
continuous_toFun :=
cov.isLocalHomeomorph.continuous_lift cov.isSeparatedMap H
(by ext ⟨t, a⟩; exact congr_fun (cov.liftPath_lifts ..) t)
(by convert f.continuous with a; exact cov.liftPath_zero ..) fun a ↦ by dsimp only;
exact (cov.liftPath (γ_0 := by simp [*])).2
