Separation across paired polygon sides

A side-pairing transformation reverses the endpoints of an oriented side while preserving the orientation of the upper half-plane. It therefore carries the left half-plane of that side to the right half-plane of the paired side. Consequently, the original polygon and its paired translate have disjoint interiors, and their intersection lies on the supporting geodesic of the paired side. The paired side itself belongs to their intersection. At every point of that side other than its finite endpoints, the two tiles together contain a neighbourhood: the strict inequalities for the other sides follow from convexity.

These are the separation facts for adjacent tiles in a polygon tessellation. They apply to finite and ideal vertices, and even to a side paired with itself. They require no discreteness or cycle hypotheses. Separation for arbitrary products of side-pairing transformations, and coverage by all translates, require additional hypotheses.

Main results

• ConvexPolygon.SidePairing.map_smul_leftHalfPlane: the supporting half-planes are exchanged.
• ConvexPolygon.SidePairing.disjoint_smul_carrier_interior_carrier: the paired translate misses the interior of the original polygon.
• ConvexPolygon.SidePairing.inter_smul_carrier_subset_range_sideGeodesic: intersections occur only on the supporting geodesic of the paired side.
• ConvexPolygon.SidePairing.mem_interior_union_smul_carrier: local coverage when the other side inequalities in both tiles are strict.
• ConvexPolygon.SidePairing.mem_interior_union_smul_carrier_of_mem_side: local coverage at every nonendpoint point of a paired side, with no additional inequalities assumed.

References

Walkden, Hyperbolic geometry (MATH32052 lecture notes, Manchester 2019), §16.1 (orientation of side pairings) and §§19–20 (Poincaré's theorem). Beardon, The Geometry of Discrete Groups, Chapter 9.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.map_smul_leftHalfPlane {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (i : Fin n) : σ.map i • leftHalfPlane (P.sideGeodesic i) = rightHalfPlane (P.sideGeodesic (σ.pair i))

The side-pairing map carries the left half-plane of the source side to the right half-plane of the paired side.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.map_smul_rightHalfPlane {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (i : Fin n) : σ.map i • rightHalfPlane (P.sideGeodesic i) = leftHalfPlane (P.sideGeodesic (σ.pair i))

The side-pairing map carries the right half-plane of the source side to the left half-plane of the paired side.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.smul_carrier_subset_closure_rightHalfPlane {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (i : Fin n) : σ.map i • P.carrier ⊆ closure (rightHalfPlane (P.sideGeodesic (σ.pair i)))

The paired translate of the polygon lies on the right of the paired side, including its supporting geodesic.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.disjoint_smul_carrier_interior_carrier {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (i : Fin n) : Disjoint (σ.map i • P.carrier) (interior P.carrier)

The paired translate misses the interior of the original polygon. This is stronger than separation of their two interiors.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.disjoint_smul_interior_carrier_carrier {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (i : Fin n) : Disjoint (σ.map i • interior P.carrier) P.carrier

The interior of the paired translate misses the entire original polygon.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.inter_smul_carrier_subset_range_sideGeodesic {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (i : Fin n) : P.carrier ∩ σ.map i • P.carrier ⊆ Set.range (geodesicLine (P.sideGeodesic (σ.pair i)))

The intersection of adjacent polygon carriers lies on the supporting geodesic of the paired side.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.side_subset_inter_smul_carrier {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (i : Fin n) : P.side (σ.pair i) ⊆ P.carrier ∩ σ.map i • P.carrier

The paired side lies in both the original polygon and its paired translate.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.mem_interior_union_smul_carrier {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (i : Fin n) {z : UpperHalfPlane} (hz : ∀ (j : Fin n), j ≠ σ.pair i → z ∈ leftHalfPlane (P.sideGeodesic j)) (hzinv : ∀ (j : Fin n), j ≠ i → (σ.map i)⁻¹ • z ∈ leftHalfPlane (P.sideGeodesic j)) : z ∈ interior (P.carrier ∪ σ.map i • P.carrier)

At a point satisfying all the other side inequalities strictly in both tiles, the polygon and its paired translate together contain a neighbourhood. In particular, this gives local coverage across a paired side away from any other supporting geodesic.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.mem_interior_union_smul_carrier_of_mem_side {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (i : Fin n) {z : UpperHalfPlane} (hz : z ∈ P.side (σ.pair i)) (hzp : P.vertex (σ.pair i) ≠ Sum.inl z) (hzq : P.vertex (σ.pair i + 1) ≠ Sum.inl z) : z ∈ interior (P.carrier ∪ σ.map i • P.carrier)

At every point of the paired side other than its finite endpoints, the two adjacent polygon tiles together contain a neighbourhood. No extra side inequalities are assumed.