Global tessellations from local tessellations

Let a group G act by isometries on a simply connected, locally connected metric space X, and let P ⊆ X be a closed path-connected tile. A local tiling assigns to each point x ∈ P a set N x ⊆ G of local neighbours: the elements h for which h • P is meant to be one of the tiles around x. The sets N x are required to behave like the tiles around a point of an actual tessellation:

• 1 ∈ N x, and x ∈ h • P for h ∈ N x;
• the neighbours of x, seen from the tile h • P, are h⁻¹ • N x: if h ∈ N x then h⁻¹ ∈ N (h⁻¹ • x), and h * k ∈ N x for k ∈ N (h⁻¹ • x);
• every point of P lies in a tiling chart built from its own neighbours.

A tiling chart (W, M) is an open set W covered, locally finitely, by tiles h • P with h ∈ M, such that at every point of W the tiles of M through it are exactly the translates of the local neighbours there. Charts need not come from a single point: near an ideal vertex of a hyperbolic polygon the natural chart has infinitely many tiles.

The main theorem says that local tilings with charts of uniform size are restrictions of one global tessellation. Let Γ be the subgroup generated by all local neighbours. Then the translates γ • P, γ ∈ Γ, cover X and are locally finite, and the only coincidences between them are the local ones: if γ ∈ Γ carries a point x ∈ P to a point of P, then γ is a local neighbour at γ • x. The uniformity hypothesis holds automatically when P is compact, and in general it only needs checking off a compact subset of P.

This is the covering-space core of Poincaré's polygon theorem. There the tile is a side-paired hyperbolic polygon, the local neighbours at a point are the tiles met by following the side pairings around it, and the angle and cycle conditions at the vertices are what make them a local tiling; the conclusion then says that the polygon is a fundamental domain for the group generated by the side pairings.

The proof glues copies {a} × P, a ∈ G, identifying (a, x) with (b, y) when a • x = b • y and a⁻¹ * b ∈ N x. The map (a, x) ↦ a • x from the glued space to X has a continuous local section through every point, read off from a chart, over a ball of uniform radius, and the glued space is Hausdorff because every point has a chart of its own; so this map is a covering map. The copies indexed by Γ are joined by paths, since P is path-connected and the copies indexed by a and a * h meet for each local neighbour h. As X is simply connected, the covering map is injective on them.

Main definitions

• TauCeti.IsTilingChart P N W M: W is an open set tiled by the translates h • P, h ∈ M, compatibly with the local neighbours N.
• TauCeti.IsLocalTiling P N: the sets N x are local neighbours of a local tiling by P.
• TauCeti.HasUniformTilingCharts P N: tiling charts of a uniform size are available at every point of P.

Main results

• TauCeti.IsLocalTiling.isTilingChart_of_closure_subset: an open set is a tiling chart if tiles meeting compatibly with the local neighbours cover a set containing its closure.
• TauCeti.IsLocalTiling.hasUniformTilingCharts_of_isCompact_of_forall_notMem: charts of a uniform size off a compact set give uniform tiling charts.
• TauCeti.IsLocalTiling.hasUniformTilingCharts_of_isCompact: a compact tile has uniform tiling charts.
• TauCeti.IsLocalTiling.mem_of_smul_mem: an element of Γ carrying a point of P into P is a local neighbour at the image point.
• TauCeti.IsLocalTiling.iUnion_smul_eq_univ: uniform tiling charts imply that the translates of P by Γ cover a preconnected pseudometric space X.
• TauCeti.IsLocalTiling.locallyFinite_smul: the translates of P by Γ are locally finite.

References

• 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.
• Alan Beardon, The Geometry of Discrete Groups, Graduate Texts in Mathematics 91, Springer, 1983, Chapter 9.

structure TauCeti.IsTilingChart {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace X] (P : Set X) (N : X → Set G) (W : Set X) (M : Set G) : Prop

