Cusps and finite-index subgroups

A boundary point is parabolic for a finite-index subgroup exactly when it is parabolic for the larger group. A positive power of a parabolic element fixing the point lies in the smaller group. Consequently the two groups have the same cusp points, although their cusp orbit sets can differ. The fibre of the cusp-orbit map is therefore the full boundary-orbit fibre. This is the projective counterpart of Mathlib's IsCusp.of_isFiniteRelIndex for subgroups of GL(2, ℝ).

The positive-power argument follows Mathlib/NumberTheory/ModularForms/Cusps.lean, adapted to Tau Ceti's effective projective action and cusp-point carrier.

theorem Subgroup.IsCuspPoint.of_isFiniteRelIndex {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [Δ.IsFiniteRelIndex Γ] {c : OnePoint ℝ} (hc : Γ.IsCuspPoint c) : Δ.IsCuspPoint c

A cusp point of a group is a cusp point of every finite-index subgroup.

theorem Subgroup.isCuspPoint_iff_of_isFiniteRelIndex {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [Δ.IsFiniteRelIndex Γ] (h : Δ ≤ Γ) {c : OnePoint ℝ} : Δ.IsCuspPoint c ↔ Γ.IsCuspPoint c

Finite-index subgroups have exactly the cusp points of the containing group.

theorem Subgroup.isCuspOrbit_iff_of_isFiniteRelIndex {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [Δ.IsFiniteRelIndex Γ] (h : Δ ≤ Γ) (q : Δ.BoundaryOrbit) : Δ.IsCuspOrbit q ↔ Γ.IsCuspOrbit (Setoid.map_of_le ⋯ q)

A boundary orbit is a cusp orbit for a finite-index subgroup exactly when its image is a cusp orbit for the containing group.

theorem Subgroup.cuspOrbitMap_surjective {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [Δ.IsFiniteRelIndex Γ] (h : Δ ≤ Γ) : Function.Surjective (cuspOrbitMap h)

Every cusp orbit of the containing group has a cusp orbit above it for a finite-index inclusion.

def Subgroup.cuspOrbitFiberEquivBoundaryOrbitFiber {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [Δ.IsFiniteRelIndex Γ] (h : Δ ≤ Γ) (C : Γ.CuspOrbit) : { D : Δ.CuspOrbit // cuspOrbitMap h D = C } ≃ { q : Δ.BoundaryOrbit // Setoid.map_of_le ⋯ q = ↑C }

A cusp-orbit fibre is the full boundary-orbit fibre over the same cusp.

Equations

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

@[simp]

theorem Subgroup.cuspOrbitFiberEquivBoundaryOrbitFiber_apply {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [Δ.IsFiniteRelIndex Γ] (h : Δ ≤ Γ) (C : Γ.CuspOrbit) (D : { D : Δ.CuspOrbit // cuspOrbitMap h D = C }) : ↑((cuspOrbitFiberEquivBoundaryOrbitFiber h C) D) = ↑↑D

The boundary-orbit equivalence retains the underlying orbit.