Finite sheet count of the Schwarz--Christoffel primitive

When the Schwarz--Christoffel primitive has an integrable boundary at every finite prevertex and at infinity, its restriction over the complement of the compactified boundary path is a proper local homeomorphism. Its fibers there are compact and discrete, hence finite. The covering-space monodromy then identifies the fibers over points joined by a path in that complement. In particular the number of preimages is constant on each path component.

For a simple polygonal boundary, the image of the primitive is one such component. Its finite sheet count is the degree that a subsequent univalence argument must show equals one.

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: a simple boundary yields one positive finite sheet count throughout the image component.

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) (hinfty : ∑ i : ι, e i < -1) {w : ℂ} (hw : w ∉ Set.range (schwarzChristoffelCompactifiedBoundary a e z₀)) : ((fun (τ : UpperHalfPlane) => schwarzChristoffelPrimitive a e z₀ ↑τ) ⁻¹' {w}).Finite

A fiber of the Schwarz--Christoffel primitive over a point outside its compactified boundary path is finite.

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) (hinfty : ∑ i : ι, e i < -1) {w₁ w₂ : ℂ} (hjoined : JoinedIn (Set.range (schwarzChristoffelCompactifiedBoundary a e z₀))ᶜ w₁ w₂) : ((fun (τ : UpperHalfPlane) => schwarzChristoffelPrimitive a e z₀ ↑τ) ⁻¹' {w₁}).ncard = ((fun (τ : UpperHalfPlane) => schwarzChristoffelPrimitive a e z₀ ↑τ) ⁻¹' {w₂}).ncard

The number of preimages of the Schwarz--Christoffel primitive is constant along paths avoiding its compactified boundary. Both fibers are finite, so this is an equality of ordinary natural-number counts.

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) (hinfty : ∑ i : ι, e i < -1) (hinj : Function.Injective (schwarzChristoffelCompactifiedBoundary a e z₀)) : ∃ (d : ℕ), 0 < d ∧ ∀ w ∈ schwarzChristoffelPrimitive a e z₀ '' UpperHalfPlane.upperHalfPlaneSet, ((fun (τ : UpperHalfPlane) => schwarzChristoffelPrimitive a e z₀ ↑τ) ⁻¹' {w}).ncard = d

If the compactified Schwarz--Christoffel boundary is simple, the primitive has a positive, finite, constant number of preimages at every point of its image.