The cusp index as a local ramification exponent

The canonical width index of compatible cusp data is the exponent of the compactified quotient map in their cusp coordinates. Its tower law therefore describes composition of these local power maps, including at the adjoined cusp.

The cusp-coordinate convention follows Diamond and Shurman, A First Course in Modular Forms, §2.4.

theorem Subgroup.CompactifiedQuotient.cuspChart_compactifiedQuotientMap_eq_pow_widthIndex {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Δ] [DiscreteTopology ↥Γ] (h : Δ ≤ Γ) (D : Δ.CuspDatum) (E : Γ.CuspDatum) (hc : D.cusp = E.cusp) (hσ : D.scaling = E.scaling) {A : ℝ} (hD : D.width ≤ A) {x : Δ.CompactifiedQuotient} (hx : x ∈ cuspNhd D A) : ↑(cuspChart E ⋯) (compactifiedQuotientMap h x) = ↑(cuspChart D hD) x ^ TauCeti.Subgroup.CuspDatum.widthIndex h D E hc hσ

The compactified quotient map has local exponent equal to the canonical cusp width index.