The Schwarz--Christoffel primitive as a covering map

Let F = schwarzChristoffelPrimitive a e z₀ and let P be the range of the compactified boundary path schwarzChristoffelCompactifiedBoundary a e z₀. Assume, as in TauCeti.Analysis.Complex.Conformal.SchwarzChristoffel.Image, that every finite prevertex is integrable and that the total exponent is less than -1.

The primitive has nonvanishing derivative, so on the upper half-plane it is a local homeomorphism. It is also proper over the complement of P (isCompact_upperHalfPlaneSet_inter_preimage_schwarzChristoffelPrimitive). A proper local homeomorphism is a covering map, so F, viewed on ℍ, is a covering map over the complement of P.

This is the topological core of the argument that the Schwarz--Christoffel map is univalent. If a simply connected set W avoids P and contains the image of the upper half-plane, then the upper half-plane is a path-connected covering space of W. Such a covering is trivial, so F is injective, and by connectedness its image is all of W. For a convex polygon, the interior of the polygon is a natural choice of W. To use it, one must know that the image lies inside the polygon and does not meet its sides.

Main results

• TauCeti.isLocalHomeomorphOn_schwarzChristoffelPrimitive -- the primitive is a local homeomorphism on the upper half-plane.
• TauCeti.isCoveringMapOn_schwarzChristoffelPrimitive_of_isCompact_preimage -- on ℍ, the primitive is a covering map over every open set where it is proper.
• TauCeti.isCoveringMapOn_schwarzChristoffelPrimitive -- on ℍ, the primitive is a covering map over the complement of the compactified boundary path.
• TauCeti.bijOn_schwarzChristoffelPrimitive_of_subset -- the primitive maps the upper half-plane bijectively onto every simply connected set that avoids the boundary path and contains the image.

References

• L. Ahlfors, Complex Analysis, Ch. 6, Section 2.
• T. Driscoll and L. Trefethen, Schwarz--Christoffel Mapping, Ch. 2.
• O. Forster, Lectures on Riemann Surfaces, Section 4.

theorem TauCeti.isLocalHomeomorphOn_schwarzChristoffelPrimitive {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) : IsLocalHomeomorphOn (schwarzChristoffelPrimitive a e z₀) UpperHalfPlane.upperHalfPlaneSet

The Schwarz--Christoffel primitive is a local homeomorphism on the upper half-plane. Its derivative is nonzero throughout this domain.

theorem TauCeti.isCoveringMapOn_schwarzChristoffelPrimitive_of_isCompact_preimage {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) {U : Set ℂ} (hU : IsOpen U) (hK : ∀ K ⊆ U, IsCompact K → IsCompact (UpperHalfPlane.upperHalfPlaneSet ∩ schwarzChristoffelPrimitive a e z₀ ⁻¹' K)) : IsCoveringMapOn (fun (τ : UpperHalfPlane) => schwarzChristoffelPrimitive a e z₀ ↑τ) U

The Schwarz--Christoffel primitive is a covering map over an open set where it is proper. Viewed as a map on ℍ, the primitive is a covering map over every open set U such that the points of the upper half-plane sent into any compact subset of U form a compact set. No assumption on the exponents is needed: the primitive is always a local homeomorphism.

theorem TauCeti.isCoveringMapOn_schwarzChristoffelPrimitive {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 < ∑ i : ι with a i = a j, e i) (hinfty : ∑ i : ι, e i < -1) : IsCoveringMapOn (fun (τ : UpperHalfPlane) => schwarzChristoffelPrimitive a e z₀ ↑τ) (Set.range (schwarzChristoffelCompactifiedBoundary a e z₀))ᶜ

The Schwarz--Christoffel primitive is a covering map off its boundary path. Viewed as a map on ℍ, the primitive is a covering map over the complement of the compactified boundary path, provided every finite prevertex is integrable and the total exponent is less than -1.

theorem TauCeti.bijOn_schwarzChristoffelPrimitive_of_subset {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 < ∑ i : ι with a i = a j, e i) (hinfty : ∑ i : ι, e i < -1) {W : Set ℂ} [SimplyConnectedSpace ↑W] (hWP : Disjoint W (Set.range (schwarzChristoffelCompactifiedBoundary a e z₀))) (hFW : schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet ⊆ W) : Set.BijOn (schwarzChristoffelPrimitive a e z₀) UpperHalfPlane.upperHalfPlaneSet W

The Schwarz--Christoffel primitive is a bijection onto a simply connected region avoiding its boundary path. If the image of the upper half-plane lies in a simply connected set W disjoint from the compactified boundary path, then the primitive maps the upper half-plane bijectively onto W.