The tessellation by a side-paired polygon with ideal vertices

Let σ be a side pairing of a convex hyperbolic polygon P, possibly with ideal vertices. Suppose that every finite vertex cycle satisfies the angle condition of Poincaré's polygon theorem, and that the cycle transformation of every ideal vertex is parabolic. This file proves that the group generated by the side-pairing maps then moves the interior of P off itself and has locally finite translates of P: these are the tessellation hypotheses from which the fundamental domain, discreteness, covolume and presentation statements for side-paired polygons are proved.

The local neighbours of the points of P form a local tiling (SidePairing.isLocalTiling), and the global tessellation theorem for local tilings applies once tiling charts of a uniform size exist. A compact polygon has them automatically; at an ideal vertex the charts at the points of P shrink towards the vertex, and a different chart is needed. Move the ideal vertex vertex j to ∞ by g, and let T be its cycle transformation. When T is parabolic, the tiles (T ^ k * (partialCycleMap j m)⁻¹) • P cover a horodisc {z | B < Im (g • z)} at the vertex (exists_setOf_lt_im_smul_subset_iUnion_smul_carrier), and have pairwise disjoint interiors. High enough in that horodisc, a point of a tile lies only on the two sides through the ideal vertex, and crossing such a side moves to the previous or the next tile of the cycle. So the horodisc with these tiles is a tiling chart (exists_isTilingChart_of_vertex_eq_inr). Since P minus horodiscs at its ideal vertices is compact, the charts at the points of this truncation, together with the horodisc charts, are uniform.

Conversely, the angle condition and the parabolic cycle condition hold at the vertices of every locally finite fundamental polygon, so for a side-paired polygon the tessellation hypotheses are equivalent to these cycle conditions.

Main results

• ConvexPolygon.SidePairing.exists_isTilingChart_of_vertex_eq_inr: a horodisc at an ideal vertex with parabolic cycle transformation, with the tiles of its cycle, is a tiling chart.
• ConvexPolygon.SidePairing.hasUniformTilingCharts_of_isParabolic: under the angle and parabolic cycle conditions, the local tiling by P has uniform tiling charts.
• ConvexPolygon.SidePairing.disjoint_smul_interior_carrier_of_isParabolic, ConvexPolygon.SidePairing.locallyFinite_smul_carrier_of_isParabolic: under these conditions, the group generated by the side-pairing maps has disjoint translates of the interior of P and locally finite translates of P.
• ConvexPolygon.SidePairing.disjoint_smul_interior_carrier_and_locallyFinite_iff: these tessellation properties are equivalent to the angle and parabolic cycle conditions.
• ConvexPolygon.SidePairing.disjoint_smul_interior_carrier_iff_of_isCompact: for a compact polygon, the translated interiors are disjoint exactly when the angle condition holds.

References

