Cusp points and cusp orbits of a projective subgroup

A cusp point of a subgroup Γ ≤ PSL(2, ℝ) is a point of the projective boundary fixed by a parabolic element of Γ. Parabolicity is invariant under conjugation, so the cusp points form an invariant subspace of OnePoint ℝ. A cusp orbit is an orbit in the full projective boundary whose representatives are cusp points.

The cusp-orbit carrier is deliberately a subtype of the boundary orbit space. This makes it the literal collection of boundary orbits that will be adjoined to a Fuchsian quotient during cusp compactification. It is canonically equivalent to the quotient of the invariant subspace of cusp points, and Subgroup.cuspOrbitEquivQuotientCuspPoints records that comparison.

This construction is the effective-projective analogue of Mathlib's IsCusp, cuspsSubMulAction, and CuspOrbits for subgroups of GL(2, ℝ).

Main declarations

• Subgroup.IsCuspPoint: a projective boundary point fixed by a parabolic element of Γ.
• Subgroup.cuspPoints: the invariant subspace of cusp points.
• Subgroup.BoundaryOrbit: the orbit space of Γ on the full projective boundary.
• Subgroup.CuspOrbit: the subtype of boundary orbits represented by cusp points.
• Subgroup.cuspOrbitEquivQuotientCuspPoints: the identification with the quotient of Subgroup.cuspPoints.

References

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

def Subgroup.IsCuspPoint (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) (c : OnePoint ℝ) : Prop

A point of the projective boundary is a cusp point of Γ ≤ PSL(2, ℝ) when it is fixed by a parabolic element of Γ.

Equations

• Γ.IsCuspPoint c = ∃ (g : ↥Γ), (↑g).IsParabolic ∧ g • c = c