A tiling chart for the local neighbours N of a tile P: an open set W covered, locally finitely, by the tiles h • P with h ∈ M, such that at each point of W the tiles of M through that point are exactly the translates of the local neighbours there. Precisely, if h ∈ M and v ∈ P with h • v ∈ W, then h • N v ⊆ M, and every h' ∈ M with h • v ∈ h' • P lies in h • N v.

• isOpen : IsOpen W

  The domain of the chart is open.

• subset_iUnion_smul : W ⊆ ⋃ h ∈ M, h • P

  The tiles of the chart cover its domain.

• locallyFinite : LocallyFinite fun (h : ↑M) => ↑h • P ∩ W

  The tiles of the chart, cut down to its domain, are locally finite.

• mul_mem (h : G) : h ∈ M → ∀ v ∈ P, h • v ∈ W → ∀ k ∈ N v, h * k ∈ M

  The translated local neighbours at a point of the domain are tiles of the chart.

• inv_mul_mem (h : G) : h ∈ M → ∀ v ∈ P, h • v ∈ W → ∀ h' ∈ M, h • v ∈ h' • P → h⁻¹ * h' ∈ N v

  Every tile of the chart through a point of the domain is a translated local neighbour.

structure TauCeti.IsLocalTiling {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace X] (P : Set X) (N : X → Set G) : Prop

A local tiling by a closed path-connected tile P: for each x ∈ P, N x is a set of local neighbours, the elements h such that h • P is one of the tiles around x. The identity is a neighbour, x ∈ h • P for each neighbour h, the neighbours of x seen from the tile h • P are the translates h⁻¹ • N x, and each point of P lies in a tiling chart made of its own neighbours.

• isClosed : IsClosed P

  The tile is closed.

• isPathConnected : IsPathConnected P

  The tile is path-connected.

• one_mem (x : X) : x ∈ P → 1 ∈ N x

  The tile itself is a neighbour of each of its points.

• inv_smul_mem (x : X) : x ∈ P → ∀ h ∈ N x, h⁻¹ • x ∈ P

  Each point lies in its neighbouring tiles.

• inv_mem (x : X) : x ∈ P → ∀ h ∈ N x, h⁻¹ ∈ N (h⁻¹ • x)

  Seen from a neighbouring tile, the tile P is again a neighbour.

• mul_mem (x : X) : x ∈ P → ∀ h ∈ N x, ∀ k ∈ N (h⁻¹ • x), h * k ∈ N x

  Neighbours of a neighbouring tile are neighbours.

• exists_isTilingChart (x : X) : x ∈ P → ∃ (W : Set X), x ∈ W ∧ IsTilingChart P N W (N x)

  Each point lies in a tiling chart made of its own neighbours.

