Polygons cut out by finitely many half-planes

A finite intersection K of closed geodesic half-planes of ℍ with nonempty interior is the carrier of a convex polygon, possibly with ideal vertices, as soon as removing finitely many open horodiscs from K leaves a bounded set (exists_convexPolygon_carrier_eq_iInter_closure_leftHalfPlane). Each side of the polygon lies on the boundary line of one of the half-planes, with the polygon on the left, and is exactly the face of K along that line; each ideal vertex is the centre of one of the horodiscs. With no horodiscs, a bounded intersection is a compact convex polygon (exists_compactConvexPolygon_carrier_eq_iInter_closure_leftHalfPlane). This converts finite half-plane descriptions, such as those of Dirichlet domains truncated at their cusps, into polygons with enumerated vertices and sides.

Proof

First discard redundant half-planes: in a minimal subfamily with the same intersection K, each line L carries a point strictly inside all the other half-planes, found by crossing L on the segment from an interior point to a point violating only the half-plane of L. The face K ∩ L is then an extended geodesic segment with two distinct endpoints in ℍ ∪ ∂ℍ, traversed with K on its left. Following faces from their ends to their starts is a permutation of the lines, and one of its cycles lists the vertices of a convex polygon. Its carrier contains K and, by the hull property ConvexPolygon.carrier_subset_closure_leftHalfPlane_of_forall, lies in K.

• An end in ℍ lies on some other line L', as otherwise K would continue along L. It is not inside the face of L', since L would then cross into the open right side of L'. It is not the end of that face either, since the two faces would then reach it from opposite sides, which the signs of the oriented angles there exclude. So it is the start of the face on L'.
• At an ideal end, move it to ∞. Two lines of the family never run to the same ideal point, nor from the same ideal point, since each carries a point strictly to the left of the other; one line may run to the ideal point another runs from, as two sides meeting at an ideal vertex do. As K has points arbitrarily high up, every semicircle has ∞ on its left, so a vertical line of the family has all its high points in K: the vertical constraints only see the real part, and the line meets K. If no line ran down from ∞, K would contain every point far enough to the left, and the points of a small fixed height escaping to the left would leave every horodisc while staying in K. So some line runs down from ∞, and its face starts there. If no horodisc were centred at ∞, the points of K high up would leave every horodisc in the same way.

References

• Alan Beardon, The Geometry of Discrete Groups, Graduate Texts in Mathematics 91, Springer, 1983, §9.4 (sides and vertices of convex polygons).
• Svetlana Katok, Fuchsian Groups, Chicago Lectures in Mathematics, University of Chicago Press, 1992, §§3.2 and 4.2 (Dirichlet regions and their cusps).

Discarding redundant half-planes

The endpoints of a face

For a geodesic line g and a set K ⊆ ℍ, the face of K along the line is the set of points geodesicLine g t in K. When K is an intersection of closed half-planes, its parameters geodesicLine g ⁻¹' K form a closed interval, and the face is an extended geodesic segment between the two points of ℍ ∪ ∂ℍ below.

Geodesic lines seen from ∞

The faces of an irredundant intersection

Throughout, K is the intersection of the closed left half-planes of finitely many geodesic lines L k, and each line L k carries the point geodesicLine (L k) (u k) strictly inside all the other half-planes.

Ideal endpoints

Moving an ideal endpoint to ∞

The polygon

theorem TauCeti.UpperHalfPlane.exists_convexPolygon_carrier_eq_iInter_closure_leftHalfPlane {ι : Type u_1} {ι' : Type u_2} [Finite ι'] (t : Finset ι) (L : ι → Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (hint : (interior (⋂ k ∈ t, closure (leftHalfPlane (L k)))).Nonempty) (g : ι' → Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) {A : ι' → ℝ} (hA : ∀ (i : ι'), 0 < A i) (hb : Bornology.IsBounded ((⋂ k ∈ t, closure (leftHalfPlane (L k))) \ ⋃ (i : ι'), {z : UpperHalfPlane | A i < (g i • z).im})) : ∃ (n : ℕ) (x : NeZero n) (P : ConvexPolygon n), P.carrier = ⋂ k ∈ t, closure (leftHalfPlane (L k)) ∧ (∀ (i : Fin n), ∃ k ∈ t, leftHalfPlane (P.sideGeodesic i) = leftHalfPlane (L k) ∧ P.side i = (⋂ k ∈ t, closure (leftHalfPlane (L k))) ∩ Set.range (geodesicLine (L k))) ∧ ∀ (i : Fin n) (ξ : OnePoint ℝ), P.vertex i = Sum.inr ξ → ∃ (j : ι'), g j • ξ = OnePoint.infty

A finite intersection of closed half-planes with a bounded cusp truncation is a convex polygon. Let K be the intersection of the closed left half-planes of the geodesic lines L k, k ∈ t, for a finite set t, and suppose that K has nonempty interior. Suppose that removing from K finitely many open horodiscs {z | A i < Im (g i • z)} with A i > 0, centred at the ideal points carried to ∞ by g i, leaves a bounded set. Then K is the carrier of a convex polygon, possibly with ideal vertices. Each side of the polygon is the face K ∩ L k of K along the line of some k ∈ t, and the polygon lies to the left of that line. Each ideal vertex is the centre of one of the horodiscs.

theorem TauCeti.UpperHalfPlane.exists_compactConvexPolygon_carrier_eq_iInter_closure_leftHalfPlane {ι : Type u_1} (t : Finset ι) (L : ι → Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (hint : (interior (⋂ k ∈ t, closure (leftHalfPlane (L k)))).Nonempty) (hb : Bornology.IsBounded (⋂ k ∈ t, closure (leftHalfPlane (L k)))) : ∃ (n : ℕ) (x : NeZero n) (P : CompactConvexPolygon n), P.carrier = ⋂ k ∈ t, closure (leftHalfPlane (L k)) ∧ ∀ (i : Fin n), ∃ k ∈ t, leftHalfPlane (geodesicBetween (P.vertex i) (P.vertex (i + 1))) = leftHalfPlane (L k) ∧ P.side i = (⋂ k ∈ t, closure (leftHalfPlane (L k))) ∩ Set.range (geodesicLine (L k))

A bounded intersection of finitely many closed half-planes is a compact convex polygon. Let K be the intersection of the closed left half-planes of the geodesic lines L k, k ∈ t, for a finite set t. If K is bounded with nonempty interior, it is the carrier of a compact convex polygon. Each side of the polygon is the face K ∩ L k of K along the line of some k ∈ t, and the polygon lies to the left of that line.