English
A map f: A → X from a simply connected, locally path-connected space lifts uniquely through a covering map p, given a base lift e0 of a0 ∈ A and compatibility conditions for homotopies.
Русский
Подъём уникален: отображение f: A→X из просто связного локально путепроходимого пространства поднимается через покрывающую карту p единственным образом, если задать базовый подъём e0 и условия совместимости для гомотопий.
LaTeX
$$$$\exists! F : C(A,E), F(a_0)=e_0 \land p\circ F = f.$$$$
Lean4
/-- A map `f` from a simply-connected, locally path-connected space `A` to another space `X` lifts
uniquely through a covering map `p : E → X`, after specifying any lift `e₀ : E` of any point
`a₀ : A`. -/
theorem existsUnique_continuousMap_lifts [SimplyConnectedSpace A] [LocPathConnectedSpace A] (f : C(A, X)) (a₀ : A)
(e₀ : E) (he : p e₀ = f a₀) : ∃! F : C(A, E), F a₀ = e₀ ∧ p ∘ F = f :=
by
refine
cov.isLocalHomeomorph.existsUnique_continuousMap_lifts f a₀ e₀ he (fun γ γ_0 ↦ ?_)
fun γ γ' Γ Γ' γ_0 γ'_0 Γ_0 Γ'_0 Γ_lifts Γ'_lifts γγ'1 ↦ ?_
· simpa [and_comm] using cov.exists_path_lifts (f.comp γ) e₀ (by simp [γ_0, he])
let pγ : Path a₀ (γ 1) := ⟨γ, γ_0, rfl⟩
let pγ' : Path a₀ (γ 1) := ⟨γ', γ'_0, γγ'1.symm⟩
convert
cov.liftPath_apply_one_eq_of_homotopicRel
(ContinuousMap.HomotopicRel.comp_continuousMap (SimplyConnectedSpace.paths_homotopic pγ pγ') f) e₀
(by simp [he]) (by simp [he]) <;>
rw [eq_liftPath_iff']
exacts [⟨Γ_lifts, Γ_0⟩, ⟨Γ'_lifts, Γ'_0⟩]
