Conformal equivalence of simply connected domains

The Riemann mapping theorem says that a simply connected open proper subset of ℂ is biholomorphic to the open unit disc. Because the disc is a single fixed model, this immediately classifies such domains up to biholomorphism: any two of them are biholomorphic to each other, and a single one is biholomorphic to itself in enough ways to move any prescribed point to any other. This file proves those two statements, and the sharpness of the properness hypothesis.

Main statements

• TauCeti.exists_bijOn_differentiableOn_invFunOn_of_isSimplyConnected — any two simply connected open proper subsets of ℂ are biholomorphic: there is a holomorphic bijection from one onto the other whose inverse is again holomorphic.
• TauCeti.exists_openPartialHomeomorph_of_isSimplyConnected — the same equivalence packaged as an OpenPartialHomeomorph ℂ ℂ conformal in both directions.
• TauCeti.nonempty_homeomorph_of_isSimplyConnected — any two simply connected open subsets of ℂ are homeomorphic as subtypes. Merely topologically, properness is not needed: the plane too is homeomorphic to the disc.
• TauCeti.exists_bijOn_self_apply_eq_of_isSimplyConnected — homogeneity: the biholomorphic self-maps of a simply connected open Ω ⊆ ℂ act transitively on Ω.
• Differentiable.exists_const_forall_eq_of_isSimplyConnected, TauCeti.not_injOn_univ_of_isSimplyConnected and TauCeti.not_bijOn_univ_of_isSimplyConnected — an entire function with values in a simply connected open proper set is constant, hence not injective, so ℂ itself is biholomorphic to no such set. This is why Ω ≠ Set.univ cannot be dropped from the biholomorphic equivalence statements above. Homogeneity needs no properness hypothesis either: Ω = Set.univ is homogeneous too, because the translations already act transitively on ℂ.

Proof outline

Everything runs through the Riemann map. Transporting a domain Ω to the disc and a second domain Ω' back off it composes to a biholomorphism Ω ≃ Ω'; the inverse of a holomorphic injection on an open set is holomorphic by DifferentiableOn.invFunOn, so the composite inverse needs no separate argument. Homogeneity inserts, between the two transports of one and the same domain, a disc automorphism carrying one image point to the other; that automorphism is supplied by the transitivity of TauCeti.unitDiscAut and read back as a scalar map. The whole plane, which has no Riemann map, is handled separately in the two statements that admit it: by a translation for homogeneity, and by Homeomorph.unitBall for the merely topological equivalence. Sharpness is Liouville's theorem: composing an entire map into Ω with the Riemann map of Ω gives a bounded entire function.

Scope

The maps produced here are not canonical and are not asserted to be unique: the equivalences of a simply connected domain with the disc form a torsor under Aut(𝔻), as recorded in the sibling Uniqueness.lean and Normalization.lean. Nothing here normalizes a choice.

Coordination with upstream Mathlib

The Riemann mapping theorem is being formalized upstream at mathlib4#33505, which proves the L0–L3 prerequisites internally as private lemmas. These corollaries rest on the L3 shim in RiemannMapping/Existence.lean and are themselves an explicitly temporary shim: once the human-curated Mathlib theorem lands, they should be re-proved on top of it and their downstream consumers refactored accordingly.

References

• L. Ahlfors, Complex Analysis, Ch. 6 §1.
• J. B. Conway, Functions of One Complex Variable I, Ch. VII §4.

