The monodromy theorem #
Analytic continuation along a path is unique (Continuation/Basic.lean), but the germ it
delivers at the far end may depend on the path. The monodromy theorem says that it only
depends on the path up to homotopy: if a germ continues along every path of a homotopy rel
endpoints, all those continuations end at the same germ.
The theorem is proved here in the form that does not hold the endpoints fixed. A homotopy of
paths whose endpoints move carries the initial germs along the path t ↦ h (t, 0) swept out by
the starting point, and what TauCeti.monodromy_theorem_of_free_homotopy asserts is that the
terminal germs are then carried along the path t ↦ h (t, 1) swept out by the finishing point:
the conclusion is again a continuation, not an equality of germs. Fixing the endpoints degenerates
both edges to constant paths, where "continues along a constant path" means "is one germ", and
recovers the classical statement TauCeti.monodromy_theorem. The extra generality is not
decorative — it is what makes monodromy an invariant of the free homotopy class of a loop
(TauCeti.monodromy_theorem_of_free_homotopy_loop), a statement about a homotopy that moves the
base point and so out of reach of the rel-endpoints form.
The engine: stability under uniform perturbation of the path #
Homotopy invariance is a consequence of a purely metric statement, proved here first and useful
on its own: a continuation over a compact parameter set is stable under small uniform
perturbations of the path. Concretely, IsAnalyticContinuationAlong.exists_representatives
turns the germs carried by a continuation into honest analytic functions on discs of one common
radius ρ > 0, matched on overlaps; the very same family of functions is then a continuation
along any path staying within ρ of the original
(IsAnalyticContinuationAlong.exists_isAnalyticContinuationAlong_of_dist_lt), so by uniqueness a
continuation along a nearby path that meets it at one parameter time meets it at all of them
(IsAnalyticContinuationAlong.exists_forall_eventuallyEq_of_dist_lt).
That comparison is made against the representative family F, not against f itself, and the
distinction is what the moving endpoints cost: the germ of the perturbed continuation lives at
γ' a, a point at which f a need not even be analytic, whereas F a is analytic on a whole
disc of radius ρ about γ a. When the perturbation fixes the endpoints the representative can
be traded back for f, and that is the classical statement
IsAnalyticContinuationAlong.exists_eventuallyEq_of_dist_lt.
The passage from germs to a uniform radius is where compactness of the parameter set enters: for
each parameter time one picks a disc on which the carried germ has an analytic representative and
a parameter neighbourhood on which the germ is constant, and a finite subcover turns the
resulting radii into a single positive ρ. Two representatives are then compared on the
intersection of their two discs, which is convex, hence preconnected, so the identity principle
(AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq) upgrades germ agreement at one point to
equality on the whole overlap.
Monodromy #
With the engine in place, TauCeti.monodromy_theorem_of_free_homotopy is the statement that the
terminal germs form a continuation along the terminal edge. Its three clauses are read off in
turn: continuity of that edge and analyticity of each terminal germ are immediate, and the
remaining clause — nearby parameters carry the same terminal germ — is the engine applied to the
row at t₀. Rows h (t, ·) and h (t₀, ·) are uniformly close for t near t₀ because h is
uniformly continuous on the compact square, and the two rows meet at the initial parameter because
hstart is a continuation. The one point needing care is that the engine compares germs at the
moved endpoints h (t, 0) and h (t, 1), while the representative family is matched to f t₀
only at h (t₀, 0) and h (t₀, 1). Transporting that match is what
TauCeti.eventually_eventuallyEq_iff_of_analyticAt is for: two analytic functions with a common
germ at a point have a common germ at every point near it, so the match survives the move.
TauCeti.monodromy_theorem_of_homotopy_refl records the loop form of the rel-endpoints statement:
continuing a germ around a null-homotopic loop returns the germ one started with, since the
continuation along the constant loop is constant.
Main results #
TauCeti.IsAnalyticContinuationAlong.exists_representatives— uniform disc representatives for a continuation over a compact parameter set.TauCeti.IsAnalyticContinuationAlong.exists_isAnalyticContinuationAlong_of_dist_lt— those representatives continue along every uniformly nearby path.TauCeti.IsAnalyticContinuationAlong.exists_forall_eventuallyEq_of_dist_lt— stability with moving endpoints: a continuation along a nearby path that matches the representative family at one parameter time matches it at every parameter time.TauCeti.IsAnalyticContinuationAlong.exists_eventuallyEq_of_dist_lt— stability: a continuation along a nearby path with the same endpoints and the same initial germ has the same terminal germ.TauCeti.monodromy_theorem_of_free_homotopy— the monodromy theorem for a free homotopy: germs continued across a homotopy whose endpoints move form a continuation along the path the far endpoint sweeps out.TauCeti.monodromy_theorem— the monodromy theorem: continuations along the paths of a homotopy rel endpoints, all starting from one germ, all end at one germ.TauCeti.monodromy_theorem_of_free_homotopy_loop— the monodromy of a loop is unchanged by a free homotopy through loops, base point included.TauCeti.monodromy_theorem_of_homotopy_refl— a germ continued around a null-homotopic loop comes back to itself.
Generality #
The germs carried are germs of maps ℂ → E into a complex Banach space, as in
Continuation/Basic.lean, where the choice is discussed; the conformal-mapping consumers of the
monodromy theorem instantiate E = ℂ. Nothing in the stability engine sees the target: the disc
representatives come from AnalyticAt.exists_ball_analyticOnNhd and are compared by the identity
principle, both of which Mathlib states for maps into an arbitrary Banach space.
Relation to Mathlib #
Mathlib's IsLocalHomeomorph.monodromy_theorem (Mathlib/Topology/Homotopy/Lifting.lean) is an
abstract monodromy statement about lifts through a separated local homeomorphism, and its
docstring names analytic continuation as the intended application. The route taken here is
independent of it: it reuses what this area already has — germ-level uniqueness of continuation
along a fixed path (IsAnalyticContinuationAlong.eventuallyEq) — and adds only the metric
stability engine, which is the concrete content that the abstract theorem's separatedness
hypothesis packages. The other route is now available too:
TauCeti/Analysis/Complex/HolomorphicSheaf.lean builds the étale space of holomorphic germs and
proves its projection to be a separated local homeomorphism, and
Mathlib's abstract theorem applies directly to that projection. That route does not subsume this
file:
TauCeti.monodromy_theorem_of_free_homotopy moves the endpoints and concludes with a
continuation along the path they sweep out, whereas the abstract theorem is rel endpoints and
concludes with an equality of two lifted points.
References #
- L. Ahlfors, Complex Analysis, Ch. 8 §1.
- J. B. Conway, Functions of One Complex Variable I (GTM 11), Ch. IX §3.
- W. Rudin, Real and Complex Analysis, Ch. 16.
Uniform disc representatives #
Uniform disc representatives for a continuation over a compact parameter set. The germs
carried by a continuation can be represented by honest functions F t, each analytic on a disc
about γ t of one radius ρ > 0 independent of t, in such a way that nearby parameter times
carry representatives that agree on the whole disc — not merely near γ t.
The uniform radius is what makes the family usable along a perturbed path: the defining
condition of a continuation controls f t only near γ t, so f t itself carries no
information at a nearby point γ' t.
Stability under uniform perturbation of the path #
One family of germs continues along every nearby path. For a continuation over a compact
parameter set there are a radius ρ > 0 and a family F carrying the same germs as f such
that F is an analytic continuation along any path that stays within ρ of γ.
Note the order of the quantifiers: the family F is produced once and for all, before the
perturbed path is given.
Stability of the carried germ under uniform perturbation of the path, measured against a
fixed comparison family. For a continuation f along γ over a compact preconnected parameter
set there are a radius ρ > 0 and a family F carrying the same germs as f such that any
continuation g along a path γ' staying within ρ of γ and agreeing with F at one
parameter time agrees with F at every parameter time.
No relation between the endpoints of γ' and those of γ is required, which is what makes this
the form a homotopy with moving endpoints consumes. The price is that the comparison has to be
made against F rather than against f: the germ of g a lives at γ' a, where f a need not
even be analytic, while F a is analytic on a whole disc of radius ρ about γ a. When the
endpoints do not move, TauCeti.IsAnalyticContinuationAlong.exists_eventuallyEq_of_dist_lt
eliminates F again.
Stability of the terminal germ under uniform perturbation of the path. For a continuation
f along γ over a compact preconnected parameter set there is a radius ρ > 0 with the
following property: any continuation g along a path γ' that stays within ρ of γ, shares
the endpoints γ' a = γ a and γ' b = γ b of γ, and starts from the same germ as f, also
ends at the same germ as f.
This is the metric heart of the monodromy theorem for a homotopy rel endpoints: nearby paths with
common endpoints continue a germ to the same place. It is the fixed-endpoint specialization of
TauCeti.IsAnalyticContinuationAlong.exists_forall_eventuallyEq_of_dist_lt, the endpoint
equalities being exactly what lets the comparison family be traded back for f.
The monodromy theorem #
The monodromy theorem for a free homotopy of paths. Let h be a continuous map of the
square, read as a family of paths h (t, ·) whose endpoints are allowed to move, and suppose a
family of germs continues along each of those paths. If the initial germs — the germ of f t 0 at
h (t, 0) — themselves continue along the initial edge t ↦ h (t, 0), then the terminal germs
continue along the terminal edge t ↦ h (t, 1).
This is the monodromy theorem in the form the deck-group and covering-space consumers need: the
continuation of a germ across a homotopy is itself a continuation, along the path the far endpoint
sweeps out. Nothing is assumed rel endpoints; TauCeti.monodromy_theorem is the special case in
which both edges are constant, where "continues along a constant path" degenerates to "carries one
germ throughout".
The monodromy theorem. Let h be a homotopy rel endpoints between two paths from z₀ to
z₁ in ℂ, and suppose a germ at z₀ continues along every path h (t, ·) of the homotopy,
all the continuations starting from that one germ. Then they all end at one and the same germ at
z₁: the result of the continuation depends on the path only through its homotopy class.
This is the rel-endpoints case of TauCeti.monodromy_theorem_of_free_homotopy, whose homotopy is
allowed to move the endpoints and whose conclusion is correspondingly a continuation along the
path the terminal point sweeps out rather than a single germ at z₁.
The monodromy of a loop depends only on its free homotopy class. If h is a homotopy
through loops — each row h (t, ·) closes up, h (t, 1) = h (t, 0) — and the initial germs
continue along the path t ↦ h (t, 0) swept out by the base point, then the germ is preserved by
continuation around every loop of the homotopy as soon as it is preserved around one of them.
This is the statement that makes monodromy an invariant of the free homotopy class of a loop, and
it is out of reach of TauCeti.monodromy_theorem, whose homotopies must fix the base point.
A germ continued around a null-homotopic loop returns to itself. If the loop p at z₀
is homotopic rel endpoints to the constant loop and a germ at z₀ continues along every path of
the homotopy, then continuing it along p gives the germ back.
Together with the uniqueness of continuation along a fixed path, this is the reason a germ that can be analytically continued along every path of a simply connected domain is single-valued there: no loop in such a domain can create a new branch.