The local tiling at a parabolic ideal vertex cycle

Let ξ be an ideal vertex of a side-paired convex polygon P. Following the side pairings from ξ pulls P back to tiles (partialCycleMap j m)⁻¹ • P, all having ξ as an ideal vertex. After moving ξ to ∞, each tile agrees, above some height, with a vertical strip, and consecutive strips share a vertical side (ConvexPolygon.SidePairing.inv_partialCycleMap_succ_smul_vertex_sub_one). After a full cycle the tile is moved by the cycle transformation, which fixes ξ.

If that cycle transformation is parabolic, it is conjugate to a translation, and the strips of one cycle exactly fill a period of it. Its integer powers then move these finitely many tiles so that they cover a whole horodisc at ξ. This is the local tessellation at an ideal vertex in Poincaré's polygon theorem, whose hypothesis at ideal cycles is exactly that their transformations are parabolic. Neither discreteness nor a fundamental-domain hypothesis is assumed.

Since the strips move strictly in one direction, the tiles met along the cycle have pairwise disjoint interiors, however often the cycle is traversed, and so do their translates by powers of the cycle transformation. Unlike at a finite vertex, no angle condition is involved. When the cycle transformation is parabolic, these tiles therefore tessellate a horodisc at the vertex.

An ideal cycle transformation is never the identity. It fixes a boundary point, so it is parabolic or hyperbolic. If a group containing it has locally finite translates of P, then it is parabolic (ConvexPolygon.isParabolic_of_smul_eq_self_of_locallyFinite). So the parabolic cycle condition holds at every ideal vertex of a locally finite fundamental polygon.

Main results

• ConvexPolygon.SidePairing.strictAnti_re_toComplex_smul_vertex_sub_one: in a coordinate moving an ideal vertex to ∞, the strips of its cycle move strictly to the left.
• SidePairing.pairwise_disjoint_inv_partialCycleMap_smul_interior_carrier_of_vertex_eq_inr: the tiles met along an ideal vertex cycle have pairwise disjoint interiors.
• ConvexPolygon.SidePairing.partialCycleMap_injective_of_vertex_eq_inr: the partial cycle maps at an ideal vertex are pairwise distinct.
• ConvexPolygon.SidePairing.cycleMap_ne_one_of_vertex_eq_inr: an ideal cycle transformation is not the identity.
• ConvexPolygon.SidePairing.isParabolic_cycleMap_of_locallyFinite: an ideal cycle transformation is parabolic when a group containing it has locally finite translates of P.
• ConvexPolygon.SidePairing.exists_pos_conj_cycleMap_eq_upperRightHom: the parabolic cycle transformation is a positive translation in every scaling sending its vertex to infinity.
• ConvexPolygon.SidePairing.exists_setOf_lt_im_smul_subset_iUnion_smul_carrier: at an ideal vertex with parabolic cycle transformation, the tiles of the cycle and their translates by powers of the cycle transformation cover a horodisc.
• SidePairing.pairwiseDisjoint_cycleMap_zpow_mul_inv_partialCycleMap_smul_interior_carrier: these tiles have pairwise disjoint interiors.

References

