Holomorphy of a compactified quotient map

An inclusion of discrete Fuchsian groups induces a map of compactified quotients. Read in the elliptic charts of the coarse quotients it is a power map with exponent the elliptic ramification index, and read in the cusp charts at an adjoined cusp it is a power map with exponent the cusp width index; in both cases it is holomorphic. This file assembles those local descriptions into holomorphy of the map on the whole compactified quotient.

The cusp-coordinate and width conventions follow Diamond and Shurman, A First Course in Modular Forms, §2.4.

theorem Subgroup.CompactifiedQuotient.mdifferentiable_compactifiedQuotientMap {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] (h : Δ ≤ Γ) : MDiff (compactifiedQuotientMap h)

The map of compactified quotients induced by an inclusion of discrete projective subgroups is holomorphic.