English
For a covering map p, a given path γ: I→X and a point e with γ(0)=p(e) admit a lift Γ: I→E with p∘Γ=γ and Γ(0)=e.
Русский
Для покрывающей карты p путь γ: I→X и точка e с γ(0)=p(e) допускают подъём Γ: I→E с p∘Γ=γ и Γ(0)=e.
LaTeX
$$$$\exists Γ: C(I,E),\; p\circ Γ = γ \land Γ(0)=e.$$$$
Lean4
/-- The path lifting property (existence) for covering maps. -/
theorem exists_path_lifts : ∃ Γ : C(I, E), p ∘ Γ = γ ∧ Γ 0 = e :=
by
let U x := (cov x).2.choose
choose mem_base U_open _ H _ using fun x ↦ (cov x).2.choose_spec
obtain ⟨t, t_0, t_mono, ⟨n_max, h_max⟩, t_sub⟩ :=
exists_monotone_Icc_subset_open_cover_unitInterval (fun x ↦ (U_open x).preimage γ.continuous) fun t _ ↦
Set.mem_iUnion.2 ⟨γ t, mem_base _⟩
suffices ∀ n, ∃ Γ : I → E, ContinuousOn Γ (Set.Icc 0 (t n)) ∧ (Set.Icc 0 (t n)).EqOn (p ∘ Γ) γ ∧ Γ 0 = e
by
obtain ⟨Γ, cont, eqOn, Γ_0⟩ := this n_max
rw [h_max _ le_rfl] at cont eqOn
exact
⟨⟨Γ,
continuousOn_univ.mp (by convert cont; rw [eq_comm, Set.eq_univ_iff_forall]; exact fun t ↦ ⟨bot_le, le_top⟩)⟩,
funext fun _ ↦ eqOn ⟨bot_le, le_top⟩, Γ_0⟩
intro n
induction n with
| zero =>
refine ⟨fun _ ↦ e, continuous_const.continuousOn, fun t ht ↦ ?_, rfl⟩
rw [t_0, Set.Icc_self, Set.mem_singleton_iff] at ht; subst ht; exact γ_0.symm
| succ n ih => ?_
obtain ⟨Γ, cont, eqOn, Γ_0⟩ := ih
obtain ⟨x, t_sub⟩ := t_sub n
have pΓtn : p (Γ (t n)) = γ (t n) := eqOn ⟨t_0 ▸ t_mono n.zero_le, le_rfl⟩
have : Nonempty (p ⁻¹' { x }) := ⟨(H x ⟨Γ (t n), Set.mem_preimage.mpr (pΓtn ▸ t_sub ⟨le_rfl, t_mono n.le_succ⟩)⟩).2⟩
let q := (cov x).toTrivialization
refine
⟨fun s ↦ if s ≤ t n then Γ s else q.invFun (γ s, (q (Γ (t n))).2), .if (fun s hs ↦ ?_) (cont.mono fun _ h ↦ ?_) ?_,
fun s hs ↦ ?_, ?_⟩
· cases frontier_Iic_subset _ hs.2
rw [← pΓtn]
refine (q.symm_apply_mk_proj ?_).symm
rw [q.mem_source, pΓtn]
exact t_sub ⟨le_rfl, t_mono n.le_succ⟩
· rw [closure_le_eq continuous_id' continuous_const] at h; exact ⟨h.1.1, h.2⟩
· apply q.continuousOn_invFun.comp ((Continuous.prodMk_left _).comp γ.2).continuousOn
simp_rw [not_le, q.target_eq]; intro s h
exact ⟨t_sub ⟨closure_lt_subset_le continuous_const continuous_subtype_val h.2, h.1.2⟩, ⟨⟩⟩
· rw [Function.comp_apply]; split_ifs with h
exacts [eqOn ⟨hs.1, h⟩, q.proj_symm_apply' (t_sub ⟨le_of_not_ge h, hs.2⟩)]
· dsimp only; rwa [if_pos (t_0 ▸ t_mono n.zero_le)]
