The q-coordinate chart at a cusp of the compactified quotient

Let Γ ≤ PSL(2, ℝ) be discrete and D a normalized cusp datum of Γ with scaling σ and width w. For a height A ≥ w the horodisc of height A at D is precisely invariant under the cusp stabilizer, so the q-coordinate q(z) = exp (2 * π * I * σ(z) / w) descends to the image of the horodisc in the coarse quotient Γ \ ℍ, and it extends by q = 0 to the cusp orbit adjoined in the compactified quotient. This file packages this extension as an open partial homeomorphism Subgroup.CompactifiedQuotient.cuspChart D hA from the compactified quotient to ℂ: its source is the cusp neighbourhood cuspNhd D A and its target the disc of radius cuspRadius D A, the exponential exp (-2 * π * A / w) of the height. On the target, the inverse sends 0 to the cusp orbit and a nonzero q to the orbit of the logarithmic lift σ⁻¹ • invQParam w q.

Continuity at the cusp orbit is the fact that the q-coordinate tends to 0 along the cusp and, conversely, that the logarithmic lift of a small q lies in a high horodisc. Continuity away from the cusp orbit comes from the open quotient map qCoordinate D onto the punctured unit disc. The compatibility of these charts with the atlas of the coarse quotient, and the resulting Riemann surface structure on the compactified quotient, are not part of this file.

Main declarations

• Subgroup.CompactifiedQuotient.cuspRadius: the radius exp (-2 * π * A / w) of the q-disc corresponding to the horodisc of height A.
• Subgroup.CompactifiedQuotient.cuspChart: the cusp chart, with Subgroup.CompactifiedQuotient.cuspChart_ofCusp and Subgroup.CompactifiedQuotient.cuspChart_ofQuotient_mk computing it on its source, and Subgroup.CompactifiedQuotient.cuspChart_symm_zero, Subgroup.CompactifiedQuotient.cuspChart_symm_coordinate and Subgroup.CompactifiedQuotient.cuspChart_symm_of_ne_zero computing its inverse on its target.

The underlying total maps of the chart and its inverse are implementation details: outside the source and target their values are junk, so they are private.

References

• Fred Diamond and Jerry Shurman, A First Course in Modular Forms, Graduate Texts in Mathematics 228, Springer, 2005, §2.4.
• Otto Forster, Lectures on Riemann Surfaces, Graduate Texts in Mathematics 81, Springer, 1981, §19.
• Svetlana Katok, Fuchsian Groups, Chicago Lectures in Mathematics, University of Chicago Press, 1992, §4.2.

The radius of the q-disc

