Changing the scaling of a cusp

Two normalized data at the same cusp have the same positive primitive generator. Their scalings are related by σ' = aσ + b, with a > 0, and their widths satisfy w' = aw. More generally, if an element k ∈ Γ carries the cusp of one datum to the cusp of another, then σ' k σ⁻¹ is such a positive real affine transformation. Consequently their exponential coordinates differ by the constant exp (2πib / (aw)), of modulus one. This is the coordinate transition needed to compare cusp charts on the upper half-plane.

The coordinate accessor TauCeti.Subgroup.CuspDatum.coordinate uses Function.Periodic.qParam, so the statements apply before choosing a complex structure on the cusp quotient. No discreteness hypothesis is needed once normalized cusp data have been supplied.

References

• Fred Diamond and Jerry Shurman, A First Course in Modular Forms, Springer, 2005, §2.4.

theorem TauCeti.cuspDatum_generator_eq {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {D D' : Γ.CuspDatum} (hc : D.cusp = D'.cusp) : D.generator = D'.generator

The positive primitive generator depends only on the cusp, not on its scaling.

theorem TauCeti.cuspDatum_exists_scaling_smul_eq_affine {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {D D' : Γ.CuspDatum} {k : ↥Γ} (hk : k • D.cusp = D'.cusp) : ∃ (a : ℝ) (b : ℝ), 0 < a ∧ ∀ (z : UpperHalfPlane), ↑(D'.scaling • k • z) = ↑a * ↑(D.scaling • z) + ↑b

If k ∈ Γ carries the cusp of D to the cusp of D', then σ' k σ⁻¹ fixes ∞, so it acts on the upper half-plane by a positive real affine transformation.

theorem TauCeti.cuspDatum_exists_scaling_eq_affine {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {D D' : Γ.CuspDatum} (hc : D.cusp = D'.cusp) : ∃ (a : ℝ) (b : ℝ), 0 < a ∧ ∀ (z : UpperHalfPlane), ↑(D'.scaling • z) = ↑a * ↑(D.scaling • z) + ↑b

Any two scalings at the same cusp differ by a positive real affine transformation.

theorem TauCeti.cuspDatum_width_eq_mul {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {D D' : Γ.CuspDatum} (hc : D.cusp = D'.cusp) {a b : ℝ} (hσ : ∀ (z : UpperHalfPlane), ↑(D'.scaling • z) = ↑a * ↑(D.scaling • z) + ↑b) : D'.width = a * D.width

Under σ' = aσ + b, the cusp width changes from w to aw.

theorem TauCeti.cuspDatum_coordinate_eq {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {D D' : Γ.CuspDatum} (hc : D.cusp = D'.cusp) {a b : ℝ} (hσ : ∀ (z : UpperHalfPlane), ↑(D'.scaling • z) = ↑a * ↑(D.scaling • z) + ↑b) (z : UpperHalfPlane) : Subgroup.CuspDatum.coordinate D' z = Complex.exp (2 * ↑Real.pi * Complex.I * ↑b / (↑a * ↑D.width)) * Subgroup.CuspDatum.coordinate D z

The exact change-of-scaling formula for the exponential cusp coordinate.

theorem TauCeti.cuspDatum_norm_coordinate_eq {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {D D' : Γ.CuspDatum} (hc : D.cusp = D'.cusp) (z : UpperHalfPlane) : ‖Subgroup.CuspDatum.coordinate D' z‖ = ‖Subgroup.CuspDatum.coordinate D z‖

The modulus of the exponential cusp coordinate is independent of the normalized scaling.