The local sector at a finite polygon vertex

The sector at a vertex of a convex hyperbolic polygon is the intersection of the closed left half-planes of its incoming and outgoing sides. The polygon lies in this sector and, near a finite vertex, agrees with it: all the nonincident side inequalities are strict at that vertex. This identifies the actual local polygon pieces used when assembling tiles around a vertex. Ideal vertices are allowed elsewhere in the polygon; the local equality concerns a vertex in the upper half-plane.

The construction commutes with projective transformations and cyclic relabelling, allowing the same local description to be used for translated polygon tiles.

References

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

def TauCeti.UpperHalfPlane.ConvexPolygon.vertexSector {n : ℕ} [NeZero n] (P : ConvexPolygon n) (j : Fin n) : Set UpperHalfPlane

The closed sector bounded by the incoming and outgoing supporting geodesics at vertex j. At a finite vertex this is the local polygon piece.

Equations

• P.vertexSector j = closure (TauCeti.UpperHalfPlane.leftHalfPlane (P.sideGeodesic (j - 1))) ∩ closure (TauCeti.UpperHalfPlane.leftHalfPlane (P.sideGeodesic j))

theorem TauCeti.UpperHalfPlane.ConvexPolygon.vertexSector_def {n : ℕ} [NeZero n] (P : ConvexPolygon n) (j : Fin n) : P.vertexSector j = closure (leftHalfPlane (P.sideGeodesic (j - 1))) ∩ closure (leftHalfPlane (P.sideGeodesic j))

The vertex sector is the intersection of the two incident closed half-planes.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.mem_vertexSector_iff {n : ℕ} [NeZero n] (P : ConvexPolygon n) (j : Fin n) (z : UpperHalfPlane) : z ∈ P.vertexSector j ↔ z ∈ closure (leftHalfPlane (P.sideGeodesic (j - 1))) ∧ z ∈ closure (leftHalfPlane (P.sideGeodesic j))

Membership in a vertex sector is given by the two incident side inequalities.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.isClosed_vertexSector {n : ℕ} [NeZero n] (P : ConvexPolygon n) (j : Fin n) : IsClosed (P.vertexSector j)

Vertex sectors are closed.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.interior_vertexSector {n : ℕ} [NeZero n] (P : ConvexPolygon n) (j : Fin n) : interior (P.vertexSector j) = leftHalfPlane (P.sideGeodesic (j - 1)) ∩ leftHalfPlane (P.sideGeodesic j)

The interior of the sector is cut out by the two strict incident side inequalities.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.mem_interior_vertexSector_iff {n : ℕ} [NeZero n] (P : ConvexPolygon n) (j : Fin n) (z : UpperHalfPlane) : z ∈ interior (P.vertexSector j) ↔ z ∈ leftHalfPlane (P.sideGeodesic (j - 1)) ∧ z ∈ leftHalfPlane (P.sideGeodesic j)

Membership in the sector interior is given by the two strict incident side inequalities.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.carrier_subset_vertexSector {n : ℕ} [NeZero n] (P : ConvexPolygon n) (j : Fin n) : P.carrier ⊆ P.vertexSector j

The polygon is contained in each of its vertex sectors.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.vertexSector_smul {n : ℕ} [NeZero n] (P : ConvexPolygon n) (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (j : Fin n) : (g • P).vertexSector j = g • P.vertexSector j

Moving the polygon moves its vertex sectors.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.vertexSector_rotate {n : ℕ} [NeZero n] (P : ConvexPolygon n) (k j : Fin n) : (P.rotate k).vertexSector j = P.vertexSector (j + k)

Cyclic relabelling relabels the vertex sectors.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.eventuallyEq_carrier_vertexSector {n : ℕ} [NeZero n] (P : ConvexPolygon n) {j : Fin n} {z : UpperHalfPlane} (hz : P.vertex j = Sum.inl z) : P.carrier =ᶠ[nhds z] P.vertexSector j

Near a finite vertex, the polygon agrees with the sector bounded by its two incident sides. No conditions on side pairings or other vertices are needed.