Degree of a finite-index quotient map over an interior point

The local multiplicities in the fibre over an interior orbit add up to the index of the subgroup. The cosets of the smaller group are partitioned by their images in the fibre; each part has as many elements as the local ramification index at its image. This is the interior-fibre calculation used to identify the degree of a finite-index map of compactified Fuchsian quotients.

theorem Subgroup.sum_localMultiplicity_compactifiedQuotientMap_fiber_ofQuotient {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] (h : Δ ≤ Γ) [Δ.IsFiniteRelIndex Γ] (p : MulAction.orbitRel.Quotient (↥Γ) UpperHalfPlane) : ∑ᶠ (y : { y : Δ.CompactifiedQuotient // compactifiedQuotientMap h y = CompactifiedQuotient.ofQuotient p }), TauCeti.RiemannSurface.localMultiplicity (compactifiedQuotientMap h) ↑y = (Δ.subgroupOf Γ).index

The sum of local multiplicities over an interior fibre of a finite-index quotient map is its subgroup index. This includes elliptic fibres, where the number of points can be smaller than the index.