Normalized cusp data of a Fuchsian group

Let Γ ≤ PSL(2, ℝ) be a discrete subgroup and c ∈ OnePoint ℝ a cusp point of Γ, that is, a point fixed by a parabolic element of Γ. Choose σ ∈ PSL(2, ℝ) with σ • c = ∞. Then the stabilizer of c in Γ is infinite cyclic, and σ conjugates it onto the group of translations z ↦ z + n * w, n ∈ ℤ, for a unique w > 0, the width of the cusp relative to σ.

The result is packaged as a normalized cusp datum Subgroup.CuspDatum: a cusp, a scaling, a generator of the full stabilizer, and a positive width with the conjugation formula. Such a datum records exactly the choices from which cusp neighbourhoods and the q-coordinate exp (2 * π * I * σ z / w) are built. The width is not an invariant of the cusp alone; it depends on the scaling, and the datum is unique once the cusp and the scaling are fixed.

Main declarations

• Subgroup.CuspDatum: normalized cusp data of Γ ≤ PSL(2, ℝ).
• Subgroup.CuspDatum.cusp_eq_of_scaling_eq: cusp data with equal scalings have equal cusps.
• Subgroup.CuspDatum.mem_stabilizer_iff_conj: the conjugated stabilizer of the cusp is exactly the group of translations by width * ℤ.
• Subgroup.CuspDatum.ext: a cusp datum is determined by its cusp and scaling.
• Subgroup.IsCuspPoint.exists_cuspDatum: for a discrete Γ, every cusp point and every scaling sending it to ∞ carry a cusp datum.

References

• Alan Beardon, The Geometry of Discrete Groups, Graduate Texts in Mathematics 91, Springer, 1983, §§5.1 and 9.2.
• Svetlana Katok, Fuchsian Groups, Chicago Lectures in Mathematics, University of Chicago Press, 1992, §§2.2 and 4.2.
• Fred Diamond and Jerry Shurman, A First Course in Modular Forms, Graduate Texts in Mathematics 228, Springer, 2005, §2.4.

structure Subgroup.CuspDatum (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) : Type

Normalized cusp data. A cusp datum of Γ ≤ PSL(2, ℝ) consists of a boundary point cusp, a scaling σ ∈ PSL(2, ℝ), an element generator of Γ generating the full stabilizer of cusp in Γ, and a positive width such that σ * generator * σ⁻¹ is the translation z ↦ z + width. Consequently σ sends cusp to ∞ (Subgroup.CuspDatum.scaling_smul_cusp), cusp is a cusp point (Subgroup.CuspDatum.isCuspPoint), and conjugation by σ identifies the full stabilizer with the translations by width * ℤ (Subgroup.CuspDatum.mem_stabilizer_iff_conj).

The width depends on the scaling and not only on the cusp; given the cusp and the scaling, the datum is unique (Subgroup.CuspDatum.ext). In particular a proper power of the generator, although also conjugate to a positive translation, never forms a cusp datum. For a discrete Γ, every cusp point and every scaling sending it to ∞ carry a cusp datum (Subgroup.IsCuspPoint.exists_cuspDatum).

• cusp : OnePoint ℝ

  The cusp point.

• scaling : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ

  A projective transformation, which sends cusp to ∞.

• generator : ↥Γ

  The selected generator of the stabilizer of cusp in Γ.

• width : ℝ

  The width of the cusp relative to scaling.

• width_pos : 0 < self.width
• zpowers_generator : zpowers self.generator = MulAction.stabilizer (↥Γ) self.cusp
• scaling_mul_generator_mul_inv : self.scaling * ↑self.generator * self.scaling⁻¹ = Matrix.ProjectiveSpecialLinearGroup.upperRightHom self.width

theorem Subgroup.CuspDatum.generator_mem_stabilizer {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) : D.generator ∈ MulAction.stabilizer (↥Γ) D.cusp

The selected generator fixes the cusp.

@[simp]

theorem Subgroup.CuspDatum.isParabolic_generator {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) : (↑D.generator).IsParabolic

The selected generator of the stabilizer of a cusp is parabolic.

@[simp]

theorem Subgroup.CuspDatum.scaling_smul_cusp {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) : D.scaling • D.cusp = OnePoint.infty

The scaling of a cusp datum sends the cusp to ∞.

theorem Subgroup.CuspDatum.cusp_eq_of_scaling_eq {Γ Δ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Δ.CuspDatum) (E : Γ.CuspDatum) (hσ : D.scaling = E.scaling) : D.cusp = E.cusp

Cusp data with the same scaling represent the same boundary point.

theorem Subgroup.CuspDatum.isCuspPoint {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) : Γ.IsCuspPoint D.cusp

The point of a cusp datum is a cusp point.

noncomputable def Subgroup.CuspDatum.cuspOrbit {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) : Γ.CuspOrbit

The cusp orbit represented by a cusp datum.

Equations

• D.cuspOrbit = Subgroup.cuspOrbitMk ⟨D.cusp, ⋯⟩

