Local polygon pieces around a vertex cycle

Following the side pairings from vertex j transports it to next^[m] j by partialCycleMap j m. Pulling the polygon at that vertex back by the inverse partial product therefore gives a tile meeting the original vertex. Near a finite vertex, any finite union of these tiles agrees with the union of their pulled-back vertex sectors. In particular, the sector union contains a neighbourhood exactly when the tile union does. This reduces local vertex coverage to the angular geometry of the incident sectors, without assuming a cycle angle condition or coverage.

Consecutive sectors lie on opposite sides of their common supporting geodesic. The construction allows partial products extending beyond a full cycle, as needed when several circuits are required around an elliptic vertex.

In the common coordinate at a finite vertex, consecutive pulled-back sectors share a boundary ray and turn clockwise by the successive interior angles. Once these angles add up to at least 2π the sectors cover all of ℍ, so the tiles cover a neighbourhood of the vertex. This is the local tessellation at a finite vertex in Poincaré's polygon theorem; for a cycle it applies after t circuits whenever t times the angle sum is at least 2π, in particular for an elliptic cycle with angle sum 2π / t.

Conversely, while the angles add up to at most 2π, the pulled-back sectors turn through at most a full circle, so their interiors, and hence the interiors of the tiles, are pairwise disjoint; in particular the partial cycle maps involved are distinct. For an elliptic cycle with angle sum 2π / t, the tiles met along t circuits therefore cover a neighbourhood of the vertex without overlapping. This local no-overlap at finite vertices is needed to derive, from the cycle conditions alone, that the translates of the polygon have disjoint interiors.

Main results

• SidePairing.mem_interior_iUnion_inv_partialCycleMap_smul_carrier_iff: the tiles cover a neighbourhood of a finite vertex exactly when their pulled-back sectors do.
• SidePairing.orientedAngle_rayToward_inv_partialCycleMap_smul_vertex: in the common coordinate at a finite vertex, the incoming ray of the m-th tile has turned clockwise through the first m angles.
• SidePairing.arg_smulDeriv_cycleMap: the rotation angle of a finite vertex cycle is its angle sum modulo 2π.
• SidePairing.iUnion_inv_partialCycleMap_smul_vertexSector_eq_univ: sectors with total angle at least 2π cover ℍ.
• SidePairing.mem_interior_iUnion_inv_partialCycleMap_smul_carrier_of_le_mul_cycleAngleSum: t circuits of a finite vertex cycle with total angle at least 2π cover a neighbourhood of the vertex.
• SidePairing.pairwiseDisjoint_inv_partialCycleMap_smul_interior_vertexSector, SidePairing.pairwiseDisjoint_inv_partialCycleMap_smul_interior_carrier: pulled-back sectors and tiles with total angle at most 2π have pairwise disjoint interiors.
• SidePairing.injOn_partialCycleMap: the corresponding partial cycle maps are distinct.
• SidePairing.pairwiseDisjoint_inv_partialCycleMap_smul_interior_carrier_of_mul_cycleAngleSum_le: t circuits of a finite vertex cycle with total angle at most 2π give tiles with pairwise disjoint interiors.

References