Beardon, The Geometry of Discrete Groups, Chapter 9. Walkden, Hyperbolic geometry (MATH32051 lecture notes, Manchester 2019), §§17.2 and 19–20 (parabolic cycles and the local tessellation in Poincaré's polygon theorem). Maskit, On Poincaré's theorem for fundamental polygons, Adv. Math. 7 (1971), 219–230.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.mul_inv_partialCycleMap_smul_vertex {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {ξ : OnePoint ℝ} (hj : P.vertex j = Sum.inr ξ) {g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} (hg : g • ξ = OnePoint.infty) (m : ℕ) : ((g * (σ.partialCycleMap j m)⁻¹) • P).vertex ((⇑σ.next)^[m] j) = Sum.inr OnePoint.infty

In a coordinate g moving an ideal vertex to ∞, every tile of its cycle has its corresponding vertex at ∞.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.strictAnti_re_toComplex_smul_vertex_sub_one {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {ξ : OnePoint ℝ} (hj : P.vertex j = Sum.inr ξ) {g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} (hg : g • ξ = OnePoint.infty) : StrictAnti fun (m : ℕ) => (toComplex ((g * (σ.partialCycleMap j m)⁻¹) • P.vertex ((⇑σ.next)^[m] j - 1))).re

The strips of an ideal cycle move strictly to the left. Let vertex j = ξ be ideal and let g carry ξ to ∞. In the coordinate g, the tile (partialCycleMap j m)⁻¹ • P is near ∞ the vertical strip ending on the right at the vertex before next^[m] j. The real part of that vertex strictly decreases with m.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.cycleMap_ne_one_of_vertex_eq_inr {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {ξ : OnePoint ℝ} (hj : P.vertex j = Sum.inr ξ) : σ.cycleMap j ≠ 1

An ideal cycle transformation is not the identity: going once around the cycle moves the strips of its tiles strictly to the left.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.pairwise_disjoint_inv_partialCycleMap_smul_interior_vertexSector_of_vertex_eq_inr {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {ξ : OnePoint ℝ} (hj : P.vertex j = Sum.inr ξ) : Pairwise (Function.onFun Disjoint fun (m : ℕ) => (σ.partialCycleMap j m)⁻¹ • interior (P.vertexSector ((⇑σ.next)^[m] j)))

The sectors of an ideal vertex cycle do not overlap. Pulling the sectors at the vertices of the cycle through an ideal vertex back along the partial cycle maps gives sectors at that vertex with pairwise disjoint interiors, however many times the cycle is traversed. Unlike at a finite vertex, no angle condition is needed: after moving the vertex to ∞, these interiors are open vertical strips moving strictly to the left.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.pairwise_disjoint_inv_partialCycleMap_smul_interior_carrier_of_vertex_eq_inr {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {ξ : OnePoint ℝ} (hj : P.vertex j = Sum.inr ξ) : Pairwise (Function.onFun Disjoint fun (m : ℕ) => (σ.partialCycleMap j m)⁻¹ • interior P.carrier)

The tiles of an ideal vertex cycle do not overlap. The tiles (partialCycleMap j m)⁻¹ • P obtained by following the side pairings from an ideal vertex have pairwise disjoint interiors, for all m.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.partialCycleMap_injective_of_vertex_eq_inr {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {ξ : OnePoint ℝ} (hj : P.vertex j = Sum.inr ξ) : Function.Injective (σ.partialCycleMap j)

The partial cycle maps at an ideal vertex are pairwise distinct.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.isParabolic_cycleMap_of_locallyFinite {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {ξ : OnePoint ℝ} (hj : P.vertex j = Sum.inr ξ) {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hT : σ.cycleMap j ∈ Γ) (hlf : LocallyFinite fun (γ : ↥Γ) => ↑γ • P.carrier) : (σ.cycleMap j).IsParabolic

Ideal cycle transformations of a locally finite tessellation are parabolic. If a subgroup Γ of PSL(2, ℝ) contains the cycle transformation at the ideal vertex vertex j and its translates of P form a locally finite family, then this cycle transformation is parabolic.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.exists_pos_conj_cycleMap_eq_upperRightHom {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {ξ : OnePoint ℝ} (hj : P.vertex j = Sum.inr ξ) (hpar : (σ.cycleMap j).IsParabolic) {g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} (hg : g • ξ = OnePoint.infty) : ∃ (w : ℝ), 0 < w ∧ g * σ.cycleMap j * g⁻¹ = Matrix.ProjectiveSpecialLinearGroup.upperRightHom w

In any scaling sending an ideal vertex to infinity, its parabolic cycle transformation is translation by a strictly positive amount. The sign is fixed by the side-pairing cycle order.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.exists_setOf_lt_im_smul_subset_iUnion_smul_carrier {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {ξ : OnePoint ℝ} (hj : P.vertex j = Sum.inr ξ) (hpar : (σ.cycleMap j).IsParabolic) {g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} (hg : g • ξ = OnePoint.infty) : ∃ (A : ℝ), {z : UpperHalfPlane | A < (g • z).im} ⊆ ⋃ (k : ℤ), ⋃ m ∈ Finset.range (σ.cycleLength j), (σ.cycleMap j ^ k * (σ.partialCycleMap j m)⁻¹) • P.carrier

The local tiling at a parabolic ideal vertex. Let vertex j = ξ be ideal with parabolic cycle transformation T, and let g carry ξ to ∞. Then above some height in the coordinate g, every point lies in a tile (T ^ k * (partialCycleMap j m)⁻¹) • P with k ∈ ℤ and m less than the cycle length. That is, these tiles cover a horodisc at ξ.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.pairwiseDisjoint_cycleMap_zpow_mul_inv_partialCycleMap_smul_interior_carrier {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {ξ : OnePoint ℝ} (hj : P.vertex j = Sum.inr ξ) : (Set.univ ×ˢ ↑(Finset.range (σ.cycleLength j))).PairwiseDisjoint fun (p : ℤ × ℕ) => (σ.cycleMap j ^ p.1 * (σ.partialCycleMap j p.2)⁻¹) • interior P.carrier

The local tiling at an ideal vertex has no overlaps. Let vertex j be ideal with cycle transformation T. The tiles (T ^ k * (partialCycleMap j m)⁻¹) • P, for k ∈ ℤ and m less than the cycle length, have pairwise disjoint interiors. When T is parabolic these tiles also cover a horodisc at the vertex (exists_setOf_lt_im_smul_subset_iUnion_smul_carrier), so they tessellate it.