theorem TauCeti.exists_bijOn_differentiableOn_invFunOn_of_isSimplyConnected {Ω Ω' : Set ℂ} (hΩo : IsOpen Ω) (hΩc : IsSimplyConnected Ω) (hΩ : Ω ≠ Set.univ) (hΩ'o : IsOpen Ω') (hΩ'c : IsSimplyConnected Ω') (hΩ' : Ω' ≠ Set.univ) : ∃ (f : ℂ → ℂ), Set.BijOn f Ω Ω' ∧ DifferentiableOn ℂ f Ω ∧ DifferentiableOn ℂ (Function.invFunOn f Ω) Ω' ∧ Set.LeftInvOn (Function.invFunOn f Ω) f Ω ∧ Set.RightInvOn (Function.invFunOn f Ω) f Ω'

Any two simply connected proper domains of ℂ are conformally equivalent. If Ω and Ω' are simply connected open proper subsets of ℂ, then some holomorphic f maps Ω bijectively onto Ω', and its inverse Function.invFunOn f Ω is holomorphic on Ω'.

Neither domain is required to be bounded, and no normalization is imposed: the map is one of a whole Aut(𝔻)-torsor of such maps. Together with TauCeti.not_bijOn_univ_of_isSimplyConnected this is a complete classification of the simply connected domains of ℂ up to biholomorphism: there are exactly two classes, ℂ and everything else.

theorem TauCeti.exists_openPartialHomeomorph_of_isSimplyConnected {Ω Ω' : Set ℂ} (hΩo : IsOpen Ω) (hΩc : IsSimplyConnected Ω) (hΩ : Ω ≠ Set.univ) (hΩ'o : IsOpen Ω') (hΩ'c : IsSimplyConnected Ω') (hΩ' : Ω' ≠ Set.univ) : ∃ (e : OpenPartialHomeomorph ℂ ℂ), e.source = Ω ∧ e.target = Ω' ∧ DifferentiableOn ℂ (↑e) Ω ∧ DifferentiableOn ℂ (↑e.symm) Ω' ∧ (∀ z ∈ Ω, ConformalAt (↑e) z) ∧ ∀ w ∈ Ω', ConformalAt (↑e.symm) w

Conformal equivalence of simply connected proper domains, packaged. A biholomorphism of Ω onto Ω' as an OpenPartialHomeomorph ℂ ℂ whose source is Ω and whose target is Ω', holomorphic and conformal in both directions. It is the Riemann map of Ω followed by the inverse of the Riemann map of Ω', both taken from TauCeti.riemannMapping_openPartialHomeomorph.

This is the packaged-equivalence companion the generality bar of TauCetiRoadmap/ConformalMapping/README.md asks for, in the same form as TauCeti.riemannMapping_openPartialHomeomorph for the disc.

theorem TauCeti.nonempty_homeomorph_of_isSimplyConnected {Ω Ω' : Set ℂ} (hΩo : IsOpen Ω) (hΩc : IsSimplyConnected Ω) (hΩ'o : IsOpen Ω') (hΩ'c : IsSimplyConnected Ω') : Nonempty (↑Ω ≃ₜ ↑Ω')

Any two simply connected domains of ℂ are homeomorphic, as subtypes.

Unlike the biholomorphism statements above this needs no properness hypothesis: the plane is not biholomorphic to the disc, but it is homeomorphic to it.

theorem TauCeti.exists_bijOn_self_apply_eq_of_isSimplyConnected {Ω : Set ℂ} (hΩo : IsOpen Ω) (hΩc : IsSimplyConnected Ω) {z₀ z₁ : ℂ} (hz₀ : z₀ ∈ Ω) (hz₁ : z₁ ∈ Ω) : ∃ (f : ℂ → ℂ), Set.BijOn f Ω Ω ∧ DifferentiableOn ℂ f Ω ∧ DifferentiableOn ℂ (Function.invFunOn f Ω) Ω ∧ f z₀ = z₁

A simply connected domain is homogeneous. The biholomorphic self-maps of a simply connected open Ω ⊆ ℂ act transitively on Ω: given z₀, z₁ ∈ Ω there is a holomorphic bijection of Ω onto itself, with holomorphic inverse, carrying z₀ to z₁.

Unlike the equivalence statements above, this needs no properness hypothesis: for Ω = Set.univ the translation z ↦ z + (z₁ - z₀) already does the job. Otherwise transitivity is inherited from the disc, where TauCeti.unitDiscAut already acts transitively, and the Riemann map transports the action. It fails badly without simple connectivity — the punctured disc, for instance, is not homogeneous.

theorem Differentiable.exists_const_forall_eq_of_isSimplyConnected {Ω : Set ℂ} {f : ℂ → ℂ} (hf : Differentiable ℂ f) (hΩo : IsOpen Ω) (hΩc : IsSimplyConnected Ω) (hΩ : Ω ≠ Set.univ) (hmaps : ∀ (z : ℂ), f z ∈ Ω) : ∃ (c : ℂ), ∀ (z : ℂ), f z = c

An entire function with values in a simply connected proper domain is constant. Composing with the Riemann map of Ω turns such a function into a bounded entire function, which Liouville's theorem forces to be constant; the Riemann map is injective, so the original function is constant too.

For bounded Ω this is Liouville's theorem itself, but the statement covers unbounded Ω such as the slit plane, where the Riemann map is doing genuine work.

theorem TauCeti.not_injOn_univ_of_isSimplyConnected {Ω : Set ℂ} {f : ℂ → ℂ} (hf : Differentiable ℂ f) (hΩo : IsOpen Ω) (hΩc : IsSimplyConnected Ω) (hΩ : Ω ≠ Set.univ) (hmaps : Set.MapsTo f Set.univ Ω) : ¬Set.InjOn f Set.univ

No injective entire function takes its values in a simply connected proper domain. Such a function is constant by Differentiable.exists_const_forall_eq_of_isSimplyConnected, and a constant map on ℂ is not injective.

Only the values of f are constrained, not the image: f is not required to cover Ω.

theorem TauCeti.not_bijOn_univ_of_isSimplyConnected {Ω : Set ℂ} {f : ℂ → ℂ} (hf : Differentiable ℂ f) (hΩo : IsOpen Ω) (hΩc : IsSimplyConnected Ω) (hΩ : Ω ≠ Set.univ) : ¬Set.BijOn f Set.univ Ω

ℂ is conformally equivalent to no simply connected proper domain. No entire function maps ℂ bijectively onto a simply connected open proper subset of ℂ: it is already barred from being injective there by TauCeti.not_injOn_univ_of_isSimplyConnected.

So the properness hypothesis in TauCeti.exists_bijOn_differentiableOn_invFunOn_of_isSimplyConnected cannot be dropped: ℂ is a simply connected domain lying in a biholomorphism class of its own.