English
Given a lift relation F of f0 and f1 on S and compatible lifts, there exists a lifted relative homotopy rel S between them.
Русский
Дано отношение подъёма F между f0 и f1 относительно S и совместимые подъёмы, существует подъём относительной гомотопии rel S между ними.
LaTeX
$$$$\text{liftHomotopyRel }(F) \text{ exists under hypotheses }$$$
Lean4
/-- The lift to a covering space of a homotopy between two continuous maps relative to a set
given compatible lifts of the continuous maps. -/
noncomputable def liftHomotopyRel [PreconnectedSpace A] {f₀' f₁' : C(A, E)} (he : ∃ a ∈ S, f₀' a = f₁' a)
(h₀ : p ∘ f₀' = f₀) (h₁ : p ∘ f₁' = f₁) : f₀'.HomotopyRel f₁' S :=
have F_0 : ∀ a, F (0, a) = p (f₀' a) := fun a ↦ (F.apply_zero a).trans (congr_fun h₀ a).symm
have rel : ∀ t, ∀ a ∈ S, cov.liftHomotopy F f₀' F_0 (t, a) = f₀' a := fun t a ha ↦
by
rw [liftHomotopy_apply, cov.const_of_comp (ContinuousMap.continuous _) _ t 0]
· apply cov.liftPath_zero
· intro t t'; simp_rw [← p.comp_apply, cov.liftPath_lifts]
exact (F.prop t a ha).trans (F.prop t' a ha).symm
{ toContinuousMap := cov.liftHomotopy F f₀' F_0
map_zero_left := cov.liftHomotopy_zero F f₀' F_0
map_one_left := by
obtain ⟨a, ha, he⟩ := he
simp_rw [toFun_eq_coe, ← curry_apply]
refine congr_fun (cov.eq_of_comp_eq (ContinuousMap.continuous _) f₁'.continuous ?_ a <| (rel 1 a ha).trans he)
ext a; rw [h₁, Function.comp_apply, curry_apply]
exact (congr_fun (cov.liftHomotopy_lifts F f₀' _) (1, a)).trans (F.apply_one a)
prop' := rel }
