Single-sheet univalence for Schwarz--Christoffel maps with several ends

If the primitive's image avoids its finite boundary trace, one uniquely attained interior value forces global injectivity. More generally, a preconnected region containing the image and avoiding the trace is mapped onto bijectively exactly when the fiber over one of its points has cardinality one. This criterion needs neither simple connectivity of that region nor injectivity of the sphere-valued boundary, which identifies all logarithmic ends with infinity.

The criterion requires a globally singleton fiber. One can establish this near an end by combining local end geometry with exclusion of all other preimages in the upper half-plane. Boundary avoidance remains a genuine hypothesis, not a consequence of local univalence.

References

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

theorem TauCeti.injOn_schwarzChristoffelPrimitive_iff_fiber_ncard_eq_one {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 ≤ ∑ i : ι with a i = a j, e i) (havoid : Disjoint (schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet) (schwarzChristoffelFiniteBoundary a e z₀)) {w : ℂ} (hw : w ∈ schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet) : Set.InjOn (schwarzChristoffelPrimitive a e z₀) UpperHalfPlane.upperHalfPlaneSet ↔ ((fun (τ : UpperHalfPlane) => schwarzChristoffelPrimitive a e z₀ ↑τ) ⁻¹' {w}).ncard = 1

Single-sheet univalence. If the image avoids its finite boundary trace, the primitive is injective exactly when one interior value has one preimage. Any number of logarithmic ends, coincident prevertices, and an unrestricted total exponent are allowed.

theorem TauCeti.bijOn_schwarzChristoffelPrimitive_iff_fiber_ncard_eq_one {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 ≤ ∑ i : ι with a i = a j, e i) {W : Set ℂ} (hW : IsPreconnected W) (hWB : Disjoint W (schwarzChristoffelFiniteBoundary a e z₀)) (hFW : schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet ⊆ W) {w : ℂ} (hw : w ∈ W) : Set.BijOn (schwarzChristoffelPrimitive a e z₀) UpperHalfPlane.upperHalfPlaneSet W ↔ ((fun (τ : UpperHalfPlane) => schwarzChristoffelPrimitive a e z₀ ↑τ) ⁻¹' {w}).ncard = 1

A degree-one mapping criterion with several logarithmic ends. A preconnected region containing the image and avoiding the finite boundary trace is the bijective image of the upper half-plane exactly when the fiber over one specified point has cardinality one. No openness or simple-connectivity hypothesis on the region is necessary.