• Alan Beardon, The Geometry of Discrete Groups, Graduate Texts in Mathematics 91, Springer, 1983, §9.8 (Poincaré's theorem).
• Bernard Maskit, On Poincaré's theorem for fundamental polygons, Adv. Math. 7 (1971), 219–230.
• David B. A. Epstein and Carlo Petronio, An exposition of Poincaré's polyhedron theorem, Enseign. Math. (2) 40 (1994), 113–170.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.exists_isTilingChart_of_vertex_eq_inr {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (hcyc : ∀ (j : Fin n) (z : UpperHalfPlane), P.vertex j = Sum.inl z → ↑(orderOf (σ.cycleMap j)) * σ.cycleAngleSum j = 2 * Real.pi) {j : Fin n} {ξ : OnePoint ℝ} (hj : P.vertex j = Sum.inr ξ) (hpar : (σ.cycleMap j).IsParabolic) {g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} (hg : g • ξ = OnePoint.infty) : ∃ (A : ℝ), ∀ (B : ℝ), A < B → IsTilingChart P.carrier σ.localNeighbors {z : UpperHalfPlane | B < (g • z).im} (Set.range fun (p : ℤ × ℕ) => σ.cycleMap j ^ p.1 * (σ.partialCycleMap j p.2)⁻¹)

The tiling chart at an ideal vertex. Let vertex j = ξ be an ideal vertex whose cycle transformation T is parabolic, let g carry ξ to ∞, and let every finite vertex cycle satisfy the angle condition. Then above some height, every horodisc {z | B < Im (g • z)} at ξ is a tiling chart whose tiles are (T ^ k * (partialCycleMap j m)⁻¹) • P, for k ∈ ℤ and m ∈ ℕ.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.hasUniformTilingCharts_of_isParabolic {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (hcyc : ∀ (j : Fin n) (z : UpperHalfPlane), P.vertex j = Sum.inl z → ↑(orderOf (σ.cycleMap j)) * σ.cycleAngleSum j = 2 * Real.pi) (hpar : ∀ (j : Fin n) (ξ : OnePoint ℝ), P.vertex j = Sum.inr ξ → (σ.cycleMap j).IsParabolic) : HasUniformTilingCharts P.carrier σ.localNeighbors

Uniform tiling charts for a side-paired polygon. If every finite vertex cycle satisfies the angle condition and every ideal vertex cycle transformation is parabolic, then the local tiling by P has tiling charts of a uniform size.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.disjoint_smul_interior_carrier_of_isParabolic {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (hcyc : ∀ (j : Fin n) (z : UpperHalfPlane), P.vertex j = Sum.inl z → ↑(orderOf (σ.cycleMap j)) * σ.cycleAngleSum j = 2 * Real.pi) (hpar : ∀ (j : Fin n) (ξ : OnePoint ℝ), P.vertex j = Sum.inr ξ → (σ.cycleMap j).IsParabolic) (γ : ↥(Subgroup.closure (Set.range σ.map))) (hγ : γ ≠ 1) : Disjoint (↑γ • interior P.carrier) (interior P.carrier)

No overlap for a side-paired polygon. If every finite vertex cycle satisfies the angle condition and every ideal vertex cycle transformation is parabolic, then distinct translates of the interior of P by the group generated by the side-pairing maps are disjoint.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.locallyFinite_smul_carrier_of_isParabolic {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (hcyc : ∀ (j : Fin n) (z : UpperHalfPlane), P.vertex j = Sum.inl z → ↑(orderOf (σ.cycleMap j)) * σ.cycleAngleSum j = 2 * Real.pi) (hpar : ∀ (j : Fin n) (ξ : OnePoint ℝ), P.vertex j = Sum.inr ξ → (σ.cycleMap j).IsParabolic) : LocallyFinite fun (γ : ↥(Subgroup.closure (Set.range σ.map))) => ↑γ • P.carrier

Local finiteness for a side-paired polygon. If every finite vertex cycle satisfies the angle condition and every ideal vertex cycle transformation is parabolic, then the translates of P by the group generated by the side-pairing maps form a locally finite family.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.disjoint_smul_interior_carrier_and_locallyFinite_iff {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) : ((∀ (γ : ↥(Subgroup.closure (Set.range σ.map))), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) ∧ LocallyFinite fun (γ : ↥(Subgroup.closure (Set.range σ.map))) => ↑γ • P.carrier) ↔ (∀ (j : Fin n) (z : UpperHalfPlane), P.vertex j = Sum.inl z → ↑(orderOf (σ.cycleMap j)) * σ.cycleAngleSum j = 2 * Real.pi) ∧ ∀ (j : Fin n) (ξ : OnePoint ℝ), P.vertex j = Sum.inr ξ → (σ.cycleMap j).IsParabolic

The cycle conditions characterize the tessellation. The translates of a side-paired polygon P by the group generated by the side-pairing maps are locally finite with disjoint interiors if and only if every finite vertex cycle satisfies the angle condition and every ideal vertex cycle transformation is parabolic.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.disjoint_smul_interior_carrier_iff_of_isCompact {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (hc : IsCompact P.carrier) : (∀ (γ : ↥(Subgroup.closure (Set.range σ.map))), γ ≠ 1 → Disjoint (↑γ • interior P.carrier) (interior P.carrier)) ↔ ∀ (j : Fin n) (z : UpperHalfPlane), P.vertex j = Sum.inl z → ↑(orderOf (σ.cycleMap j)) * σ.cycleAngleSum j = 2 * Real.pi

The angle condition characterizes no overlap for a compact side-paired polygon. The translates of the interior of a compact polygon P by the group generated by the side-pairing maps are disjoint if and only if, at every vertex, the cycle transformation has finite order m and the interior angles along the cycle add up to 2π / m.