Finite sheet count of the Schwarz--Christoffel primitive

When every finite prevertex has total exponent at least -1, the restriction of the Schwarz--Christoffel primitive over the complement of its finite boundary trace is a proper local homeomorphism. Its fibers there are compact and discrete, hence finite. Covering-space monodromy identifies the fibers over points joined by a path in that complement, so the number of preimages is constant on each path component. Any number of logarithmic ends is allowed, and the total exponent is unrestricted.

If the image avoids the finite boundary trace, it has one positive finite sheet count throughout. Showing this count equals one establishes global univalence.

Main results

• TauCeti.finite_schwarzChristoffelPrimitive_fiber: a fiber away from the boundary is finite.
• TauCeti.ncard_schwarzChristoffelPrimitive_fiber_eq_of_joinedIn: paths in the complement preserve fiber cardinality.
• TauCeti.exists_constant_schwarzChristoffelPrimitive_fiber_ncard: boundary avoidance yields one positive finite sheet count throughout the image.

References

• L. Ahlfors, Complex Analysis, Chapter 6, Section 2.
• O. Forster, Lectures on Riemann Surfaces, Section 4.

theorem TauCeti.finite_schwarzChristoffelPrimitive_fiber {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 ≤ ∑ i : ι with a i = a j, e i) {w : ℂ} (hw : w ∉ schwarzChristoffelFiniteBoundary a e z₀) : ((fun (τ : UpperHalfPlane) => schwarzChristoffelPrimitive a e z₀ ↑τ) ⁻¹' {w}).Finite

A fiber outside the finite boundary trace is finite, including when several prevertices are logarithmic ends.

theorem TauCeti.ncard_schwarzChristoffelPrimitive_fiber_eq_of_joinedIn {ι : Type u_1} [Fintype ι] (a e : ι → ℝ) (z₀ : UpperHalfPlane) (hfinite : ∀ (j : ι), -1 ≤ ∑ i : ι with a i = a j, e i) {w₁ w₂ : ℂ} (hjoined : JoinedIn (schwarzChristoffelFiniteBoundary a e z₀)ᶜ w₁ w₂) : ((fun (τ : UpperHalfPlane) => schwarzChristoffelPrimitive a e z₀ ↑τ) ⁻¹' {w₁}).ncard = ((fun (τ : UpperHalfPlane) => schwarzChristoffelPrimitive a e z₀ ↑τ) ⁻¹' {w₂}).ncard

Paths avoiding the finite boundary trace preserve the number of preimages. Both fibers are finite, so these are ordinary natural-number counts even with several logarithmic ends.

theorem TauCeti.exists_constant_schwarzChristoffelPrimitive_fiber_ncard {ι : 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₀)) : ∃ (d : ℕ), 0 < d ∧ ∀ w ∈ schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet, ((fun (τ : UpperHalfPlane) => schwarzChristoffelPrimitive a e z₀ ↑τ) ⁻¹' {w}).ncard = d

If the image avoids the finite boundary trace, the primitive has a positive finite constant number of preimages throughout its image. No boundary simplicity is required.