Finite vertex cycles are vertex orbits

Let σ pair the sides of a convex hyperbolic polygon P, and let Γ contain its side-pairing maps, with distinct translates of the interior disjoint. Two finite vertices of P are Γ-equivalent exactly when their indices lie in the same vertex cycle. More precisely, every transformation identifying two finite vertices is one of the partial cycle products met during one full turn about the first vertex.

Together with the vertex stabilizer theorem, this identifies the finite vertex cycles and their cycle orders with the corresponding orbits and stabilizer orders in the coarse quotient. It does not assert that every elliptic orbit meets a vertex: a self-paired side can also have an elliptic midpoint. FiniteVertexCycle is the type of finite vertex cycles, counted vertex by vertex in natCard_finiteVertexCycle_eq_sum, and EllipticVertexCycle restricts the finite cycles to those with nonidentity cycle transformation. Neither discreteness nor local finiteness is needed for the finite vertex result.

References

• Alan Beardon, The Geometry of Discrete Groups, Chapter 9 (vertex cycles of a fundamental polygon).
• Svetlana Katok, Fuchsian Groups, Chapter 3 (side identifications and elliptic cycles).

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.mem_orbit_iff_mem_cycle {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {j k : Fin n} {z w : UpperHalfPlane} (hz : P.vertex j = Sum.inl z) (hw : P.vertex k = Sum.inl w) (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) : w ∈ MulAction.orbit (↥Γ) z ↔ k ∈ σ.cycle j

Two finite vertices of a polygon with disjoint translated interiors represent the same group orbit exactly when they lie in the same side-pairing cycle.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.finiteVertex_quotientMk_eq_quotientMk_iff_sameCycle {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) (j k : { i : Fin n // (P.vertex i).isLeft = true }) : Quotient.mk'' ((P.vertex ↑j).getLeft ⋯) = Quotient.mk'' ((P.vertex ↑k).getLeft ⋯) ↔ σ.next.SameCycle ↑j ↑k

On the finite vertices, the orbit relation is exactly the cycle relation. This also applies to cycles with trivial vertex stabilizer.

@[reducible, inline]

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

The same-cycle quotient of the finite vertices: the finite vertex cycles of σ, including those whose cycle transformation is the identity. It is independent of the ambient subgroup and of the fundamental-polygon hypotheses.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.natCard_finiteVertexCycle_eq_sum {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {K : Type u_1} [Semifield K] [CharZero K] : ↑(Nat.card σ.FiniteVertexCycle) = ∑ i : Fin n, if (P.vertex i).isLeft = true then 1 / ↑(σ.cycleLength i) else 0

The number of finite vertex cycles is the sum, over the finite vertices, of the inverse lengths of their cycles.

@[reducible, inline]

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

The same-cycle quotient of the finite vertices whose cycle transformation is nonidentity. It is independent of the ambient subgroup and of the fundamental-polygon hypotheses.

noncomputable def TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.finiteVertexCycleEquiv {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) : σ.FiniteVertexCycle ≃ ↑(Set.range fun (j : { i : Fin n // (P.vertex i).isLeft = true }) => Quotient.mk'' ((P.vertex ↑j).getLeft ⋯))

Finite vertex cycles correspond bijectively to the coarse quotient orbits meeting a finite vertex of P. The domain is Mathlib's same-cycle quotient, restricted to finite vertices; the codomain is the image of those vertices under the ordinary orbit projection. In particular, cycles of stabilizer order one are retained, and no assertion about elliptic side midpoints is made.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.finiteVertexCycleEquiv_apply {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hmap : ∀ (i : Fin n), σ.map i ∈ Γ) (hdisj : ∀ (γ : ↥Γ), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) (j : { i : Fin n // (P.vertex i).isLeft = true }) : ↑((σ.finiteVertexCycleEquiv hmap hdisj) (Quotient.mk'' j)) = Quotient.mk'' ((P.vertex ↑j).getLeft ⋯)

The finite-cycle bijection sends a vertex cycle to the actual orbit of its vertex.