English
If two paths γ0, γ1 in X are connected by a homotopy γ relative to endpoints, and a lift Γ of γ to E exists for every t with a fixed starting point e, then the endpoints Γ(t,1) are independent of t; in particular, Γ(t,1)=Γ(0,1) for all t.
Русский
Пусть две пути γ0, γ1 в X соединены гомотопией γ относительно концов; если каждый срез γ(t,·) допускает непрерывный подъем Γ_t в E через разнесённое отображение p, начинающийся в фиксированной точке, тогда концы подъёмов не зависят от t: для всех t выполняется Γ(t,1)=Γ(0,1).
LaTeX
$$$$\forall γ_0, γ_1: C(I,X), γ: γ_0.HomotopyRel γ_1\{0,1\}, \Gamma: I\to C(I,E), \forall t: I, p(\Gamma(t,·)) = γ(t,·),
\Rightarrow Γ(t,1)=Γ(0,1).$$$$
Lean4
/-- The abstract monodromy theorem: if `γ₀` and `γ₁` are two paths in a topological space `X`,
`γ` is a homotopy between them relative to the endpoints, and the path at each time step of
the homotopy, `γ (t, ·)`, lifts to a continuous path `Γ t` through a separated local
homeomorphism `p : E → X`, starting from some point in `E` independent of `t`. Then the
endpoints of these lifts are also independent of `t`.
This can be applied to continuation of analytic functions as follows: for a sheaf of analytic
functions on an analytic manifold `X`, we may consider its étale space `E` (whose points are
analytic germs) with the natural projection `p : E → X`, which is a local homeomorphism and a
separated map (because two analytic functions agreeing on a nonempty open set agree on the
whole connected component). An analytic continuation of a germ along a path `γ (t, ·) : C(I, X)`
corresponds to a continuous lift of `γ (t, ·)` to `E` starting from that germ. If `γ` is a
homotopy and the germ admits continuation along every path `γ (t, ·)`, then the result of the
continuations are independent of `t`. In particular, if `X` is simply connected and an analytic
germ at `p : X` admits a continuation along every path in `X` from `p` to `q : X`, then the
continuation to `q` is independent of the path chosen. -/
theorem monodromy_theorem {γ₀ γ₁ : C(I, X)} (γ : γ₀.HomotopyRel γ₁ {0, 1}) (Γ : I → C(I, E))
(Γ_lifts : ∀ t s, p (Γ t s) = γ (t, s)) (Γ_0 : ∀ t, Γ t 0 = Γ 0 0) (t : I) : Γ t 1 = Γ 0 1 :=
by
have := homeo.continuous_lift sep (.comp γ .prodSwap) (g := fun st ↦ Γ st.2 st.1) ?_ ?_ ?_
· apply sep.const_of_comp homeo.isLocallyInjective (this.comp (.prodMk_right 1))
intro t t'; change p (Γ _ _) = p (Γ _ _); simp_rw [Γ_lifts, γ.eq_fst _ (.inr rfl)]
· ext; apply Γ_lifts
· simp_rw [Γ_0]; exact continuous_const
· exact fun t ↦ (Γ t).2
