The q-coordinate of a normalized cusp datum

For a cusp datum with scaling σ and width w, the coordinate is q(z) = exp (2 * π * I * σ(z) / w). Its fibres are exactly the orbits of the full cusp stabilizer. It therefore identifies the stabilizer quotient of the upper half-plane with the punctured unit disc. The forward map is the q-coordinate and the inverse is the orbit of a logarithmic lift transported back by σ⁻¹.

This uses the translation quotient computed in TauCeti.Analysis.Complex.UpperHalfPlane.CuspCoordinate. No discreteness assumption is needed once a normalized cusp datum is given: its primitive-generator condition identifies the full stabilizer. The coordinate is holomorphic, and scaled horodiscs of positive height correspond exactly to smaller punctured discs. This is a local model for cusp charts; embedding such a neighbourhood into the full group quotient additionally requires precise invariance of the horodisc.

References

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

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

The exponential coordinate of a normalized cusp datum on the upper half-plane.

Equations

• TauCeti.Subgroup.CuspDatum.coordinate D z = Function.Periodic.qParam D.width ↑(D.scaling • z)

theorem TauCeti.Subgroup.CuspDatum.coordinate_apply {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (z : UpperHalfPlane) : coordinate D z = Function.Periodic.qParam D.width ↑(D.scaling • z)

The cusp coordinate is the q-parameter of the scaled point, with the datum's width.

@[simp]

theorem TauCeti.Subgroup.CuspDatum.coordinate_inv_smul {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (z : UpperHalfPlane) : coordinate D (D.scaling⁻¹ • z) = Function.Periodic.qParam D.width ↑z

Applying the inverse scaling before the cusp coordinate recovers the ordinary q-parameter.

@[simp]

theorem TauCeti.Subgroup.CuspDatum.coordinate_ne_zero {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (z : UpperHalfPlane) : coordinate D z ≠ 0

The exponential cusp coordinate never vanishes on the upper half-plane.

theorem TauCeti.Subgroup.CuspDatum.norm_coordinate_lt_one {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (z : UpperHalfPlane) : ‖coordinate D z‖ < 1

The exponential cusp coordinate lies in the open unit disc.

theorem TauCeti.Subgroup.CuspDatum.coe_scaling_smul_generator {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (z : UpperHalfPlane) : ↑(D.scaling • ↑D.generator • z) = ↑(D.scaling • z) + ↑D.width

In scaling coordinates, the selected generator acts by translation through the width.

@[simp]

theorem TauCeti.Subgroup.CuspDatum.coordinate_smul {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) {g : ↥Γ} (hg : g ∈ MulAction.stabilizer (↥Γ) D.cusp) (z : UpperHalfPlane) : coordinate D (g • z) = coordinate D z

The exponential cusp coordinate is invariant under the full cusp stabilizer.

theorem TauCeti.Subgroup.CuspDatum.eq_of_coordinate_eq {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) {A : Type u_1} [TopologicalSpace A] [PreconnectedSpace A] {f g : A → UpperHalfPlane} (hf : Continuous f) (hg : Continuous g) (hq : ∀ (a : A), coordinate D (f a) = coordinate D (g a)) (a₀ : A) (h₀ : f a₀ = g a₀) : f = g

Continuous lifts with the same q-projection agree if they agree at one point of a preconnected source.

theorem TauCeti.Subgroup.CuspDatum.scaling_smul_generator_zpow {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (n : ℤ) (z : UpperHalfPlane) : D.scaling • D.generator ^ n • z = ↑n * D.width +ᵥ D.scaling • z

In the scaling coordinate, powers of the primitive cusp generator are integral-width translations.

noncomputable def TauCeti.Subgroup.CuspDatum.qCoordinate {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (z : UpperHalfPlane) : { q : Complex.UnitDisc // q ≠ 0 }

The exponential coordinate, regarded as a map into the punctured unit disc.

Equations

• TauCeti.Subgroup.CuspDatum.qCoordinate D z = ⟨Complex.UnitDisc.mk (TauCeti.Subgroup.CuspDatum.coordinate D z) ⋯, ⋯⟩

theorem TauCeti.Subgroup.CuspDatum.qCoordinate_eq {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (z : UpperHalfPlane) : qCoordinate D z = UpperHalfPlane.qParamPuncturedUnitDisc D.width ⋯ (D.scaling • z)

Evaluation of the normalized q-coordinate as the width parameter after scaling.

theorem TauCeti.Subgroup.CuspDatum.qCoordinate_eq_comp {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) : qCoordinate D = UpperHalfPlane.qParamPuncturedUnitDisc D.width ⋯ ∘ fun (x : UpperHalfPlane) => D.scaling • x

The normalized q-coordinate is the width parameter composed with scaling.

@[simp]

theorem TauCeti.Subgroup.CuspDatum.coe_qCoordinate {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (z : UpperHalfPlane) : ↑↑(qCoordinate D z) = coordinate D z

theorem TauCeti.Subgroup.CuspDatum.orbitRel_iff_qCoordinate_eq {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (z z' : UpperHalfPlane) : (MulAction.orbitRel (↥(MulAction.stabilizer (↥Γ) D.cusp)) UpperHalfPlane) z z' ↔ qCoordinate D z = qCoordinate D z'

The q-coordinate has exactly the full cusp-stabilizer orbits as its fibres.

theorem TauCeti.Subgroup.CuspDatum.qCoordinate_eq_iff {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (z z' : UpperHalfPlane) : qCoordinate D z = qCoordinate D z' ↔ ∃ (n : ℤ), z = D.generator ^ n • z'

Two points have the same q-coordinate exactly when they differ by an integer power of the selected generator.

@[simp]

theorem TauCeti.Subgroup.CuspDatum.qCoordinate_smul {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (g : ↥(MulAction.stabilizer (↥Γ) D.cusp)) (z : UpperHalfPlane) : qCoordinate D (g • z) = qCoordinate D z

The q-coordinate is invariant under the full stabilizer, not just the selected generator.

@[simp]

theorem TauCeti.Subgroup.CuspDatum.qCoordinate_smul_of_mem {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) {g : ↥Γ} (hg : g ∈ MulAction.stabilizer (↥Γ) D.cusp) (z : UpperHalfPlane) : qCoordinate D (g • z) = qCoordinate D z

The q-coordinate is invariant under any group element fixing the cusp.

@[simp]

theorem TauCeti.Subgroup.CuspDatum.qCoordinate_smul_invQParamUpperHalfPlane {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (q : { q : Complex.UnitDisc // q ≠ 0 }) : qCoordinate D (D.scaling⁻¹ • UpperHalfPlane.invQParamUpperHalfPlane D.width ⋯ q) = q

The scaled logarithmic lift is a right inverse of the q-coordinate.

noncomputable def TauCeti.Subgroup.CuspDatum.quotientHomeomorph {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) : MulAction.orbitRel.Quotient (↥(MulAction.stabilizer (↥Γ) D.cusp)) UpperHalfPlane ≃ₜ { q : Complex.UnitDisc // q ≠ 0 }

The q-coordinate identifies the quotient by the full cusp stabilizer with the punctured unit disc.

Equations

• TauCeti.Subgroup.CuspDatum.quotientHomeomorph D = (Homeomorph.Quotient.congr (Homeomorph.smul D.scaling) ⋯).trans (TauCeti.UpperHalfPlane.cuspTranslationQuotientHomeomorph D.width ⋯)

@[simp]

theorem TauCeti.Subgroup.CuspDatum.quotientHomeomorph_mk {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (z : UpperHalfPlane) : (quotientHomeomorph D) (Quotient.mk'' z) = qCoordinate D z

The quotient homeomorphism sends the orbit of a point to its q-coordinate.

@[simp]

theorem TauCeti.Subgroup.CuspDatum.quotientHomeomorph_symm_apply {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (q : { q : Complex.UnitDisc // q ≠ 0 }) : (quotientHomeomorph D).symm q = Quotient.mk'' (D.scaling⁻¹ • UpperHalfPlane.invQParamUpperHalfPlane D.width ⋯ q)

The inverse quotient homeomorphism sends a punctured-disc point to the orbit of its width-dependent logarithmic lift transported back by the inverse scaling.

theorem TauCeti.Subgroup.CuspDatum.isOpenQuotientMap_qCoordinate {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) : IsOpenQuotientMap (qCoordinate D)

The normalized q-coordinate is an open quotient map.

theorem TauCeti.Subgroup.CuspDatum.mdifferentiable_qCoordinate {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) : MDiff (qCoordinate D)

The normalized q-coordinate is holomorphic as a map into the punctured unit disc.

theorem TauCeti.Subgroup.CuspDatum.mdifferentiable_coordinate {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) : MDiff (coordinate D)

The normalized q-coordinate, regarded as a complex-valued function, is holomorphic.

theorem TauCeti.Subgroup.CuspDatum.norm_qCoordinate_lt_iff {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (A : ℝ) (z : UpperHalfPlane) : ‖↑↑(qCoordinate D z)‖ < Real.exp (-2 * Real.pi * A / D.width) ↔ A < (D.scaling • z).im

A scaled horodisc is exactly the inverse image of a punctured disc under the q-coordinate.

theorem TauCeti.Subgroup.CuspDatum.image_qCoordinate_setOf_lt_im {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (A : ℝ) : qCoordinate D '' {z : UpperHalfPlane | A < (D.scaling • z).im} = {q : { q : Complex.UnitDisc // q ≠ 0 } | ‖↑↑q‖ < Real.exp (-2 * Real.pi * A / D.width)}

The image of a scaled horodisc is the punctured disc of the corresponding exponential radius.

theorem TauCeti.Subgroup.CuspDatum.tendsto_qCoordinate {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) {α : Type u_1} {l : Filter α} {f : α → UpperHalfPlane} (h : Filter.Tendsto (fun (a : α) => D.scaling • f a) l UpperHalfPlane.atImInfty) : Filter.Tendsto (fun (a : α) => ↑↑(qCoordinate D (f a))) l (nhdsWithin 0 {0}ᶜ)

The q-coordinate tends to zero whenever the height in the scaling coordinate tends to infinity. The limit is through nonzero values, as required for a punctured cusp chart.