A cofinite Fuchsian group has finitely many cusp orbits

Let D be a normalized cusp datum of a discrete Γ ≤ PSL(2, ℝ), with scaling σ and width w. The horodisc strip of height A is the part of the horodisc of height A lying over one period: the set of z with 0 ≤ re (σ • z) < w and A < im (σ • z). When A > 0, its hyperbolic area is w / A; in particular the strip of height w has area exactly 1.

Once the height is at least the width, the translates of a horodisc strip by the elements of Γ are pairwise disjoint: two translates can only meet through an element of the cusp stabilizer, by the precise invariance of high horodiscs, and a nontrivial element of the stabilizer shifts re (σ • z) by a nonzero multiple of w. Strips at two inequivalent cusps have disjoint translates when their heights satisfy 0 ≤ A and w * w' ≤ A * A', by Shimizu's inequality at two cusps.

Consequently, choosing one strip of height equal to the width for each cusp orbit produces a family of sets of area 1 whose translates are pairwise disjoint, and a fundamental domain of Γ has at least as much area as their union. Hence the number of cusp orbits is at most the covolume (Subgroup.card_cuspOrbit_le_covolume), and a cofinite Fuchsian group has only finitely many cusp orbits (Subgroup.IsCofinite.finite_cuspOrbit).

Main results

• TauCeti.Subgroup.CuspDatum.volume_horodiscStrip: for A > 0, the horodisc strip of height A has area w / A.
• TauCeti.Subgroup.CuspDatum.iUnion_smul_horodiscStrip: the generator translates of a strip cover its horodisc.
• TauCeti.Subgroup.CuspDatum.pairwise_disjoint_smul_horodiscStrip: for a height at least the width, the Γ-translates of a horodisc strip are pairwise disjoint.
• TauCeti.Subgroup.CuspDatum.disjoint_smul_horodiscStrip_smul_horodiscStrip: the translates of strips at two inequivalent cusps are disjoint when 0 ≤ A and w * w' ≤ A * A'.
• Subgroup.card_cuspOrbit_le_covolume: the number of cusp orbits of a discrete Γ is at most its covolume.
• Subgroup.IsCofinite.finite_cuspOrbit: a cofinite Fuchsian group has finitely many cusp orbits.

References

• Svetlana Katok, Fuchsian Groups, Chicago Lectures in Mathematics, University of Chicago Press, 1992, §§4.1–4.2.
• Alan Beardon, The Geometry of Discrete Groups, Graduate Texts in Mathematics 91, Springer, 1983, §§9.2 and 10.4.

def TauCeti.Subgroup.CuspDatum.horodiscStrip {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (A : ℝ) : Set UpperHalfPlane

The horodisc strip of height A at the cusp represented by D: the part of the horodisc of height A lying over one period [0, width) in the scaling coordinate.

Equations

• TauCeti.Subgroup.CuspDatum.horodiscStrip D A = {z : UpperHalfPlane | (D.scaling • z).re ∈ Set.Ico 0 D.width ∧ A < (D.scaling • z).im}

@[simp]

theorem TauCeti.Subgroup.CuspDatum.mem_horodiscStrip {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) {A : ℝ} {z : UpperHalfPlane} : z ∈ horodiscStrip D A ↔ (D.scaling • z).re ∈ Set.Ico 0 D.width ∧ A < (D.scaling • z).im

Membership in a horodisc strip is a bound on the real part and a lower bound on the imaginary part in the scaling coordinate.

theorem TauCeti.Subgroup.CuspDatum.horodiscStrip_subset_horodisc {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (A : ℝ) : horodiscStrip D A ⊆ horodisc D A

A horodisc strip lies in the horodisc of the same height.

theorem TauCeti.Subgroup.CuspDatum.horodiscStrip_eq_inv_smul {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (A : ℝ) : horodiscStrip D A = D.scaling⁻¹ • {z : UpperHalfPlane | z.re ∈ Set.Ico 0 D.width ∧ A < z.im}

The horodisc strip is the image under σ⁻¹ of the region over [0, width) above height A.

theorem TauCeti.Subgroup.CuspDatum.iUnion_smul_horodiscStrip {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (A : ℝ) : ⋃ (n : ℤ), D.generator ^ n • horodiscStrip D A = horodisc D A

The translates of one horodisc strip by powers of the cusp generator cover the whole horodisc.

theorem TauCeti.Subgroup.CuspDatum.measurableSet_horodiscStrip {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (A : ℝ) : MeasurableSet (horodiscStrip D A)

A horodisc strip is measurable.

theorem TauCeti.Subgroup.CuspDatum.volume_horodiscStrip {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) {A : ℝ} (hA : 0 < A) : MeasureTheory.volume (horodiscStrip D A) = ENNReal.ofReal (D.width / A)

The area of a horodisc strip. The horodisc strip of height A > 0 has hyperbolic area width / A.

@[simp]

theorem TauCeti.Subgroup.CuspDatum.volume_horodiscStrip_width {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) : MeasureTheory.volume (horodiscStrip D D.width) = 1

The horodisc strip whose height is the width has hyperbolic area 1.

theorem TauCeti.Subgroup.CuspDatum.pairwise_disjoint_smul_horodiscStrip {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) [DiscreteTopology ↥Γ] {A : ℝ} (hA : D.width ≤ A) : Pairwise fun (g h : ↥Γ) => Disjoint (g • horodiscStrip D A) (h • horodiscStrip D A)

The translates of a high horodisc strip are pairwise disjoint. Let D be a normalized cusp datum of a discrete Γ ≤ PSL(2, ℝ) and let the height A be at least the width of D. Then the translates of the horodisc strip of height A by distinct elements of Γ are disjoint.

theorem TauCeti.Subgroup.CuspDatum.disjoint_smul_horodiscStrip_smul_horodiscStrip {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) [DiscreteTopology ↥Γ] (D' : Γ.CuspDatum) (hc : D'.cusp ∉ MulAction.orbit (↥Γ) D.cusp) {A A' : ℝ} (hA : 0 ≤ A) (hAA' : D.width * D'.width ≤ A * A') (g h : ↥Γ) : Disjoint (g • horodiscStrip D A) (h • horodiscStrip D' A')

Horodisc strips at inequivalent cusps have disjoint translates. Let D and D' be normalized cusp data of a discrete Γ ≤ PSL(2, ℝ) whose cusps are not Γ-equivalent, and let the heights satisfy 0 ≤ A and D.width * D'.width ≤ A * A'. Then every translate of the strip at D is disjoint from every translate of the strip at D'.

theorem Subgroup.card_cuspOrbit_le_covolume {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] : ↑(ENat.card Γ.CuspOrbit) ≤ MeasureTheory.covolume (↥Γ) UpperHalfPlane MeasureTheory.volume

The number of cusp orbits is at most the covolume. For a discrete subgroup Γ ≤ PSL(2, ℝ), the cardinality of the set of cusp orbits is at most the hyperbolic area of the quotient Γ \ ℍ.

theorem Subgroup.IsCofinite.finite_cuspOrbit {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hΓ : Γ.IsCofinite) : Finite Γ.CuspOrbit

A cofinite Fuchsian group has finitely many cusp orbits.