theorem Subgroup.isCuspPoint_iff_exists_parabolicFixedPoint_eq {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {c : OnePoint ℝ} : Γ.IsCuspPoint c ↔ ∃ (g : ↥Γ), (↑g).IsParabolic ∧ (↑g).parabolicFixedPoint = c

A point is a cusp point exactly when it is the unique fixed point of a parabolic element of Γ.

theorem Subgroup.isCuspPoint_iff_exists_mem_stabilizer_isParabolic {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {c : OnePoint ℝ} : Γ.IsCuspPoint c ↔ ∃ g ∈ MulAction.stabilizer (↥Γ) c, (↑g).IsParabolic

A point is a cusp point exactly when its stabilizer in Γ contains a parabolic element.

theorem Subgroup.IsCuspPoint.exists_ne_one_mem_stabilizer {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {c : OnePoint ℝ} (hc : Γ.IsCuspPoint c) : ∃ (g : ↥Γ), g ≠ 1 ∧ g ∈ MulAction.stabilizer (↥Γ) c ∧ (↑g).IsParabolic

Every cusp stabilizer contains a nonidentity parabolic element.

theorem Subgroup.IsCuspPoint.mono {Γ Δ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {c : OnePoint ℝ} (hΓΔ : Γ ≤ Δ) (hc : Γ.IsCuspPoint c) : Δ.IsCuspPoint c

A cusp point for a subgroup remains a cusp point after enlarging the subgroup.

theorem Subgroup.IsCuspPoint.smul {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {c : OnePoint ℝ} (hc : Γ.IsCuspPoint c) (g : ↥Γ) : Γ.IsCuspPoint (g • c)

The image of a cusp point under an element of Γ is again a cusp point.

@[simp]

theorem Subgroup.isCuspPoint_smul_iff {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (g : ↥Γ) (c : OnePoint ℝ) : Γ.IsCuspPoint (g • c) ↔ Γ.IsCuspPoint c

Cusp-point membership is invariant under the action of Γ.

def Subgroup.cuspPoints (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) : SubMulAction (↥Γ) (OnePoint ℝ)

The cusp points of Γ, as an invariant subspace of the projective boundary.

Equations

• Γ.cuspPoints = { carrier := {c : OnePoint ℝ | Γ.IsCuspPoint c}, smul_mem' := ⋯ }

@[simp]

theorem Subgroup.mem_cuspPoints {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {c : OnePoint ℝ} : c ∈ Γ.cuspPoints ↔ Γ.IsCuspPoint c

@[reducible, inline]

abbrev Subgroup.BoundaryOrbit (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) : Type

The orbit space of Γ on the full projective boundary.

Equations

• Γ.BoundaryOrbit = MulAction.orbitRel.Quotient (↥Γ) (OnePoint ℝ)

def Subgroup.IsCuspOrbit (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) (C : Γ.BoundaryOrbit) : Prop

A boundary orbit is a cusp orbit when one, equivalently every, representative is a cusp point.

Equations

• Γ.IsCuspOrbit C = ∃ (c : OnePoint ℝ), Γ.IsCuspPoint c ∧ Quotient.mk'' c = C

@[simp]

theorem Subgroup.isCuspOrbit_mk_iff {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (c : OnePoint ℝ) : Γ.IsCuspOrbit (Quotient.mk'' c) ↔ Γ.IsCuspPoint c

The orbit of a boundary point is a cusp orbit exactly when that point is a cusp point.

@[reducible, inline]

abbrev Subgroup.CuspOrbit (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) : Type

The cusp orbits of Γ, as the subtype of its boundary orbits represented by cusp points.

Equations

• Γ.CuspOrbit = { C : Γ.BoundaryOrbit // Γ.IsCuspOrbit C }

noncomputable def Subgroup.cuspOrbitMk {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (c : ↥Γ.cuspPoints) : Γ.CuspOrbit

The cusp orbit represented by a cusp point.

Equations

• Subgroup.cuspOrbitMk c = ⟨Quotient.mk'' ↑c, ⋯⟩

@[simp]

theorem Subgroup.cuspOrbitMk_val {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (c : ↥Γ.cuspPoints) : ↑(cuspOrbitMk c) = Quotient.mk'' ↑c

theorem Subgroup.cuspOrbitMk_eq_iff {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (c d : ↥Γ.cuspPoints) : cuspOrbitMk c = cuspOrbitMk d ↔ ↑c ∈ MulAction.orbit ↥Γ ↑d

Two cusp points represent the same cusp orbit exactly when they lie in the same Γ-orbit.

noncomputable def Subgroup.cuspOrbitEquivQuotientCuspPoints (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) : Γ.CuspOrbit ≃ MulAction.orbitRel.Quotient ↥Γ ↥Γ.cuspPoints

The subtype of cusp orbits in the full boundary quotient is canonically equivalent to the orbit quotient of the invariant subspace of cusp points.

Equations

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

@[simp]

theorem Subgroup.cuspOrbitEquivQuotientCuspPoints_cuspOrbitMk {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (c : ↥Γ.cuspPoints) : Γ.cuspOrbitEquivQuotientCuspPoints (cuspOrbitMk c) = Quotient.mk'' c

theorem Subgroup.cuspOrbitMk_surjective {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} : Function.Surjective cuspOrbitMk

Every cusp orbit has a cusp-point representative.

noncomputable def Subgroup.cuspOrbitMap {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) : Δ.CuspOrbit → Γ.CuspOrbit

Inclusion of projective subgroups sends each cusp orbit to its orbit under the larger group.

Equations

• Subgroup.cuspOrbitMap h = Subtype.map (Setoid.map_of_le ⋯) ⋯

@[simp]

theorem Subgroup.cuspOrbitMap_val {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (C : Δ.CuspOrbit) : ↑(cuspOrbitMap h C) = Setoid.map_of_le ⋯ ↑C

@[simp]

theorem Subgroup.cuspOrbitMap_cuspOrbitMk {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (c : ↥Δ.cuspPoints) : cuspOrbitMap h (cuspOrbitMk c) = cuspOrbitMk ⟨↑c, ⋯⟩

@[simp]

theorem Subgroup.cuspOrbitMap_self {Δ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} : cuspOrbitMap ⋯ = id

The cusp-orbit map for a reflexive inclusion is the identity.

@[simp]

theorem Subgroup.cuspOrbitMap_cuspOrbitMap {Δ Γ Θ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (k : Γ ≤ Θ) (C : Δ.CuspOrbit) : cuspOrbitMap k (cuspOrbitMap h C) = cuspOrbitMap ⋯ C

Two subgroup inclusions induce the map for their composite on each cusp orbit.

theorem Subgroup.cuspOrbitMap_comp {Δ Γ Θ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (k : Γ ≤ Θ) : cuspOrbitMap k ∘ cuspOrbitMap h = cuspOrbitMap ⋯

Cusp-orbit maps compose along a tower of subgroup inclusions.

theorem Subgroup.countable_setOf_isCuspPoint (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) [Countable ↥Γ] : {c : OnePoint ℝ | Γ.IsCuspPoint c}.Countable

The cusp points of a countable subgroup form a countable set: each is the fixed point of one of its parabolic elements.

instance Subgroup.instCountableCuspPoints (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) [Countable ↥Γ] : Countable ↥Γ.cuspPoints

instance Subgroup.instCountableCuspOrbit (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) [Countable ↥Γ] : Countable Γ.CuspOrbit

A countable subgroup of PSL(2, ℝ) has countably many cusp orbits.