The degree of a finite-index map of compactified Fuchsian quotients

For a finite-index inclusion Δ ≤ Γ of discrete subgroups of PSL(2, ℝ), every fibre of the induced map of compactified quotients has [Γ : Δ] points counted with local multiplicity. Over an interior point this is Subgroup.sum_localMultiplicity_compactifiedQuotientMap_fiber_ofQuotient. Over an adjoined cusp, the cosets of Δ in Γ are partitioned by the cusp orbits of Δ they translate the cusp into; the part belonging to the orbit of c has [stabilizer Γ c : stabilizer Δ c] elements, which is the local multiplicity there, the ratio of cusp widths. Consequently the degree of the map, the supremum of its fibre sums, is the index. No compactness of the quotients is needed.

The computation follows the degree and ramification count for the projection X(Γ) → X(1) in Diamond and Shurman, A First Course in Modular Forms, §3.1.

Main statements

• Subgroup.sum_localMultiplicity_compactifiedQuotientMap_fiber_ofCusp: local multiplicities over an adjoined cusp sum to the index.
• Subgroup.fiberMultiplicitySum_compactifiedQuotientMap: every fibre sum is the index.
• Subgroup.degree_compactifiedQuotientMap: the degree is the index.

theorem Subgroup.sum_localMultiplicity_compactifiedQuotientMap_fiber_ofCusp {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] (h : Δ ≤ Γ) [Δ.IsFiniteRelIndex Γ] (C : Γ.CuspOrbit) : ∑ᶠ (y : { y : Δ.CompactifiedQuotient // compactifiedQuotientMap h y = CompactifiedQuotient.ofCusp C }), TauCeti.RiemannSurface.localMultiplicity (compactifiedQuotientMap h) ↑y = (Δ.subgroupOf Γ).index

The sum of local multiplicities over the fibre above an adjoined cusp of a finite-index quotient map is its subgroup index. The fibre consists of the cusp orbits of the smaller group above the cusp, each counted with its cusp width ratio.

@[simp]

theorem Subgroup.fiberMultiplicitySum_compactifiedQuotientMap {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] (h : Δ ≤ Γ) [Δ.IsFiniteRelIndex Γ] (y : Γ.CompactifiedQuotient) : TauCeti.RiemannSurface.fiberMultiplicitySum (compactifiedQuotientMap h) y = (Δ.subgroupOf Γ).index

Every fibre of a finite-index map of compactified Fuchsian quotients has as many points, counted with local multiplicity, as the index of the subgroup.

@[simp]

theorem Subgroup.degree_compactifiedQuotientMap {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] (h : Δ ≤ Γ) [Δ.IsFiniteRelIndex Γ] : TauCeti.RiemannSurface.degree (compactifiedQuotientMap h) = (Δ.subgroupOf Γ).index

The degree of a finite-index map of compactified Fuchsian quotients is the index. For Δ ≤ Γ discrete of finite index, the map X(Δ) → X(Γ) induced by the inclusion has degree [Γ : Δ].