The local form of a compactified quotient map at a cusp #
For an inclusion of discrete Fuchsian groups, use cusp data with the same representative and
scaling. The larger group's cusp chart composed with the compactified quotient map is the
n-th power of the smaller group's cusp chart, where n is the ratio of their widths.
Thus the cusp-width ratio is the local ramification exponent of the map.
The coordinate convention follows Diamond and Shurman, A First Course in Modular Forms, §2.4.
theorem
Subgroup.CompactifiedQuotient.cuspChart_compactifiedQuotientMap_eq_pow
{Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)}
[DiscreteTopology ↥Δ]
[DiscreteTopology ↥Γ]
(h : Δ ≤ Γ)
(D : Δ.CuspDatum)
(E : Γ.CuspDatum)
(hc : D.cusp = E.cusp)
(hσ : D.scaling = E.scaling)
{n : ℕ}
(hw : D.width = ↑n * E.width)
{A : ℝ}
(hD : D.width ≤ A)
{x : Δ.CompactifiedQuotient}
(hx : x ∈ cuspNhd D A)
:
In cusp charts with common scaling, the map of compactified quotients is the power map whose exponent is the ratio of the cusp widths.