Domains with holomorphic square roots

A set U ⊆ ℂ has holomorphic square roots (TauCeti.HasHolomorphicSquareRoots U) if every function holomorphic and nowhere zero on U is the square of a function holomorphic on U.

Beyond connectedness, this is the only consequence of simple connectivity that the proof of the Riemann mapping theorem uses: the Koebe square-root trick takes a square root of z - a to inject a proper domain into the disc, and a square root of a disc automorphism to beat a map that is not onto. Isolating it as a hypothesis lets that proof run on every domain with the property, and so shows that a connected open proper subset of ℂ with the property is conformally a disc. Since ℂ itself is convex, every connected open set with the property is therefore simply connected (TauCeti.HasHolomorphicSquareRoots.isSimplyConnected, in Conformal/RiemannMapping/Existence.lean), and for an open connected set the two conditions are equivalent. In Rudin's list of characterisations of simply connected plane domains, this file gives (b) ⇒ (i) (IsSimplyConnected.hasHolomorphicSquareRoots); the converse (i) ⇒ (b) is TauCeti.HasHolomorphicSquareRoots.isSimplyConnected. A property that is easier to verify from the geometry of the complement — for example vanishing of the winding numbers of cycles in U about points outside U, via the homology form of Cauchy's theorem — thereby becomes a proof of simple connectivity.

Main definitions

• TauCeti.HasHolomorphicSquareRoots — nowhere-zero holomorphic functions have holomorphic square roots.

Main results

• IsSimplyConnected.hasHolomorphicSquareRoots — a simply connected open set has holomorphic square roots.
• TauCeti.HasHolomorphicSquareRoots.image — the property is carried along a holomorphic map injective on an open set.

References

• W. Rudin, Real and Complex Analysis, 3rd ed., Theorem 13.11.

structure TauCeti.HasHolomorphicSquareRoots (U : Set ℂ) : Prop

A set U ⊆ ℂ has holomorphic square roots if every function holomorphic and nowhere zero on U is, on U, the square of a function holomorphic on U. It is introduced by the anonymous constructor and eliminated by TauCeti.HasHolomorphicSquareRoots.exists_differentiableOn_sq_eq.

• exists_differentiableOn_sq_eq ⦃g : ℂ → ℂ⦄ : DifferentiableOn ℂ g U → 0 ∉ g '' U → ∃ (f : ℂ → ℂ), DifferentiableOn ℂ f U ∧ Set.EqOn (fun (z : ℂ) => f z ^ 2) g U

  A function holomorphic and nowhere zero on U is, on U, the square of a function holomorphic on U.

theorem IsSimplyConnected.hasHolomorphicSquareRoots {U : Set ℂ} (hUc : IsSimplyConnected U) (hUo : IsOpen U) : TauCeti.HasHolomorphicSquareRoots U

A simply connected open set has holomorphic square roots. This is the case n = 2 of TauCeti.exists_differentiableOn_pow_eq.

theorem TauCeti.HasHolomorphicSquareRoots.image {U : Set ℂ} (hU : HasHolomorphicSquareRoots U) (hUo : IsOpen U) {φ : ℂ → ℂ} (hφ : DifferentiableOn ℂ φ U) (hφi : Set.InjOn φ U) : HasHolomorphicSquareRoots (φ '' U)

Holomorphic square roots are carried along injective holomorphic maps. If U is open and has holomorphic square roots, and φ is holomorphic and injective on U, then φ '' U has holomorphic square roots: a root of g ∘ φ on U, composed with the holomorphic inverse Function.invFunOn φ U, is a root of g on φ '' U.