Convex hyperbolic polygons with ideal vertices

A convex hyperbolic polygon with n ≥ 3 vertices is given by its vertices v₀, …, vₙ₋₁ in ℍ ∪ ∂ℍ, modelled as ℍ ⊕ OnePoint ℝ, listed counterclockwise: consecutive vertices are distinct, and every vertex other than the endpoints of an edge lies strictly to the left of the geodesic through that edge, in the open half-plane or on the open arc of ideal points on its left (ConvexPolygon). A vertex on ∂ℍ is an ideal vertex. The side from vᵢ to vᵢ₊₁ (ConvexPolygon.side i) is the closed piece of geodesic between them: a segment if both lie in ℍ, a ray if one of them is ideal, a whole geodesic line if both are. It lies on the full geodesic line ConvexPolygon.sideGeodesic i running from vᵢ to vᵢ₊₁, the carrier is the intersection of the closed left half-planes of these lines (ConvexPolygon.carrier) and contains every side, and the interior angle at a vertex is the angle between the two sides there (ConvexPolygon.interiorAngle), which is 0 at an ideal vertex.

A compact convex polygon (CompactConvexPolygon, all vertices in ℍ) is a convex polygon with the same sides, carrier and angles (CompactConvexPolygon.toConvexPolygon), and every convex polygon without ideal vertices arises this way (ConvexPolygon.exists_eq_toConvexPolygon).

Main definitions

• ConvexPolygon n: a convex hyperbolic polygon with n vertices in ℍ ∪ ∂ℍ.
• ConvexPolygon.side, ConvexPolygon.sideGeodesic, ConvexPolygon.carrier, ConvexPolygon.interiorAngle: its sides, the geodesic lines of its sides, its carrier and its interior angles.
• ConvexPolygon.rotate: the cyclic relabelling of the vertices.
• CompactConvexPolygon.toConvexPolygon: a compact convex polygon as a convex polygon.

Main results

• ConvexPolygon.vertex_injective: the vertices are distinct.
• ConvexPolygon.isClosed_carrier, ConvexPolygon.mem_carrier_iff_sideForm_nonpos: the carrier is closed, and is cut out by the side forms of the edges.
• ConvexPolygon.side_subset_range_sideGeodesic, ConvexPolygon.side_subset_carrier: each side lies on its geodesic line and in the carrier.
• ConvexPolygon.vertex_mem_extClosedLeftHalfPlane_sideGeodesic: every vertex is weakly to the left of the geodesic line of every side.
• ConvexPolygon.sideForm_sideGeodesic_toComplex_nonpos, ConvexPolygon.sideForm_sideGeodesic_toComplex_neg: every vertex other than ∞ lies in the closed left half-plane of the geodesic line of every side, strictly when it is not an endpoint of that side.
• The MulAction of PSL(2, ℝ) on convex polygons, with ConvexPolygon.side_smul, ConvexPolygon.carrier_smul and ConvexPolygon.interiorAngle_smul; the cyclic relabelling ConvexPolygon.rotate, with ConvexPolygon.rotate_zero, ConvexPolygon.rotate_rotate, ConvexPolygon.side_rotate, ConvexPolygon.carrier_rotate and ConvexPolygon.sum_interiorAngle_rotate.
• CompactConvexPolygon.side_toConvexPolygon, CompactConvexPolygon.carrier_toConvexPolygon, CompactConvexPolygon.interiorAngle_toConvexPolygon: the embedding preserves sides, carrier and angles.

The counterclockwise orientation is a convention of this file, as for CompactConvexPolygon.

Source

Walkden, Hyperbolic geometry (MATH32051 lecture notes, Manchester 2019), §7.1 (polygons with vertices in ℍ ∪ ∂ℍ; their sides [vᵢ, vᵢ₊₁], which are rays or geodesic lines at ideal vertices; ideal vertices and their zero angle) and §14.2 (a convex hyperbolic polygon is an intersection of finitely many half-planes).

structure TauCeti.UpperHalfPlane.ConvexPolygon (n : ℕ) [NeZero n] : Type

A convex hyperbolic polygon with n vertices vertex 0, …, vertex (n - 1) in ℍ ∪ ∂ℍ, listed counterclockwise: consecutive vertices are distinct, and every vertex other than vertex i and vertex (i + 1) lies strictly to the left of the geodesic from vertex i to vertex (i + 1).

