High horodiscs in a Fuchsian quotient

For a normalized cusp datum D and a height at least its width, the horodisc at that height is precisely invariant under the cusp stabilizer. This file packages the horodisc as an invariant subspace for that stabilizer and proves that its orbit space maps by an open embedding into the coarse quotient Γ \\ ℍ. The image is an open subset that can serve as a punctured cusp chart domain after compactification, with the q-coordinate supplied by the stabilizer quotient.

References

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

@[reducible, inline]

abbrev TauCeti.Subgroup.CuspDatum.horodiscSubMulAction {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (A : ℝ) : SubMulAction (↥(MulAction.stabilizer (↥Γ) D.cusp)) UpperHalfPlane

The horodisc at D's cusp, as an invariant subspace for its full stabilizer.

Equations

• TauCeti.Subgroup.CuspDatum.horodiscSubMulAction D A = { carrier := TauCeti.Subgroup.CuspDatum.horodisc D A, smul_mem' := ⋯ }

@[simp]

theorem TauCeti.Subgroup.CuspDatum.coe_horodiscSubMulAction {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (A : ℝ) : ↑(horodiscSubMulAction D A) = horodisc D A

@[simp]

theorem TauCeti.Subgroup.CuspDatum.mem_horodiscSubMulAction {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) {A : ℝ} {z : UpperHalfPlane} : z ∈ horodiscSubMulAction D A ↔ z ∈ horodisc D A

noncomputable def TauCeti.Subgroup.CuspDatum.horodiscQuotientToQuotient {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (A : ℝ) : MulAction.orbitRel.Quotient ↥(MulAction.stabilizer (↥Γ) D.cusp) ↥(horodiscSubMulAction D A) → MulAction.orbitRel.Quotient (↥Γ) UpperHalfPlane

The map from the cusp-stabilizer quotient of a horodisc to the full coarse quotient.

Equations

• TauCeti.Subgroup.CuspDatum.horodiscQuotientToQuotient D A = Quotient.map' Subtype.val ⋯

@[simp]

theorem TauCeti.Subgroup.CuspDatum.horodiscQuotientToQuotient_mk {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) {A : ℝ} (z : ↥(horodiscSubMulAction D A)) : horodiscQuotientToQuotient D A ⟦z⟧ = ⟦↑z⟧

theorem TauCeti.Subgroup.CuspDatum.continuous_horodiscQuotientToQuotient {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (A : ℝ) : Continuous (horodiscQuotientToQuotient D A)

The local quotient map of a horodisc is continuous.

theorem TauCeti.Subgroup.CuspDatum.isOpenMap_horodiscQuotientToQuotient {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (A : ℝ) : IsOpenMap (horodiscQuotientToQuotient D A)

The local quotient map of a horodisc is open onto its image in the coarse quotient.

theorem TauCeti.Subgroup.CuspDatum.range_horodiscQuotientToQuotient {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (A : ℝ) : Set.range (horodiscQuotientToQuotient D A) = Quotient.mk (MulAction.orbitRel (↥Γ) UpperHalfPlane) '' horodisc D A

The range of the local quotient map is the image of the horodisc in the coarse quotient.

theorem TauCeti.Subgroup.CuspDatum.quotientMk_eq_iff_qCoordinate_eq {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) [DiscreteTopology ↥Γ] {A : ℝ} (hA : D.width ≤ A) {z z' : UpperHalfPlane} (hz : z ∈ horodisc D A) (hz' : z' ∈ horodisc D A) : ⟦z⟧ = ⟦z'⟧ ↔ qCoordinate D z = qCoordinate D z'

On a high horodisc, two points have the same image in the coarse quotient exactly when their q-coordinates agree. Thus the q-coordinate distinguishes the points of the punctured cusp neighbourhood in the coarse quotient.

theorem TauCeti.Subgroup.CuspDatum.isOpenEmbedding_horodiscQuotientToQuotient {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) [DiscreteTopology ↥Γ] {A : ℝ} (hA : D.width ≤ A) : Topology.IsOpenEmbedding (horodiscQuotientToQuotient D A)

Above the cusp width, the local horodisc quotient embeds openly into the coarse quotient.

theorem TauCeti.Subgroup.CuspDatum.isOpen_image_quotientMk_horodisc {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (A : ℝ) : IsOpen (Quotient.mk (MulAction.orbitRel (↥Γ) UpperHalfPlane) '' horodisc D A)

A horodisc has open image in the coarse quotient.