The local tiling of a side-paired polygon

Let σ be a side pairing of a convex hyperbolic polygon P. Following the side pairings predicts the tiles around each point x of P: the polygon itself, its translate (map i)⁻¹ • P across each side i through x, and, at a finite vertex x = vertex j, the tiles (partialCycleMap j m)⁻¹ • P met by following the vertex cycle of j. These are the local neighbours σ.localNeighbors x.

Suppose that every finite vertex cycle satisfies the angle condition of Poincaré's polygon theorem: the order m of its cycle transformation is finite and the interior angles along the cycle add up to 2π / m. Then the local neighbours form a local tiling by P in the sense of TauCeti.IsLocalTiling. Along a side the polygon and its paired translate cover a neighbourhood, and around a finite vertex the tiles met during m circuits of the cycle fill a full turn without overlapping.

Ideal vertices impose no condition here: they are not points of the upper half-plane. They enter when the generic local tiling theorems are applied, which needs tiling charts of a uniform size; this is done in SidePairing/HorodiscChart.lean. Charts other than those at the points of P are built from sets of tiles with pairwise disjoint interiors, and a tile of such a set through a point h • v, v ∈ P, is a translated local neighbour of v as soon as the set contains all these translates (inv_mul_mem_localNeighbors_of_smul_mem).

Main definitions

• ConvexPolygon.SidePairing.localNeighbors: the local neighbours of a point.

Main results

• ConvexPolygon.SidePairing.localNeighbors_eq_range: at a finite vertex, the local neighbours are the inverse partial cycle products.
• ConvexPolygon.SidePairing.isLocalTiling: under the angle condition at the finite vertex cycles, the local neighbours form a local tiling by P.
• ConvexPolygon.SidePairing.closure_biUnion_localNeighbors: the local neighbours generate the group generated by the side-pairing maps.
• ConvexPolygon.SidePairing.inv_mul_mem_localNeighbors_of_smul_mem: a tile through a translated point of P, in a set of tiles with disjoint interiors containing the translated local neighbours, is a translated local neighbour.

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.

def TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.localNeighbors {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (x : UpperHalfPlane) : Set (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)

The local neighbours of a point x for the tiling by a side-paired polygon P: the elements h such that h • P is one of the tiles around x predicted by the side pairing. They are the identity, the inverse side-pairing map (map i)⁻¹ for each side i through x, whose translate of P lies across side i, and, when x is a finite vertex vertex j, the inverse partial cycle products (partialCycleMap j m)⁻¹.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.mem_localNeighbors_iff {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {x : UpperHalfPlane} {h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} : h ∈ σ.localNeighbors x ↔ h = 1 ∨ (∃ (i : Fin n), x ∈ P.side i ∧ (σ.map i)⁻¹ = h) ∨ ∃ (j : Fin n) (m : ℕ), P.vertex j = Sum.inl x ∧ (σ.partialCycleMap j m)⁻¹ = h

Membership in the local neighbours.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.one_mem_localNeighbors {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) (x : UpperHalfPlane) : 1 ∈ σ.localNeighbors x

The identity is a local neighbour of every point.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.inv_map_mem_localNeighbors {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {x : UpperHalfPlane} {i : Fin n} (hx : x ∈ P.side i) : (σ.map i)⁻¹ ∈ σ.localNeighbors x

The inverse side-pairing map of a side through x is a local neighbour of x.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.inv_partialCycleMap_mem_localNeighbors {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {x : UpperHalfPlane} (hx : P.vertex j = Sum.inl x) (m : ℕ) : (σ.partialCycleMap j m)⁻¹ ∈ σ.localNeighbors x

At a finite vertex, the inverse partial cycle products are local neighbours.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.localNeighbors_of_mem_interior {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {x : UpperHalfPlane} (hx : x ∈ interior P.carrier) : σ.localNeighbors x = {1}

An interior point of the polygon has only the identity as local neighbour.

The cycle of a finite vertex

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.localNeighbors_eq_range {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) {j : Fin n} {x : UpperHalfPlane} (hx : P.vertex j = Sum.inl x) (hj : 0 < orderOf (σ.cycleMap j)) : σ.localNeighbors x = Set.range fun (m : ℕ) => (σ.partialCycleMap j m)⁻¹

The local neighbours of a finite vertex are the inverse partial cycle products, provided the cycle transformation there has finite order.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.finite_localNeighbors {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) (x : UpperHalfPlane) : (σ.localNeighbors x).Finite

Under the angle condition, every point has finitely many local neighbours.

The local tiling axioms

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.inv_mul_mem_localNeighbors_of_smul_mem {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) {M : Set (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (hM : ∀ a ∈ M, ∀ b ∈ M, (a • interior P.carrier ∩ b • interior P.carrier).Nonempty → a = b) {h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} {v : UpperHalfPlane} (hv : v ∈ P.carrier) (hmul : ∀ k ∈ σ.localNeighbors v, h * k ∈ M) {h' : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} (hh' : h' ∈ M) (hvh' : h • v ∈ h' • P.carrier) : h⁻¹ * h' ∈ σ.localNeighbors v

Tiles through a point are translated local neighbours. Let M be a set of tiles with pairwise disjoint interiors, let v ∈ P, and suppose M contains the translates h * k of the local neighbours k of v. Then, under the angle condition, every tile of M through h • v is such a translate: the local neighbours of v cover a neighbourhood of v, so a tile through h • v overlaps one of their translates.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.isLocalTiling {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) : IsLocalTiling P.carrier σ.localNeighbors

The local tiling of a side-paired polygon. If at every finite vertex the cycle transformation has finite order m and the interior angles along the cycle add up to 2π / m, then the local neighbours of the points of P form a local tiling by P.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.SidePairing.closure_biUnion_localNeighbors {n : ℕ} [NeZero n] {P : ConvexPolygon n} (σ : P.SidePairing) : Subgroup.closure (⋃ x ∈ P.carrier, σ.localNeighbors x) = Subgroup.closure (Set.range σ.map)

The local neighbours of the points of P generate the same group as the side-pairing maps.