• vertex : Fin n → UpperHalfPlane ⊕ OnePoint ℝ

  The vertices, in counterclockwise order; indices are taken cyclically.

• three_le : 3 ≤ n

  A polygon has at least three vertices.

• vertex_ne_vertex_add_one (i : Fin n) : self.vertex i ≠ self.vertex (i + 1)

  Consecutive vertices are distinct.

• vertex_mem_extLeftHalfPlane (i j : Fin n) : j ≠ i → j ≠ i + 1 → self.vertex j ∈ extLeftHalfPlane (geodesicFromTo (self.vertex i) (self.vertex (i + 1)))

  Every vertex off an edge lies strictly to the left of it.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.ext_iff {n : ℕ} {inst✝ : NeZero n} {x y : ConvexPolygon n} : x = y ↔ x.vertex = y.vertex

theorem TauCeti.UpperHalfPlane.ConvexPolygon.ext {n : ℕ} {inst✝ : NeZero n} {x y : ConvexPolygon n} (vertex : x.vertex = y.vertex) : x = y

Sides and vertices

noncomputable def TauCeti.UpperHalfPlane.ConvexPolygon.sideGeodesic {n : ℕ} [NeZero n] (P : ConvexPolygon n) (i : Fin n) : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ

The full geodesic line supporting the side of a convex polygon from vertex i to vertex (i + 1), oriented from vertex i to vertex (i + 1).

Equations

• P.sideGeodesic i = TauCeti.UpperHalfPlane.geodesicFromTo (P.vertex i) (P.vertex (i + 1))

theorem TauCeti.UpperHalfPlane.ConvexPolygon.sideGeodesic_def {n : ℕ} [NeZero n] (P : ConvexPolygon n) (i : Fin n) : P.sideGeodesic i = geodesicFromTo (P.vertex i) (P.vertex (i + 1))

The geodesic line of a side, unfolded.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.isGeodesicFromTo_sideGeodesic {n : ℕ} [NeZero n] (P : ConvexPolygon n) (i : Fin n) : IsGeodesicFromTo (P.sideGeodesic i) (P.vertex i) (P.vertex (i + 1))

The geodesic line of the side from vertex i runs from vertex i to vertex (i + 1).