noncomputable def Subgroup.CompactifiedQuotient.cuspRadius {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (A : ℝ) : ℝ

The radius exp (-2 * π * A / w) of the punctured q-disc onto which the horodisc of height A is mapped by the q-coordinate of a cusp datum of width w.

Equations

• Subgroup.CompactifiedQuotient.cuspRadius D A = Real.exp (-2 * Real.pi * A / D.width)

theorem Subgroup.CompactifiedQuotient.cuspRadius_pos {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (A : ℝ) : 0 < cuspRadius D A

theorem Subgroup.CompactifiedQuotient.cuspRadius_lt_one {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) {A : ℝ} (hA : 0 < A) : cuspRadius D A < 1

theorem Subgroup.CompactifiedQuotient.cuspRadius_antitone {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) : Antitone (cuspRadius D)

theorem Subgroup.CompactifiedQuotient.tendsto_cuspRadius_atTop {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) : Filter.Tendsto (cuspRadius D) Filter.atTop (nhds 0)

The radius of the q-disc tends to zero as the height tends to infinity.

theorem Subgroup.CompactifiedQuotient.norm_coordinate_lt_cuspRadius_iff {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (A : ℝ) (z : UpperHalfPlane) : ‖TauCeti.Subgroup.CuspDatum.coordinate D z‖ < cuspRadius D A ↔ z ∈ TauCeti.Subgroup.CuspDatum.horodisc D A

A horodisc is the inverse image of the q-disc of the corresponding radius.

The forward map

The total map underlying the cusp chart. Its values off the cusp neighbourhood are junk, so it and its lemmas are private.

The inverse map

The total map underlying the inverse of the cusp chart. Its values off the unit disc are junk, so it and its lemmas are private.

Continuity

The chart

noncomputable def Subgroup.CompactifiedQuotient.cuspChart {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) {A : ℝ} [DiscreteTopology ↥Γ] (hA : D.width ≤ A) : OpenPartialHomeomorph Γ.CompactifiedQuotient ℂ

The cusp chart of the compactified quotient at the cusp datum D and a height A at least its width. Its source is the cusp neighbourhood cuspNhd D A and its target the disc of radius cuspRadius D A; it sends the cusp orbit to 0 and the orbit of a point z of the horodisc to its q-coordinate coordinate D z.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Subgroup.CompactifiedQuotient.cuspChart_source {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) {A : ℝ} [DiscreteTopology ↥Γ] (hA : D.width ≤ A) : (cuspChart D hA).source = cuspNhd D A

@[simp]

theorem Subgroup.CompactifiedQuotient.cuspChart_target {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) {A : ℝ} [DiscreteTopology ↥Γ] (hA : D.width ≤ A) : (cuspChart D hA).target = Metric.ball 0 (cuspRadius D A)

theorem Subgroup.CompactifiedQuotient.ofCusp_mem_cuspChart_source {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) {A : ℝ} [DiscreteTopology ↥Γ] (hA : D.width ≤ A) : ofCusp D.cuspOrbit ∈ (cuspChart D hA).source

@[simp]

theorem Subgroup.CompactifiedQuotient.cuspChart_ofCusp {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) {A : ℝ} [DiscreteTopology ↥Γ] (hA : D.width ≤ A) : ↑(cuspChart D hA) (ofCusp D.cuspOrbit) = 0

The cusp chart sends its cusp orbit to 0.

@[simp]

theorem Subgroup.CompactifiedQuotient.cuspChart_ofQuotient_mk {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) {A : ℝ} [DiscreteTopology ↥Γ] (hA : D.width ≤ A) {z : UpperHalfPlane} (hz : z ∈ TauCeti.Subgroup.CuspDatum.horodisc D A) : ↑(cuspChart D hA) (ofQuotient ⟦z⟧) = TauCeti.Subgroup.CuspDatum.coordinate D z

The cusp chart sends the orbit of a point of the horodisc to its q-coordinate.

@[simp]

theorem Subgroup.CompactifiedQuotient.cuspChart_symm_zero {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) {A : ℝ} [DiscreteTopology ↥Γ] (hA : D.width ≤ A) : ↑(cuspChart D hA).symm 0 = ofCusp D.cuspOrbit

The inverse of the cusp chart sends 0 to the cusp orbit.

@[simp]

theorem Subgroup.CompactifiedQuotient.cuspChart_symm_coordinate {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) {A : ℝ} [DiscreteTopology ↥Γ] (hA : D.width ≤ A) {z : UpperHalfPlane} (hz : z ∈ TauCeti.Subgroup.CuspDatum.horodisc D A) : ↑(cuspChart D hA).symm (TauCeti.Subgroup.CuspDatum.coordinate D z) = ofQuotient ⟦z⟧

The inverse of the cusp chart sends the q-coordinate of a point of the horodisc to its orbit.

theorem Subgroup.CompactifiedQuotient.cuspChart_symm_of_ne_zero {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) {A : ℝ} [DiscreteTopology ↥Γ] (hA : D.width ≤ A) {q : ℂ} (hq : q ∈ (cuspChart D hA).target) (hq0 : q ≠ 0) : ↑(cuspChart D hA).symm q = ofQuotient ⟦D.scaling⁻¹ • ↑UpperHalfPlane.ofComplex (Function.Periodic.invQParam D.width q)⟧

The inverse of the cusp chart sends a nonzero point q of its target to the orbit of the logarithmic lift σ⁻¹ • invQParam w q.