theorem TauCeti.IsLocalTiling.isTilingChart_of_closure_subset {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [TopologicalSpace X] [ContinuousConstSMul G X] {P : Set X} {N : X → Set G} (hP : IsLocalTiling P N) {W W' : Set X} {M : Set G} (hW : IsOpen W) (hWW' : closure W ⊆ W') (hcov : W' ⊆ ⋃ h ∈ M, h • P) (hmul : ∀ h ∈ M, ∀ v ∈ P, h • v ∈ W' → ∀ k ∈ N v, h * k ∈ M) (hinv : ∀ h ∈ M, ∀ v ∈ P, h • v ∈ W' → ∀ h' ∈ M, h • v ∈ h' • P → h⁻¹ * h' ∈ N v) : IsTilingChart P N W M

Tiling charts from the chart axioms on a larger set. Let W be open, and let the tiles h • P, h ∈ M, cover a set W' containing the closure of W. Suppose that at each point h • v of W', with h ∈ M and v ∈ P, the tiles of M through h • v are exactly the translates by h of the local neighbours of v. Then (W, M) is a tiling chart: its local finiteness is inherited from the charts of the points of P.

def TauCeti.HasUniformTilingCharts {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [PseudoMetricSpace X] (P : Set X) (N : X → Set G) : Prop

A local tiling has uniform tiling charts if there is a radius ε > 0 such that for each point y ∈ P some tiling chart (W, M), with M in the group generated by the local neighbours, contains the ball of radius ε about a translate h • y with h ∈ M.

theorem TauCeti.hasUniformTilingCharts_iff {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [PseudoMetricSpace X] {P : Set X} {N : X → Set G} : HasUniformTilingCharts P N ↔ ∃ ε > 0, ∀ y ∈ P, ∃ (W : Set X) (M : Set G), IsTilingChart P N W M ∧ M ⊆ ↑(Subgroup.closure (⋃ x ∈ P, N x)) ∧ ∃ h ∈ M, Metric.ball (h • y) ε ⊆ W

theorem TauCeti.IsLocalTiling.hasUniformTilingCharts_of_isCompact_of_forall_notMem {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [PseudoMetricSpace X] {P : Set X} {N : X → Set G} (hP : IsLocalTiling P N) {K : Set X} (hK : IsCompact K) {ε : ℝ} (hε : 0 < ε) (hout : ∀ y ∈ P, y ∉ K → ∃ (W : Set X) (M : Set G), IsTilingChart P N W M ∧ M ⊆ ↑(Subgroup.closure (⋃ x ∈ P, N x)) ∧ ∃ h ∈ M, Metric.ball (h • y) ε ⊆ W) : HasUniformTilingCharts P N

Uniform tiling charts away from a compact set. If the points of P outside a compact set K have tiling charts containing balls of a common radius ε > 0, then the local tiling has uniform tiling charts: on the compact part K ∩ P, the charts of the points of P have a Lebesgue number.

theorem TauCeti.IsLocalTiling.hasUniformTilingCharts_of_isCompact {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [PseudoMetricSpace X] {P : Set X} {N : X → Set G} (hP : IsLocalTiling P N) (hc : IsCompact P) : HasUniformTilingCharts P N

A compact tile has uniform tiling charts.

theorem TauCeti.IsLocalTiling.iUnion_smul_eq_univ {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [PseudoMetricSpace X] {P : Set X} {N : X → Set G} [IsIsometricSMul G X] [PreconnectedSpace X] (hP : IsLocalTiling P N) (hu : HasUniformTilingCharts P N) : ⋃ γ ∈ Subgroup.closure (⋃ x ∈ P, N x), γ • P = Set.univ

The translates of the tile cover the space. For a local tiling with uniform charts of a preconnected pseudometric space acted on by isometries, the translates of P by the group generated by the local neighbours cover the space.

The space glued from copies of the tile

Local sections from tiling charts

The global tessellation

theorem TauCeti.IsLocalTiling.mem_of_smul_mem {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [MetricSpace X] {P : Set X} {N : X → Set G} [IsIsometricSMul G X] [LocallyConnectedSpace X] [SimplyConnectedSpace X] (hP : IsLocalTiling P N) (hu : HasUniformTilingCharts P N) {γ : G} (hγ : γ ∈ Subgroup.closure (⋃ x ∈ P, N x)) {x : X} (hx : x ∈ P) (hγx : γ • x ∈ P) : γ ∈ N (γ • x)

Coincidences of translates are local. For a local tiling with uniform charts of a simply connected, locally connected metric space, an element γ of the group generated by the local neighbours which carries a point x ∈ P to a point of P is a local neighbour at γ • x.

theorem TauCeti.IsLocalTiling.locallyFinite_smul {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [MetricSpace X] {P : Set X} {N : X → Set G} [IsIsometricSMul G X] [LocallyConnectedSpace X] [SimplyConnectedSpace X] (hP : IsLocalTiling P N) (hu : HasUniformTilingCharts P N) : LocallyFinite fun (γ : ↥(Subgroup.closure (⋃ x ∈ P, N x))) => ↑γ • P

The translates of the tile are locally finite. For a local tiling with uniform charts of a simply connected, locally connected metric space, the translates of P by the group generated by the local neighbours form a locally finite family.