theorem TauCeti.UpperHalfPlane.ConvexPolygon.vertex_mem_extLeftHalfPlane_sideGeodesic {n : ℕ} [NeZero n] (P : ConvexPolygon n) {i j : Fin n} (hji : j ≠ i) (hji' : j ≠ i + 1) : P.vertex j ∈ extLeftHalfPlane (P.sideGeodesic i)

A vertex off an edge lies strictly to the left of it.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.vertex_mem_extClosedLeftHalfPlane_sideGeodesic {n : ℕ} [NeZero n] (P : ConvexPolygon n) (i j : Fin n) : P.vertex j ∈ extClosedLeftHalfPlane (P.sideGeodesic i)

Every vertex is weakly to the left of the geodesic line of every side: the endpoints of the side lie on its closure, and the other vertices strictly to its left.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.vertex_injective {n : ℕ} [NeZero n] (P : ConvexPolygon n) : Function.Injective P.vertex

The vertices of a convex polygon are distinct.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.vertex_ne_vertex_sub_one {n : ℕ} [NeZero n] (P : ConvexPolygon n) (i : Fin n) : P.vertex i ≠ P.vertex (i - 1)

A vertex differs from the previous one.

The carrier

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

The carrier of a convex polygon: the intersection of the closed left half-planes of its edges.

Equations

• P.carrier = ⋂ (i : Fin n), closure (TauCeti.UpperHalfPlane.leftHalfPlane (P.sideGeodesic i))

theorem TauCeti.UpperHalfPlane.ConvexPolygon.carrier_def {n : ℕ} [NeZero n] (P : ConvexPolygon n) : P.carrier = ⋂ (i : Fin n), closure (leftHalfPlane (P.sideGeodesic i))

The carrier, unfolded: the intersection of the closed left half-planes of the edges.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.mem_carrier_iff {n : ℕ} [NeZero n] (P : ConvexPolygon n) (z : UpperHalfPlane) : z ∈ P.carrier ↔ ∀ (i : Fin n), z ∈ closure (leftHalfPlane (P.sideGeodesic i))

Membership in the carrier.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.carrier_subset_closure_leftHalfPlane {n : ℕ} [NeZero n] (P : ConvexPolygon n) (i : Fin n) : P.carrier ⊆ closure (leftHalfPlane (P.sideGeodesic i))

The polygon lies in the closed left half-plane of each side.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.mem_carrier_iff_sideForm_nonpos {n : ℕ} [NeZero n] (P : ConvexPolygon n) (z : UpperHalfPlane) : z ∈ P.carrier ↔ ∀ (i : Fin n), sideForm (P.sideGeodesic i) ↑z ≤ 0

The carrier is cut out by the side forms of the edges.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.isClosed_carrier {n : ℕ} [NeZero n] (P : ConvexPolygon n) : IsClosed P.carrier

The carrier is closed.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.measurableSet_carrier {n : ℕ} [NeZero n] (P : ConvexPolygon n) : MeasurableSet P.carrier

The carrier is measurable.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.interior_carrier {n : ℕ} [NeZero n] (P : ConvexPolygon n) : interior P.carrier = ⋂ (i : Fin n), leftHalfPlane (P.sideGeodesic i)

The interior is the intersection of the open left half-planes of the sides.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.mem_interior_carrier_iff {n : ℕ} [NeZero n] (P : ConvexPolygon n) (z : UpperHalfPlane) : z ∈ interior P.carrier ↔ ∀ (i : Fin n), z ∈ leftHalfPlane (P.sideGeodesic i)

A point is in the polygon interior exactly when it is strictly left of every side.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.mem_interior_carrier_iff_sideForm_neg {n : ℕ} [NeZero n] (P : ConvexPolygon n) (z : UpperHalfPlane) : z ∈ interior P.carrier ↔ ∀ (i : Fin n), sideForm (P.sideGeodesic i) ↑z < 0

A point is in the polygon interior exactly when every side form is strictly negative.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.sideForm_sideGeodesic_toComplex_neg {n : ℕ} [NeZero n] (P : ConvexPolygon n) {i j : Fin n} (hj : P.vertex j ≠ Sum.inr OnePoint.infty) (hji : j ≠ i) (hji' : j ≠ i + 1) : sideForm (P.sideGeodesic i) (toComplex (P.vertex j)) < 0

A vertex other than ∞ and off an edge lies strictly to its left: the side form of the edge is negative there.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.sideForm_sideGeodesic_toComplex_nonpos {n : ℕ} [NeZero n] (P : ConvexPolygon n) (i j : Fin n) (hj : P.vertex j ≠ Sum.inr OnePoint.infty) : sideForm (P.sideGeodesic i) (toComplex (P.vertex j)) ≤ 0

Every vertex other than ∞ lies in the closed left half-plane of every edge: the side form of the edge is nonpositive there.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.vertex_mem_carrier {n : ℕ} [NeZero n] (P : ConvexPolygon n) {i : Fin n} {z : UpperHalfPlane} (h : P.vertex i = Sum.inl z) : z ∈ P.carrier

A vertex in ℍ lies in the carrier.

Sides

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

The side of a convex polygon from vertex i to vertex (i + 1): the geodesic segment between them if both lie in ℍ, the geodesic ray from the one in ℍ towards the other if exactly one of them is ideal, and the whole geodesic line sideGeodesic i if both are ideal.

Equations

• P.side i = TauCeti.UpperHalfPlane.extGeodesicSegment (P.vertex i) (P.vertex (i + 1))

theorem TauCeti.UpperHalfPlane.ConvexPolygon.side_def {n : ℕ} [NeZero n] (P : ConvexPolygon n) (i : Fin n) : P.side i = extGeodesicSegment (P.vertex i) (P.vertex (i + 1))

The side of a convex polygon, unfolded: the geodesic piece between vertex i and vertex (i + 1).

theorem TauCeti.UpperHalfPlane.ConvexPolygon.mem_side_of_vertex_eq_inl {n : ℕ} [NeZero n] (P : ConvexPolygon n) {i : Fin n} {z : UpperHalfPlane} (h : P.vertex i = Sum.inl z) : z ∈ P.side i

A vertex in ℍ lies on the side starting there.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.mem_side_of_vertex_add_one_eq_inl {n : ℕ} [NeZero n] (P : ConvexPolygon n) {i : Fin n} {z : UpperHalfPlane} (h : P.vertex (i + 1) = Sum.inl z) : z ∈ P.side i

A vertex in ℍ lies on the side ending there.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.side_subset_range_sideGeodesic {n : ℕ} [NeZero n] (P : ConvexPolygon n) (i : Fin n) : P.side i ⊆ Set.range (geodesicLine (P.sideGeodesic i))

A side lies on its geodesic line.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.side_subset_carrier {n : ℕ} [NeZero n] (P : ConvexPolygon n) (i : Fin n) : P.side i ⊆ P.carrier

The sides lie in the carrier.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.side_subset_frontier_carrier {n : ℕ} [NeZero n] (P : ConvexPolygon n) (i : Fin n) : P.side i ⊆ frontier P.carrier

Every side belongs to the topological boundary of the polygon.

Interior angles

noncomputable def TauCeti.UpperHalfPlane.ConvexPolygon.interiorAngle {n : ℕ} [NeZero n] (P : ConvexPolygon n) (i : Fin n) : ℝ

The interior angle of a convex polygon at vertex i: the angle between the edges to vertex (i - 1) and to vertex (i + 1), which is 0 at an ideal vertex.

Equations

• P.interiorAngle i = TauCeti.UpperHalfPlane.vertexAngle (P.vertex i) (P.vertex (i - 1)) (P.vertex (i + 1))

theorem TauCeti.UpperHalfPlane.ConvexPolygon.interiorAngle_def {n : ℕ} [NeZero n] (P : ConvexPolygon n) (i : Fin n) : P.interiorAngle i = vertexAngle (P.vertex i) (P.vertex (i - 1)) (P.vertex (i + 1))

The interior angle of a convex polygon, unfolded.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.interiorAngle_eq_zero_of_vertex_eq_inr {n : ℕ} [NeZero n] (P : ConvexPolygon n) {i : Fin n} {ξ : OnePoint ℝ} (h : P.vertex i = Sum.inr ξ) : P.interiorAngle i = 0

The interior angle at an ideal vertex is 0.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.interiorAngle_nonneg {n : ℕ} [NeZero n] (P : ConvexPolygon n) (i : Fin n) : 0 ≤ P.interiorAngle i

The interior angles are nonnegative.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.interiorAngle_pos_of_isLeft_vertex {n : ℕ} [NeZero n] (P : ConvexPolygon n) {i : Fin n} (hi : (P.vertex i).isLeft = true) : 0 < P.interiorAngle i

The interior angle at a finite vertex is positive.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.interiorAngle_le_pi {n : ℕ} [NeZero n] (P : ConvexPolygon n) (i : Fin n) : P.interiorAngle i ≤ Real.pi

The interior angles are at most π.

The action of PSL(2, ℝ)

@[instance_reducible]

noncomputable instance TauCeti.UpperHalfPlane.ConvexPolygon.instMulActionProjectiveSpecialLinearGroupFinOfNatNatReal {n : ℕ} [NeZero n] : MulAction (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (ConvexPolygon n)

PSL(2, ℝ) acts on convex polygons by moving their vertices.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.vertex_smul {n : ℕ} [NeZero n] (P : ConvexPolygon n) (h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (i : Fin n) : (h • P).vertex i = h • P.vertex i

The vertices of the translate.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.side_smul {n : ℕ} [NeZero n] (P : ConvexPolygon n) (h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (i : Fin n) : (h • P).side i = h • P.side i

The sides of the translate are the translates of the sides.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.closure_leftHalfPlane_sideGeodesic_smul {n : ℕ} [NeZero n] (P : ConvexPolygon n) (h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (i : Fin n) : closure (leftHalfPlane ((h • P).sideGeodesic i)) = h • closure (leftHalfPlane (P.sideGeodesic i))

The closed left half-plane of an edge of the translate is the translate of that of the edge.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.carrier_smul {n : ℕ} [NeZero n] (P : ConvexPolygon n) (h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) : (h • P).carrier = h • P.carrier

The carrier of the translate is the translate of the carrier.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.interiorAngle_smul {n : ℕ} [NeZero n] (P : ConvexPolygon n) (h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (i : Fin n) : (h • P).interiorAngle i = P.interiorAngle i

The interior angles are invariant under PSL(2, ℝ).

Cyclic relabelling

def TauCeti.UpperHalfPlane.ConvexPolygon.rotate {n : ℕ} [NeZero n] (P : ConvexPolygon n) (k : Fin n) : ConvexPolygon n

The same polygon with its vertices relabelled cyclically, starting from vertex k.

Equations

• P.rotate k = { vertex := fun (i : Fin n) => P.vertex (i + k), three_le := ⋯, vertex_ne_vertex_add_one := ⋯, vertex_mem_extLeftHalfPlane := ⋯ }

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.vertex_rotate {n : ℕ} [NeZero n] (P : ConvexPolygon n) (k i : Fin n) : (P.rotate k).vertex i = P.vertex (i + k)

The vertices of the relabelled polygon.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.rotate_zero {n : ℕ} [NeZero n] (P : ConvexPolygon n) : P.rotate 0 = P

Relabelling by 0 does nothing.

@[simp]

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

Relabelling twice is relabelling by the sum.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.sideGeodesic_rotate {n : ℕ} [NeZero n] (P : ConvexPolygon n) (k i : Fin n) : (P.rotate k).sideGeodesic i = P.sideGeodesic (i + k)

The edges of the relabelled polygon.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.side_rotate {n : ℕ} [NeZero n] (P : ConvexPolygon n) (k i : Fin n) : (P.rotate k).side i = P.side (i + k)

The sides of the relabelled polygon.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.carrier_rotate {n : ℕ} [NeZero n] (P : ConvexPolygon n) (k : Fin n) : (P.rotate k).carrier = P.carrier

Relabelling the vertices does not change the carrier.

@[simp]

theorem TauCeti.UpperHalfPlane.ConvexPolygon.interiorAngle_rotate {n : ℕ} [NeZero n] (P : ConvexPolygon n) (k i : Fin n) : (P.rotate k).interiorAngle i = P.interiorAngle (i + k)

The interior angles of the relabelled polygon.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.sum_interiorAngle_rotate {n : ℕ} [NeZero n] (P : ConvexPolygon n) (k : Fin n) : ∑ i : Fin n, (P.rotate k).interiorAngle i = ∑ i : Fin n, P.interiorAngle i

Relabelling the vertices does not change the angle sum.

Compact convex polygons

def TauCeti.UpperHalfPlane.CompactConvexPolygon.toConvexPolygon {n : ℕ} [NeZero n] (P : CompactConvexPolygon n) : ConvexPolygon n

A compact convex polygon, as a convex polygon without ideal vertices.

Equations

• P.toConvexPolygon = { vertex := fun (i : Fin n) => Sum.inl (P.vertex i), three_le := ⋯, vertex_ne_vertex_add_one := ⋯, vertex_mem_extLeftHalfPlane := ⋯ }

@[simp]

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.vertex_toConvexPolygon {n : ℕ} [NeZero n] (P : CompactConvexPolygon n) (i : Fin n) : P.toConvexPolygon.vertex i = Sum.inl (P.vertex i)

The vertices of toConvexPolygon.

@[simp]

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.side_toConvexPolygon {n : ℕ} [NeZero n] (P : CompactConvexPolygon n) (i : Fin n) : P.toConvexPolygon.side i = P.side i

toConvexPolygon does not change the sides.

@[simp]

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.carrier_toConvexPolygon {n : ℕ} [NeZero n] (P : CompactConvexPolygon n) : P.toConvexPolygon.carrier = P.carrier

toConvexPolygon does not change the carrier.

@[simp]

theorem TauCeti.UpperHalfPlane.CompactConvexPolygon.interiorAngle_toConvexPolygon {n : ℕ} [NeZero n] (P : CompactConvexPolygon n) (i : Fin n) : P.toConvexPolygon.interiorAngle i = P.interiorAngle i

toConvexPolygon does not change the interior angles.

theorem TauCeti.UpperHalfPlane.ConvexPolygon.exists_eq_toConvexPolygon {n : ℕ} [NeZero n] (P : ConvexPolygon n) (h : ∀ (i : Fin n), ∃ (z : UpperHalfPlane), P.vertex i = Sum.inl z) : ∃ (Q : CompactConvexPolygon n), Q.toConvexPolygon = P

A convex polygon without ideal vertices is a compact convex polygon.