Cusp widths under subgroup inclusion

For normalized cusp data of Δ ≤ Γ with the same boundary point and scaling, the width for Δ is a positive integer multiple of the width for Γ. In the corresponding coordinates, the map of cusp quotients is therefore the power map q ↦ q ^ n. This is the local input for computing ramification at cusps of maps between compactified Fuchsian quotients.

The integer is forced by the full stabilizers: the primitive generator for Δ lies in the cyclic stabilizer for Γ. The argument does not require finite index of Δ in Γ.

This follows the cusp-width convention of Diamond and Shurman, A First Course in Modular Forms, §2.4.

theorem TauCeti.Subgroup.CuspDatum.exists_width_eq_nat_mul {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (D : Δ.CuspDatum) (E : Γ.CuspDatum) (hc : D.cusp = E.cusp) (hσ : D.scaling = E.scaling) : ∃ (n : ℕ), 0 < n ∧ D.width = ↑n * E.width

With a common scaling, the width for a subgroup is a positive integral multiple of the width for the larger group. The integer is the exponent of the smaller cusp generator in the larger cusp stabilizer.

theorem TauCeti.Subgroup.CuspDatum.width_le_of_width_eq_nat_mul {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Δ.CuspDatum) (E : Γ.CuspDatum) {n : ℕ} (hw : D.width = ↑n * E.width) {A : ℝ} (hD : D.width ≤ A) : E.width ≤ A

A positive integral multiple of a cusp width bounds that width from above.

theorem TauCeti.Subgroup.CuspDatum.coordinate_pow_eq {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Δ.CuspDatum) (E : Γ.CuspDatum) {n : ℕ} (hσ : D.scaling = E.scaling) (hw : D.width = ↑n * E.width) (z : UpperHalfPlane) : coordinate D z ^ n = coordinate E z

The larger group's q-coordinate is the n-th power of the smaller group's coordinate when their normalized widths differ by the factor n.