Theorems · Theorem · algebraic topology

IsLocalHomeomorph.monodromy_theorem

∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X},
  IsLocalHomeomorph p →
    IsSeparatedMap p →
      ∀ {γ₀ γ₁ : C(↑unitInterval, X)} (γ : γ₀.HomotopyRel γ₁ {0, 1}) (Γ : ↑unitInterval → C(↑unitInterval, E)),
        (∀ (t s : ↑unitInterval), p ((Γ t) s) = γ (t, s)) →
          (∀ (t : ↑unitInterval), (Γ t) 0 = (Γ 0) 0) → ∀ (t : ↑unitInterval), (Γ t) 1 = (Γ 0) 1

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.

Defined in

Mathlib.Topology.Homotopy.Lifting

Cited by

0 results in Mathlib

Foundations

Depth 123 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpace