Local multiplicity of a compactified quotient map at an elliptic orbit

For an inclusion of discrete Fuchsian groups, the induced map of compactified quotients has local multiplicity at an interior orbit equal to the relative index of the two point stabilizers. This follows from the power-map expression in the compatible elliptic charts.

The local cyclic quotient model follows Farkas--Kra, Riemann Surfaces, Chapter I, §§4--5.

theorem Subgroup.CompactifiedQuotient.localMultiplicity_compactifiedQuotientMap_ofQuotient_eq_ellipticRamificationIndex {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] (h : Δ ≤ Γ) (z : UpperHalfPlane) : TauCeti.RiemannSurface.localMultiplicity (compactifiedQuotientMap h) (ofQuotient (Quotient.mk'' z)) = ellipticRamificationIndex h z

At an interior orbit, the local multiplicity of a compactified quotient map is the relative index of the source point stabilizer in the target point stabilizer.