@[simp]

theorem Subgroup.CuspDatum.cuspOrbit_val {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) : ↑D.cuspOrbit = Quotient.mk'' D.cusp

theorem Subgroup.CuspDatum.cuspOrbit_eq_iff {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D D' : Γ.CuspDatum) : D.cuspOrbit = D'.cuspOrbit ↔ D.cusp ∈ MulAction.orbit (↥Γ) D'.cusp

Two cusp data represent the same cusp orbit exactly when their cusps are Γ-equivalent.

theorem Subgroup.CuspDatum.mem_stabilizer_iff {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) {g : ↥Γ} : g ∈ MulAction.stabilizer (↥Γ) D.cusp ↔ ∃ (n : ℤ), D.generator ^ n = g

The stabilizer of the cusp consists of the integer powers of the selected generator.

@[simp]

theorem Subgroup.CuspDatum.scaling_mul_generator_zpow_mul_inv {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (n : ℤ) : D.scaling * ↑D.generator ^ n * D.scaling⁻¹ = Matrix.ProjectiveSpecialLinearGroup.upperRightHom (↑n * D.width)

Conjugation by the scaling sends the n-th power of the generator to translation by n * width.

@[simp]

theorem Subgroup.CuspDatum.orderOf_generator_eq_zero {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) : orderOf D.generator = 0

The selected generator of the stabilizer of a cusp has infinite order: for n ≠ 0, its n-th power is conjugate to translation by n * width ≠ 0.

theorem Subgroup.CuspDatum.mem_stabilizer_iff_conj {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) {g : ↥Γ} : g ∈ MulAction.stabilizer (↥Γ) D.cusp ↔ ∃ (n : ℤ), D.scaling * ↑g * D.scaling⁻¹ = Matrix.ProjectiveSpecialLinearGroup.upperRightHom (↑n * D.width)

The conjugated cusp stabilizer is width * ℤ. An element of Γ fixes the cusp exactly when its conjugate by the scaling is translation by an integer multiple of the width.

theorem Subgroup.CuspDatum.ext {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {D D' : Γ.CuspDatum} (hc : D.cusp = D'.cusp) (hσ : D.scaling = D'.scaling) : D = D'

Uniqueness of normalized cusp data. A cusp datum is determined by its cusp and its scaling: the width is then the positive generator of the conjugated stabilizer, and the generator is the corresponding element of Γ.

theorem Subgroup.CuspDatum.ext_iff {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {D D' : Γ.CuspDatum} : D = D' ↔ D.cusp = D'.cusp ∧ D.scaling = D'.scaling

@[simp]

theorem Subgroup.cuspOrbitMap_cuspOrbit {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (D : Δ.CuspDatum) : cuspOrbitMap h D.cuspOrbit = cuspOrbitMk ⟨D.cusp, ⋯⟩

Enlarging the subgroup sends a normalized cusp datum to the orbit of its cusp point.

theorem Subgroup.cuspOrbitMap_cuspOrbit_eq_of_cusp_eq {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) {D : Δ.CuspDatum} {E : Γ.CuspDatum} (hc : E.cusp = D.cusp) : cuspOrbitMap h D.cuspOrbit = E.cuspOrbit

Cusp data with the same boundary point have corresponding cusp orbits under inclusion.

theorem Subgroup.IsCuspPoint.exists_cuspDatum {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] {c : OnePoint ℝ} (hc : Γ.IsCuspPoint c) {σ : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} (hσ : σ • c = OnePoint.infty) : ∃ (D : Γ.CuspDatum), D.cusp = c ∧ D.scaling = σ

Existence of normalized cusp data. Let Γ ≤ PSL(2, ℝ) be discrete and c a cusp point of Γ. For every σ ∈ PSL(2, ℝ) with σ • c = ∞ there is a cusp datum with cusp c and scaling σ: the stabilizer of c in Γ is infinite cyclic, generated by an element that σ conjugates to a positive translation.

theorem Subgroup.IsCuspPoint.exists_cuspDatum_cusp_eq {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] {c : OnePoint ℝ} (hc : Γ.IsCuspPoint c) : ∃ (D : Γ.CuspDatum), D.cusp = c

Every cusp point of a discrete subgroup of PSL(2, ℝ) is the cusp of a cusp datum.

theorem Subgroup.CuspDatum.cuspOrbit_surjective {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] : Function.Surjective cuspOrbit

Every cusp orbit of a discrete subgroup of PSL(2, ℝ) is represented by a cusp datum.

noncomputable def Subgroup.CuspOrbit.cuspDatum {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] (C : Γ.CuspOrbit) : Γ.CuspDatum

A chosen normalized cusp datum representing a cusp orbit of a discrete group.

Equations

• C.cuspDatum = ⋯.choose

@[simp]

theorem Subgroup.CuspOrbit.cuspOrbit_cuspDatum {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] (C : Γ.CuspOrbit) : C.cuspDatum.cuspOrbit = C