Cusp meridians and their lifts #

For a normalized cusp datum D, the horizontal path in scaling coordinates from σ(z) to σ(z) + n w projects under the q-coordinate to the loop q(z) exp (2 π i n t). For n = 1 this traverses its circle counterclockwise once. Its unique lift starting at z ends at D.generator • z, not at its inverse. More generally, the endpoint for n signed turns is D.generator ^ n • z.

These paths stay at constant scaled height, so they lie in every horodisc containing their basepoint. Reversing a meridian negates the number of turns and inverts its endpoint transformation. This fixes the orientation convention for cusp relations in quotient presentations.

Uniqueness uses Mathlib's exponential covering map, rather than a chosen logarithm along the loop. No discreteness or cofiniteness assumption is needed once the normalized datum is supplied.

References #

Fred Diamond and Jerry Shurman, A First Course in Modular Forms, §2.4.
Otto Forster, Lectures on Riemann Surfaces, §19.

source

noncomputable def TauCeti.Subgroup.CuspDatum.meridianLift {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (n : ℤ) (z : UpperHalfPlane) :

Path z (D.generator ^ n • z)

The lift of n signed turns around a cusp: horizontal translation through n widths in the scaling coordinate.

Equations

TauCeti.Subgroup.CuspDatum.meridianLift D n z = { toFun := fun (t : ↑unitInterval) => D.scaling⁻¹ • (↑t * ↑n * D.width +ᵥ D.scaling • z), continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

Instances For

source

theorem TauCeti.Subgroup.CuspDatum.meridianLift_apply {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (n : ℤ) (z : UpperHalfPlane) (t : ↑unitInterval) :

(meridianLift D n z) t = D.scaling⁻¹ • (↑t * ↑n * D.width +ᵥ D.scaling • z)

The horizontal lift, evaluated at a time in the unit interval.

source

@[simp]

theorem TauCeti.Subgroup.CuspDatum.scaling_smul_meridianLift {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (n : ℤ) (z : UpperHalfPlane) (t : ↑unitInterval) :

D.scaling • (meridianLift D n z) t = ↑t * ↑n * D.width +ᵥ D.scaling • z

In scaling coordinates, a meridian lift is horizontal translation at constant speed.

source

noncomputable def TauCeti.Subgroup.CuspDatum.meridian {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (n : ℤ) (z : UpperHalfPlane) :

Path (qCoordinate D z) (qCoordinate D z)

The cusp meridian with n signed turns, based at the q-coordinate of z.

Equations

TauCeti.Subgroup.CuspDatum.meridian D n z = ((TauCeti.Subgroup.CuspDatum.meridianLift D n z).map ⋯).cast ⋯ ⋯

Instances For

source

@[simp]

theorem TauCeti.Subgroup.CuspDatum.meridian_apply {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (n : ℤ) (z : UpperHalfPlane) (t : ↑unitInterval) :

(meridian D n z) t = qCoordinate D ((meridianLift D n z) t)

The meridian is the q-projection of its horizontal lift.

source

@[simp]

theorem TauCeti.Subgroup.CuspDatum.coe_meridian {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (n : ℤ) (z : UpperHalfPlane) (t : ↑unitInterval) :

↑↑((meridian D n z) t) = coordinate D z * Complex.exp (↑n * (2 * ↑Real.pi * Complex.I) * ↑↑t)

The meridian makes exactly n signed turns about zero. Positive turns are counterclockwise in the complex q-plane.

source

theorem TauCeti.Subgroup.CuspDatum.eq_meridianLift_of_qCoordinate_eq {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (n : ℤ) (z : UpperHalfPlane) {f : ↑unitInterval → UpperHalfPlane} (hf : Continuous f) (h₀ : f 0 = z) (hq : ∀ (t : ↑unitInterval), qCoordinate D (f t) = (meridian D n z) t) :

f = ⇑(meridianLift D n z)

The horizontal path is the unique continuous lift of the meridian starting at z. In particular its endpoint is the nth power of the selected primitive generator.

source