Ideal vertex stabilizers and orbits of a fundamental polygon

Let σ pair the sides of a convex hyperbolic polygon P, and let Γ contain the side-pairing maps, and suppose distinct translates of its interior are disjoint. At an ideal vertex with parabolic cycle transformation, the full stabilizer is generated by that transformation. In particular, the cycle transformation is primitive in the stabilizer, not merely a nonzero power of its generator. Local finiteness of the translates supplies the parabolic hypothesis via ConvexPolygon.SidePairing.isParabolic_cycleMap_of_locallyFinite.

For a vertex with parabolic cycle transformation, another ideal vertex is Γ-equivalent to it exactly when it lies in the same side-pairing cycle. These results identify the parabolic ideal cycles with the boundary orbits meeting their vertices; exhaustion of all cusp orbits is a separate assertion. IdealVertexCycle is the same-cycle quotient of the ideal vertices.

The normal form for an element identifying two ideal vertices is a partial cycle product, followed by an integer power of the cycle transformation. It comes from the horodisc covered by the cycle tiles: the interior of any tile incident to the vertex meets that horodisc, and interior disjointness identifies it with one of the cycle tiles.

The stabilizer membership and orbit equivalences can be used with simp only after supplying their polygon hypotheses explicitly. They are not global simplification rules: their left-hand sides do not determine the polygon, side pairing, or vertex indices.

References

• Alan Beardon, The Geometry of Discrete Groups, Chapter 9 (vertex cycles of fundamental polygons).
• Svetlana Katok, Fuchsian Groups, Chapters 3--4 (parabolic cycles and cusp stabilizers).

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.exists_partialCycleMap_mul_zpow_eq_of_smul_idealVertex_eq {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {j l : Fin n} {ξ η : OnePoint ℝ} (hj : P.vertex j = Sum.inr ξ) (hl : P.vertex l = Sum.inr η) (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) (hpar : (σ.cycleMap j).IsParabolic) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) {g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} (hg : g ∈ Γ) (hgξ : g • ξ = η) : ∃ m < σ.cycleLength j, ∃ (k : ℤ), σ.partialCycleMap j m * σ.cycleMap j ^ k = g ∧ (⇑σ.next)^[m] j = l

Every transformation identifying two ideal vertices of a polygon with disjoint translated interiors is a partial cycle product followed by a power of the cycle transformation at the first vertex, provided the cycle transformation is parabolic. The partial product uses fewer than one cycle's worth of side pairings.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.smul_eq_self_iff_mem_zpowers_cycleMap_of_vertex_eq_inr {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {j : Fin n} {ξ : OnePoint ℝ} (hj : P.vertex j = Sum.inr ξ) (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) (hpar : (σ.cycleMap j).IsParabolic) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) {g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} (hg : g ∈ Γ) : g • ξ = ξ ↔ g ∈ Subgroup.zpowers (σ.cycleMap j)

An element of the acting group fixes an ideal vertex exactly when it is an integer power of that vertex's cycle transformation. Thus the parabolic cycle transformation is primitive in the full stabilizer.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.map_stabilizer_eq_zpowers_cycleMap_of_vertex_eq_inr {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {j : Fin n} {ξ : OnePoint ℝ} (hj : P.vertex j = Sum.inr ξ) (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) (hpar : (σ.cycleMap j).IsParabolic) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) : Subgroup.map Γ.subtype (MulAction.stabilizer (↥Γ) ξ) = Subgroup.zpowers (σ.cycleMap j)

The full stabilizer of an ideal vertex, viewed in PSL(2, ℝ), is generated by its cycle transformation, not by a proper root of that transformation.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.mem_orbit_iff_mem_cycle_of_vertex_eq_inr {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {j l : Fin n} {ξ η : OnePoint ℝ} (hj : P.vertex j = Sum.inr ξ) (hl : P.vertex l = Sum.inr η) (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) (hpar : (σ.cycleMap j).IsParabolic) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) : η ∈ MulAction.orbit (↥Γ) ξ ↔ l ∈ σ.cycle j

Two ideal vertices represent the same boundary orbit exactly when their indices belong to the same side-pairing cycle.

@[reducible, inline]

abbrev TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.IdealVertexCycle {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) : Type

The same-cycle quotient of the ideal vertices. It is independent of the ambient subgroup and of the fundamental-polygon hypotheses; for a locally finite fundamental polygon it is identified with the cusp orbits in ConvexPolygon.SidePairing.idealVertexCycleEquiv.