The global branch of a germ on a simply connected domain

Monodromy.lean proves that analytic continuation along a path depends on the path only through its homotopy class. This file draws the conclusion that makes monodromy usable: on a simply connected domain, a germ that continues along every path is the germ of a single holomorphic function on the whole domain. Equivalently, on such a domain continuation creates no new branches, so "multi-valued analytic function" is a phenomenon of the topology of the domain and not of the germ.

The hypothesis is TauCeti.ContinuesInside f₀ U z₀ from Conformal/Continuation/Basic.lean: the germ of f₀ at z₀ continues along every path in U issuing from z₀. It is exactly what a holomorphic function on U supplies (TauCeti.ContinuesInside.of_differentiableOn), and by the two-way form below it is supplied by nothing else once U is simply connected.

Main results

• TauCeti.ContinuesInside.eventuallyEq_at_one — path independence: on a simply connected U, two continuations of one germ along two paths in U with the same endpoints end at the same germ.
• TauCeti.ContinuesInside.exists_analyticOnNhd — the monodromy theorem for a simply connected domain: a germ that continues along every path of a simply connected open U is the germ of a function analytic on all of U.
• TauCeti.continuesInside_iff_exists_analyticOnNhd — the two-way form on a simply connected open set: continuable along every path inside U ⟺ the germ of a function analytic on U.

The branch produced is unique as soon as U is preconnected, by the identity principle (AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq); no uniqueness statement is added here.

The construction

Path independence is monodromy plus simple connectivity: two paths in U with the same endpoints are joined by a homotopy whose every intermediate path is again inside U (Path.exists_homotopy_forall_mem_of_isSimplyConnected), so the hypothesis supplies a continuation along each of them and TauCeti.monodromy_theorem applies. Uniqueness of continuation along a fixed path (TauCeti.IsAnalyticContinuationAlong.eventuallyEq, over the preconnected parameter interval) then matches the two given continuations with the two extreme members of that family.

The global branch is F w = (value at w of the terminal germ of a continuation to w), chosen once per point of U by path connectedness; path independence says the choice does not matter. The work is in showing F analytic, that is, in comparing the terminal germs at two different points. The comparison uses the metric stability of continuation (TauCeti.IsAnalyticContinuationAlong.exists_isAnalyticContinuationAlong_of_dist_lt): a continuation along a path δ ending at z is carried by a family that continues along every path uniformly ρ-close to δ, so the sheared path x ↦ δ x + x • (w - z), which ends at a nearby w, is continued by that same family. The shear leaves δ by less than ρ, and by less than the distance from the compact set δ '' I to the complement of U, so it stays inside U and path independence applies to it. Hence F agrees near z with a fixed analytic representative of the terminal germ at z, which is what analyticity at z needs. The same identification at z₀, applied to the constant path, is what gives F the prescribed germ there.

Generality

The germ carried is the germ of a map ℂ → E into a complex Banach space, as in Continuation/Basic.lean, where the choice is discussed; the conformal-mapping consumers instantiate E = ℂ. The domain U is a subset of ℂ throughout: it is the topology of U that the theorem is about, and the shear that moves the endpoint of a path is a statement about paths in ℂ.

Relation to the roadmap and to Mathlib

This completes the L4 target "the monodromy theorem (continuations along homotopic paths agree)" of TauCetiRoadmap/ConformalMapping/README.md with the statement that layer is built for: the passage from local germ data to a single-valued function on a simply connected domain, which is what the reflection and continuation layers hand to their consumers. Layer L4 lies outside the roadmap's shim-deletion clause for the upstream Riemann-mapping effort (leanprover-community/mathlib4#33505), which contains no continuation or monodromy material.

Mathlib has the abstract monodromy statement IsLocalHomeomorph.monodromy_theorem and the lifting criterion IsCoveringMap.existsUnique_continuousMap_lifts for a simply connected base (Mathlib/Topology/Homotopy/Lifting.lean), but consuming them for germs of holomorphic functions require the étale space of those germs as a topological space, which Mathlib does not have; TauCeti/Analysis/Complex/HolomorphicSheaf.lean builds it and Conformal/Continuation/Etale.lean supplies the continuation/lift correspondence needed to apply the abstract theorem to it. Mathlib's simple-connectivity and path homotopy APIs are consumed rather than restated: IsSimplyConnected.isPathConnected here, and SimplyConnectedSpace.paths_homotopic with Path.Homotopy.map through Path.exists_homotopy_forall_mem_of_isSimplyConnected. So is its metric thickening of a compact set.

References

• L. Ahlfors, Complex Analysis, Ch. 8 §1.3.
• J. B. Conway, Functions of One Complex Variable I (GTM 11), Ch. IX §3.
• W. Rudin, Real and Complex Analysis, Ch. 16 (the monodromy theorem).

Path independence and the global branch

theorem TauCeti.ContinuesInside.eventuallyEq_at_one {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {U : Set ℂ} {z₀ : ℂ} {f₀ : ℂ → E} {γ δ : ↑unitInterval → ℂ} {f g : ↑unitInterval → ℂ → E} (hUc : IsSimplyConnected U) (H : ContinuesInside f₀ U z₀) (hγ : Continuous γ) (hγU : ∀ (x : ↑unitInterval), γ x ∈ U) (hγ0 : γ 0 = z₀) (hδ : Continuous δ) (hδU : ∀ (x : ↑unitInterval), δ x ∈ U) (hδ0 : δ 0 = z₀) (hend : δ 1 = γ 1) (hf : IsAnalyticContinuationAlong f γ Set.univ) (hf0 : f 0 =ᶠ[nhds z₀] f₀) (hg : IsAnalyticContinuationAlong g δ Set.univ) (hg0 : g 0 =ᶠ[nhds z₀] f₀) : f 1 =ᶠ[nhds (γ 1)] g 1

Path independence of continuation on a simply connected domain. Two continuations of one germ, along two paths in U that start at z₀ and share their endpoint, carry the same germ at the endpoint.

theorem TauCeti.ContinuesInside.exists_analyticOnNhd {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {U : Set ℂ} {z₀ : ℂ} {f₀ : ℂ → E} (hUo : IsOpen U) (hUc : IsSimplyConnected U) (hz₀ : z₀ ∈ U) (H : ContinuesInside f₀ U z₀) : ∃ (F : ℂ → E), AnalyticOnNhd ℂ F U ∧ F =ᶠ[nhds z₀] f₀

The monodromy theorem for a simply connected domain. A germ that continues along every path of a simply connected open set U issuing from z₀ is the germ at z₀ of a single function analytic on all of U.

So on a simply connected domain analytic continuation produces no new branches, and a "multi-valued analytic function" there is single-valued after all.

theorem TauCeti.continuesInside_iff_exists_analyticOnNhd {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {U : Set ℂ} {z₀ : ℂ} {f₀ : ℂ → E} (hUo : IsOpen U) (hUc : IsSimplyConnected U) (hz₀ : z₀ ∈ U) : ContinuesInside f₀ U z₀ ↔ ∃ (F : ℂ → E), AnalyticOnNhd ℂ F U ∧ F =ᶠ[nhds z₀] f₀

The monodromy theorem, in two-way form. On a simply connected open set U, a germ at a point z₀ ∈ U continues along every path in U from z₀ if and only if it is the germ of a function analytic on all of U.

The forward direction is TauCeti.ContinuesInside.exists_analyticOnNhd; the reverse is the observation that a holomorphic function is its own continuation.