Local multiplicity of a compactified quotient map at a cusp

For an inclusion of discrete Fuchsian groups, compatible normalized cusp data give local coordinates in which the induced map of compactified quotients is a power map. Consequently its local multiplicity at the adjoined cusp is the canonical cusp width index. Since that index is the relative index of the cusp stabilizers, the local multiplicity at the orbit of a cusp point c is [stabilizer Γ c : stabilizer Δ c], with no choice of cusp data.

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

theorem Subgroup.CompactifiedQuotient.localMultiplicity_compactifiedQuotientMap_ofCusp_eq_widthIndex {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] (h : Δ ≤ Γ) (D : Δ.CuspDatum) (E : Γ.CuspDatum) (hσ : D.scaling = E.scaling) : TauCeti.RiemannSurface.localMultiplicity (compactifiedQuotientMap h) (ofCusp D.cuspOrbit) = TauCeti.Subgroup.CuspDatum.widthIndex h D E ⋯ hσ

For normalized cusp data with the same scaling, the local multiplicity at an adjoined cusp of a compactified quotient map is the canonical positive integer by which the cusp width changes.

theorem Subgroup.CompactifiedQuotient.localMultiplicity_compactifiedQuotientMap_ofCusp_cuspOrbitMk {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] (h : Δ ≤ Γ) (c : ↥Δ.cuspPoints) : TauCeti.RiemannSurface.localMultiplicity (compactifiedQuotientMap h) (ofCusp (cuspOrbitMk c)) = (Δ.subgroupOf Γ).relIndex (MulAction.stabilizer ↥Γ ↑c)

The local multiplicity of a compactified quotient map at the orbit of a cusp point c is the relative index of the smaller group in the stabilizer of c in the larger group, that is, [stabilizer Γ c : stabilizer Δ c].