Bundled finite holomorphic maps of compactified Fuchsian quotients

A finite-index inclusion of discrete projective subgroups induces a finite holomorphic map of compactified quotients. This file bundles the canonical quotient map for the generic degree, divisor, and ramification APIs. Its forward function and composition law agree with the existing unbundled maps. No compactness hypothesis is needed for the bundle; composition uses the compact source hypothesis of the generic finite holomorphic map API.

The local elliptic model used to prove nonconstancy follows Farkas--Kra, Riemann Surfaces, Chapter I, §§4--5.

noncomputable def TauCeti.Fuchsian.compactifiedQuotientFiniteHolomorphicMap {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] (h : Δ ≤ Γ) [Δ.IsFiniteRelIndex Γ] : RiemannSurface.FiniteHolomorphicMap Δ.CompactifiedQuotient Γ.CompactifiedQuotient

The finite holomorphic map of compactified quotients induced by a finite-index inclusion. Its forward function is the ordinary map on interior orbits and cusp orbits. No compactness hypothesis is needed to construct it.

Equations

• TauCeti.Fuchsian.compactifiedQuotientFiniteHolomorphicMap h = { toFun := Subgroup.compactifiedQuotientMap h, holomorphic := ⋯, nonconstant := ⋯, finite_fiber := ⋯ }

@[simp]

theorem TauCeti.Fuchsian.coe_compactifiedQuotientFiniteHolomorphicMap {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] (h : Δ ≤ Γ) [Δ.IsFiniteRelIndex Γ] : ↑(compactifiedQuotientFiniteHolomorphicMap h) = Subgroup.compactifiedQuotientMap h

The bundled map has exactly the canonical compactified quotient map as its forward function.

@[simp]

theorem TauCeti.Fuchsian.compactifiedQuotientFiniteHolomorphicMap_comp {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] (h : Δ ≤ Γ) [Δ.IsFiniteRelIndex Γ] [hcompact : CompactSpace Δ.CompactifiedQuotient] {Θ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Θ] (k : Γ ≤ Θ) [Γ.IsFiniteRelIndex Θ] : (compactifiedQuotientFiniteHolomorphicMap k).comp (compactifiedQuotientFiniteHolomorphicMap h) = compactifiedQuotientFiniteHolomorphicMap ⋯

Bundled finite holomorphic maps compose along subgroup towers, so generic divisor functoriality and ramification chain rules apply to the canonical quotient maps.