Local finiteness of the translates of a compact convex polygon

Let Γ ≤ PSL(2, ℝ) act properly discontinuously on the upper half-plane, as every discrete subgroup does. The carrier of a compact convex hyperbolic polygon P is compact, so the family of translates {γ • P.carrier | γ ∈ Γ} is locally finite in the sense of Katok. The same holds for the translated sides and vertices, indexed by pairs (γ, i), since each lies in the corresponding translated carrier; and the union of the translates of the carrier is closed. Conversely, local finiteness of the carrier translates already implies that Γ is discrete. This is the discreteness step used when a polygon construction first produces a locally finite tessellation and only afterwards identifies its transformation group as Fuchsian.

Main results

• CompactConvexPolygon.locallyFinite_smul_carrier: the translates of the carrier are locally finite.
• CompactConvexPolygon.discreteTopology_of_locallyFinite_smul_carrier: local finiteness of the carrier translates implies discreteness of the acting subgroup.
• CompactConvexPolygon.locallyFinite_smul_side, CompactConvexPolygon.locallyFinite_singleton_smul_vertex: the translates of the sides, respectively of the vertices, are locally finite.
• CompactConvexPolygon.isClosed_iUnion_smul_carrier: the union of the translates of the carrier is closed.

These are the polygon cases of TauCeti.locallyFinite_smul_of_isCompact, LocallyFinite.comp_fst and TauCeti.isClosed_iUnion_smul_of_isCompact.

Source

Katok, Fuchsian groups, geodesic flows on surfaces of constant negative curvature and symbolic coding of geodesics, Clay Math. Proc. 10 (2010), Definition 8.2, p. 27 (locally finite family of subsets) and Definition 11.1, p. 37 (locally finite fundamental region: its tessellation {T(F) | T ∈ Γ} is locally finite).

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.discreteTopology_of_locallyFinite_smul_carrier {n : ℕ} [NeZero n] (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) (P : CompactConvexPolygon n) (hlocal : LocallyFinite fun (γ : ↥Γ) => ↑γ • P.carrier) : DiscreteTopology ↥Γ

A subgroup whose translates of a compact convex polygon are locally finite is discrete. This is the specialization of TauCeti.discreteTopology_of_locallyFinite_smul used for locally finite polygon tessellations.

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.locallyFinite_smul_carrier {n : ℕ} [NeZero n] (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) (P : CompactConvexPolygon n) [ProperlyDiscontinuousSMul (↥Γ) UpperHalfPlane] : LocallyFinite fun (γ : ↥Γ) => ↑γ • P.carrier

The translates of a compact convex polygon under a properly discontinuous Γ ≤ PSL(2, ℝ) are locally finite, in the sense of Katok, Definition 8.2, p. 27: every point has a neighbourhood meeting only finitely many of them.

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.locallyFinite_smul_side {n : ℕ} [NeZero n] (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) (P : CompactConvexPolygon n) [ProperlyDiscontinuousSMul (↥Γ) UpperHalfPlane] : LocallyFinite fun (p : ↥Γ × Fin n) => ↑p.1 • P.side p.2

The translates of the sides of a compact convex polygon under a properly discontinuous Γ ≤ PSL(2, ℝ), indexed by (γ, i) ∈ Γ × Fin n, are locally finite.

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.locallyFinite_singleton_smul_vertex {n : ℕ} [NeZero n] (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) (P : CompactConvexPolygon n) [ProperlyDiscontinuousSMul (↥Γ) UpperHalfPlane] : LocallyFinite fun (p : ↥Γ × Fin n) => {↑p.1 • P.vertex p.2}

The translates of the vertices of a compact convex polygon under a properly discontinuous Γ ≤ PSL(2, ℝ), as singletons indexed by (γ, i) ∈ Γ × Fin n, are locally finite.

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.isClosed_iUnion_smul_carrier {n : ℕ} [NeZero n] (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) (P : CompactConvexPolygon n) [ProperlyDiscontinuousSMul (↥Γ) UpperHalfPlane] : IsClosed (⋃ (γ : ↥Γ), ↑γ • P.carrier)

The union of the translates of a compact convex polygon under a properly discontinuous Γ ≤ PSL(2, ℝ) is closed.