Beardon, The Geometry of Discrete Groups, Chapter 9. Walkden, Hyperbolic geometry, §§17 and 19–20 (vertex cycles and the local tessellation in Poincaré's polygon theorem).

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.inv_map_smul_vertexSector_next_subset_closure_rightHalfPlane {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) : (σ.map j)⁻¹ • P.vertexSector (σ.next j) ⊆ closure (rightHalfPlane (P.sideGeodesic j))

Successive pulled-back sectors are separated by the supporting geodesic of the side leaving the current vertex.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.disjoint_inv_map_smul_vertexSector_next_interior_vertexSector {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) : Disjoint ((σ.map j)⁻¹ • P.vertexSector (σ.next j)) (interior (P.vertexSector j))

The interiors of consecutive vertex sectors are disjoint, including when a side is paired with itself.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.disjoint_inv_partialCycleMap_smul_vertexSector_succ_interior {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (j : Fin n) (m : ℕ) : Disjoint ((σ.partialCycleMap j (m + 1))⁻¹ • P.vertexSector ((⇑σ.next)^[m + 1] j)) ((σ.partialCycleMap j m)⁻¹ • interior (P.vertexSector ((⇑σ.next)^[m] j)))

In the common coordinate at the initial vertex, each sector misses the interior of the preceding sector. This is adjacent-sector separation, without a claim about nonadjacent sectors.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.inv_partialCycleMap_smul_vertex {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {z : UpperHalfPlane} (hz : P.vertex j = Sum.inl z) (m : ℕ) : ((σ.partialCycleMap j m)⁻¹ • P).vertex ((⇑σ.next)^[m] j) = Sum.inl z

The tile at step m of a cycle through a finite vertex z has z as its vertex.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.eventuallyEq_inv_partialCycleMap_smul_carrier_vertexSector {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {z : UpperHalfPlane} (hz : P.vertex j = Sum.inl z) (m : ℕ) : (σ.partialCycleMap j m)⁻¹ • P.carrier =ᶠ[nhds z] (σ.partialCycleMap j m)⁻¹ • P.vertexSector ((⇑σ.next)^[m] j)

Near the initial finite vertex, every tile in a vertex cycle equals its pulled-back sector. This holds also for partial products extending beyond one circuit.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.eventuallyEq_iUnion_inv_partialCycleMap_smul_carrier_vertexSector {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {z : UpperHalfPlane} (hz : P.vertex j = Sum.inl z) (r : ℕ) : ⋃ m ∈ Finset.range r, (σ.partialCycleMap j m)⁻¹ • P.carrier =ᶠ[nhds z] ⋃ m ∈ Finset.range r, (σ.partialCycleMap j m)⁻¹ • P.vertexSector ((⇑σ.next)^[m] j)

A finite fan of tiles along a vertex cycle locally equals its fan of sectors.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.mem_interior_iUnion_inv_partialCycleMap_smul_carrier_iff {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {z : UpperHalfPlane} (hz : P.vertex j = Sum.inl z) (r : ℕ) : z ∈ interior (⋃ m ∈ Finset.range r, (σ.partialCycleMap j m)⁻¹ • P.carrier) ↔ z ∈ interior (⋃ m ∈ Finset.range r, (σ.partialCycleMap j m)⁻¹ • P.vertexSector ((⇑σ.next)^[m] j))

The cycle tiles cover a neighbourhood of a finite vertex if and only if their sectors cover one. No angular coverage is assumed in deriving this equivalence.

Coverage of a neighbourhood of a finite vertex

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.orientedAngle_rayToward_inv_partialCycleMap_smul_vertex {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {z : UpperHalfPlane} (hz : P.vertex j = Sum.inl z) (m : ℕ) : z.orientedAngle (geodesicLine (z.rayToward (P.vertex (j - 1))) 1) (geodesicLine (z.rayToward (((σ.partialCycleMap j m)⁻¹ • P).vertex ((⇑σ.next)^[m] j - 1))) 1) = ↑(-∑ l ∈ Finset.range m, P.interiorAngle ((⇑σ.next)^[l] j))

In the common coordinate at a finite vertex, the incoming ray of the m-th tile is reached from the incoming ray of the first tile by turning clockwise through the first m angles.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.orientedAngle_rayToward_inv_partialCycleMap_smul_vertex_add_one_left {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {z : UpperHalfPlane} (hz : P.vertex j = Sum.inl z) (m : ℕ) (w : UpperHalfPlane) : z.orientedAngle (geodesicLine (z.rayToward (((σ.partialCycleMap j m)⁻¹ • P).vertex ((⇑σ.next)^[m] j + 1))) 1) w = z.orientedAngle (geodesicLine (z.rayToward (P.vertex (j - 1))) 1) w + ↑(∑ l ∈ Finset.range (m + 1), P.interiorAngle ((⇑σ.next)^[l] j))

In the common coordinate at a finite vertex, the angle of w measured from the outgoing ray of the m-th tile is its angle measured from the incoming ray of the first tile, plus the first m + 1 angles.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.arg_smulDeriv_cycleMap {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {z : UpperHalfPlane} (hz : P.vertex j = Sum.inl z) : ↑((σ.cycleMap j).smulDeriv z).arg = ↑(σ.cycleAngleSum j)

The cycle transformation at a finite vertex rotates its tangent space counterclockwise through the cycle angle sum, modulo 2π. This does not require discreteness or no-overlap.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.iUnion_inv_partialCycleMap_smul_vertexSector_eq_univ {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {z : UpperHalfPlane} (hz : P.vertex j = Sum.inl z) {r : ℕ} (hr : 2 * Real.pi ≤ ∑ m ∈ Finset.range r, P.interiorAngle ((⇑σ.next)^[m] j)) : ⋃ m ∈ Finset.range r, (σ.partialCycleMap j m)⁻¹ • P.vertexSector ((⇑σ.next)^[m] j) = Set.univ

The vertex sectors along a cycle cover the plane once their angles reach 2π. Pull back the sectors of the vertices next^[m] j, m < r, to the finite vertex z = vertex j by the inverse partial cycle maps. If their interior angles sum to at least 2π, these sectors turn around z through a full circle, so their union is all of ℍ.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.mem_interior_iUnion_inv_partialCycleMap_smul_carrier {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {z : UpperHalfPlane} (hz : P.vertex j = Sum.inl z) {r : ℕ} (hr : 2 * Real.pi ≤ ∑ m ∈ Finset.range r, P.interiorAngle ((⇑σ.next)^[m] j)) : z ∈ interior (⋃ m ∈ Finset.range r, (σ.partialCycleMap j m)⁻¹ • P.carrier)

Local coverage at a finite vertex. If the interior angles at the first r vertices of the cycle through a finite vertex z = vertex j sum to at least 2π, then the pulled-back tiles (partialCycleMap j m)⁻¹ • P, m < r, cover a neighbourhood of z.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.mem_interior_iUnion_inv_partialCycleMap_smul_carrier_of_le_mul_cycleAngleSum {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {z : UpperHalfPlane} (hz : P.vertex j = Sum.inl z) {t : ℕ} (ht : 2 * Real.pi ≤ ↑t * σ.cycleAngleSum j) : z ∈ interior (⋃ m ∈ Finset.range (t * σ.cycleLength j), (σ.partialCycleMap j m)⁻¹ • P.carrier)

Local coverage at a finite vertex cycle. If t circuits of the cycle through a finite vertex z = vertex j have total angle at least 2π, then the tiles met along those circuits cover a neighbourhood of z. This is the case of an elliptic cycle whose angle sum is 2π / t in Poincaré's polygon theorem.

Disjointness of the tiles around a finite vertex

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.mem_inv_partialCycleMap_smul_interior_vertexSector_iff {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {z w : UpperHalfPlane} (hz : P.vertex j = Sum.inl z) (hw : z ≠ w) (m : ℕ) : w ∈ (σ.partialCycleMap j m)⁻¹ • interior (P.vertexSector ((⇑σ.next)^[m] j)) ↔ ∃ x ∈ Set.Ioo (∑ l ∈ Finset.range m, P.interiorAngle ((⇑σ.next)^[l] j)) (∑ l ∈ Finset.range (m + 1), P.interiorAngle ((⇑σ.next)^[l] j)), z.orientedAngle (geodesicLine (z.rayToward (P.vertex (j - 1))) 1) w = ↑(-x)

The interior of a pulled-back sector in the common coordinate. At a finite vertex z, a point w ≠ z is interior to the m-th pulled-back sector exactly when it lies clockwise of the incoming ray of the first tile by an angle strictly between the sums of the first m and the first m + 1 interior angles.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.pairwiseDisjoint_inv_partialCycleMap_smul_interior_vertexSector {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {z : UpperHalfPlane} (hz : P.vertex j = Sum.inl z) {r : ℕ} (hr : ∑ m ∈ Finset.range r, P.interiorAngle ((⇑σ.next)^[m] j) ≤ 2 * Real.pi) : (↑(Finset.range r)).PairwiseDisjoint fun (m : ℕ) => (σ.partialCycleMap j m)⁻¹ • interior (P.vertexSector ((⇑σ.next)^[m] j))

The vertex sectors along a cycle do not overlap while their angles stay within 2π. Pull back the sectors of the vertices next^[m] j, m < r, to the finite vertex z = vertex j by the inverse partial cycle maps. If their interior angles sum to at most 2π, these sectors turn around z through at most a full circle, so their interiors are pairwise disjoint.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.pairwiseDisjoint_inv_partialCycleMap_smul_interior_carrier {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {z : UpperHalfPlane} (hz : P.vertex j = Sum.inl z) {r : ℕ} (hr : ∑ m ∈ Finset.range r, P.interiorAngle ((⇑σ.next)^[m] j) ≤ 2 * Real.pi) : (↑(Finset.range r)).PairwiseDisjoint fun (m : ℕ) => (σ.partialCycleMap j m)⁻¹ • interior P.carrier

Local no-overlap at a finite vertex. If the interior angles at the first r vertices of the cycle through a finite vertex z = vertex j sum to at most 2π, then the pulled-back tiles (partialCycleMap j m)⁻¹ • P, m < r, have pairwise disjoint interiors.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.injOn_partialCycleMap {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {z : UpperHalfPlane} (hz : P.vertex j = Sum.inl z) {r : ℕ} (hr : ∑ m ∈ Finset.range r, P.interiorAngle ((⇑σ.next)^[m] j) ≤ 2 * Real.pi) : Set.InjOn (σ.partialCycleMap j) ↑(Finset.range r)

The tiles around a finite vertex are distinct while their angles stay within 2π: the partial cycle maps partialCycleMap j m, m < r, are pairwise distinct when the interior angles at the first r vertices of the cycle sum to at most 2π.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.pairwiseDisjoint_inv_partialCycleMap_smul_interior_carrier_of_mul_cycleAngleSum_le {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {z : UpperHalfPlane} (hz : P.vertex j = Sum.inl z) {t : ℕ} (ht : ↑t * σ.cycleAngleSum j ≤ 2 * Real.pi) : (↑(Finset.range (t * σ.cycleLength j))).PairwiseDisjoint fun (m : ℕ) => (σ.partialCycleMap j m)⁻¹ • interior P.carrier

Local no-overlap at a finite vertex cycle. If t circuits of the cycle through a finite vertex z = vertex j have total angle at most 2π, then the tiles met along those circuits have pairwise disjoint interiors. For an elliptic cycle whose angle sum is 2π / t, these tiles also cover a neighbourhood of z, by mem_interior_iUnion_inv_partialCycleMap_smul_carrier_of_le_mul_cycleAngleSum.