Geodesic segments, rays and lines between points of ℍ ∪ ∂ℍ

For points p, q of ℍ ∪ ∂ℍ, modelled as ℍ ⊕ OnePoint ℝ, extGeodesicSegment p q is the closed piece of the geodesic through p and q lying between them, as a set of points of ℍ: the segment geodesicSegment z w between two points of ℍ, the ray from a point of ℍ towards an ideal point, and the whole geodesic line between two distinct ideal points. Between an ideal point and itself it is empty. The piece does not depend on the order of p and q (extGeodesicSegment_comm), contains the endpoints that lie in ℍ, lies on every geodesic line running from p to q (extGeodesicSegment_subset_range_geodesicLine), and is equivariant under PSL(2, ℝ) (smul_extGeodesicSegment).

Closed half-planes are convex in this extended sense: if p and q are weakly to the left of geodesicLine k (extClosedLeftHalfPlane k), then so is the piece between them (extGeodesicSegment_subset_closure_leftHalfPlane), and in particular a geodesic ray or line whose endpoints are weakly to the left of geodesicLine k lies in its closed left half-plane (geodesicLine_image_Ici_subset_closure_leftHalfPlane, range_geodesicLine_subset_closure_leftHalfPlane). Away from finite endpoints, this containment is strict unless the supporting lines coincide (mem_leftHalfPlane_of_mem_extGeodesicSegment).

Main declarations

• TauCeti.UpperHalfPlane.extGeodesicSegment p q: the closed geodesic piece between two points of ℍ ∪ ∂ℍ.
• TauCeti.UpperHalfPlane.extGeodesicSegment_comm, TauCeti.UpperHalfPlane.smul_extGeodesicSegment: symmetry and equivariance.
• TauCeti.UpperHalfPlane.extGeodesicSegment_subset_closure_leftHalfPlane: closed half-planes are convex.

Source

Walkden, Hyperbolic geometry (MATH32051 lecture notes, Manchester 2019), §7.1 (for z, w ∈ ℍ ∪ ∂ℍ, the part [z, w] of the unique geodesic through z and w lying between them; the sides of a polygon with vertices in ℍ ∪ ∂ℍ) and Solution 14.1 (half-planes are convex).

The geodesic piece between two points of ℍ ∪ ∂ℍ

def TauCeti.UpperHalfPlane.extGeodesicSegment : UpperHalfPlane ⊕ OnePoint ℝ → UpperHalfPlane ⊕ OnePoint ℝ → Set UpperHalfPlane

The closed piece of the geodesic through p and q lying between them, for points p, q of ℍ ∪ ∂ℍ: the segment geodesicSegment z w for z, w ∈ ℍ (the point {z} if z = w), the ray from z ∈ ℍ towards an ideal point ξ (in either order of p and q), and the whole geodesic line between two distinct ideal points. Between an ideal point and itself it is ∅.

Equations

• One or more equations did not get rendered due to their size.
• TauCeti.UpperHalfPlane.extGeodesicSegment (Sum.inl z) (Sum.inl w) = z.geodesicSegment w
• TauCeti.UpperHalfPlane.extGeodesicSegment (Sum.inl z) (Sum.inr η) = TauCeti.UpperHalfPlane.geodesicLine (z.rayToward (Sum.inr η)) '' Set.Ici 0
• TauCeti.UpperHalfPlane.extGeodesicSegment (Sum.inr ξ) (Sum.inl w) = TauCeti.UpperHalfPlane.geodesicLine (w.rayToward (Sum.inr ξ)) '' Set.Ici 0

@[simp]

theorem TauCeti.UpperHalfPlane.extGeodesicSegment_inl_inl (z w : UpperHalfPlane) : extGeodesicSegment (Sum.inl z) (Sum.inl w) = z.geodesicSegment w

Between two points of ℍ, the piece is the geodesic segment.

@[simp]

theorem TauCeti.UpperHalfPlane.extGeodesicSegment_inl_inr (z : UpperHalfPlane) (η : OnePoint ℝ) : extGeodesicSegment (Sum.inl z) (Sum.inr η) = geodesicLine (z.rayToward (Sum.inr η)) '' Set.Ici 0

Between a point z of ℍ and an ideal point η, the piece is the ray from z to η.

@[simp]

theorem TauCeti.UpperHalfPlane.extGeodesicSegment_inr_inl (ξ : OnePoint ℝ) (w : UpperHalfPlane) : extGeodesicSegment (Sum.inr ξ) (Sum.inl w) = geodesicLine (w.rayToward (Sum.inr ξ)) '' Set.Ici 0

Between an ideal point ξ and a point w of ℍ, the piece is the ray from w to ξ.

@[simp]

theorem TauCeti.UpperHalfPlane.extGeodesicSegment_inr_self (ξ : OnePoint ℝ) : extGeodesicSegment (Sum.inr ξ) (Sum.inr ξ) = ∅

Between an ideal point and itself, the piece is empty.

theorem TauCeti.UpperHalfPlane.extGeodesicSegment_inr_inr {ξ η : OnePoint ℝ} (h : ξ ≠ η) : extGeodesicSegment (Sum.inr ξ) (Sum.inr η) = Set.range (geodesicLine (geodesicFromTo (Sum.inr ξ) (Sum.inr η)))

Between two distinct ideal points, the piece is the whole geodesic line joining them.

theorem TauCeti.UpperHalfPlane.extGeodesicSegment_comm (p q : UpperHalfPlane ⊕ OnePoint ℝ) : extGeodesicSegment q p = extGeodesicSegment p q

The piece does not depend on the order of its endpoints.

@[simp]

theorem TauCeti.UpperHalfPlane.left_mem_extGeodesicSegment (z : UpperHalfPlane) (q : UpperHalfPlane ⊕ OnePoint ℝ) : z ∈ extGeodesicSegment (Sum.inl z) q

A starting point in ℍ lies on the piece.

@[simp]

theorem TauCeti.UpperHalfPlane.right_mem_extGeodesicSegment (p : UpperHalfPlane ⊕ OnePoint ℝ) (w : UpperHalfPlane) : w ∈ extGeodesicSegment p (Sum.inl w)

An end point in ℍ lies on the piece.

theorem TauCeti.UpperHalfPlane.extGeodesicSegment_subset_range_geodesicLine {g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} {p q : UpperHalfPlane ⊕ OnePoint ℝ} (hg : IsGeodesicFromTo g p q) : extGeodesicSegment p q ⊆ Set.range (geodesicLine g)

The piece between p and q lies on every geodesic line running from p to q.

@[simp]

theorem TauCeti.UpperHalfPlane.smul_extGeodesicSegment (h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (p q : UpperHalfPlane ⊕ OnePoint ℝ) : h • extGeodesicSegment p q = extGeodesicSegment (h • p) (h • q)

The piece transforms naturally under the action.

Closed half-planes are convex

theorem TauCeti.UpperHalfPlane.range_geodesicLine_subset_closure_leftHalfPlane {g k : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} (h₀ : Sum.inr (g • ↑0) ∈ extClosedLeftHalfPlane k) (h₁ : Sum.inr (g • OnePoint.infty) ∈ extClosedLeftHalfPlane k) : Set.range (geodesicLine g) ⊆ closure (leftHalfPlane k)

A geodesic line whose two ideal endpoints are weakly to the left of geodesicLine k lies in the closed left half-plane of k.

theorem TauCeti.UpperHalfPlane.geodesicLine_image_Ici_subset_closure_leftHalfPlane {g k : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} (h₀ : geodesicLine g 0 ∈ closure (leftHalfPlane k)) (h₁ : Sum.inr (g • OnePoint.infty) ∈ extClosedLeftHalfPlane k) : geodesicLine g '' Set.Ici 0 ⊆ closure (leftHalfPlane k)

A geodesic ray geodesicLine g '' [0, ∞) starting in the closed left half-plane of k, whose forward endpoint g • ∞ is weakly to the left of geodesicLine k, lies in the closed left half-plane of k.

theorem TauCeti.UpperHalfPlane.extGeodesicSegment_subset_closure_leftHalfPlane {k : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} {p q : UpperHalfPlane ⊕ OnePoint ℝ} (hp : p ∈ extClosedLeftHalfPlane k) (hq : q ∈ extClosedLeftHalfPlane k) : extGeodesicSegment p q ⊆ closure (leftHalfPlane k)

Closed half-planes are convex: the piece between two points of ℍ ∪ ∂ℍ weakly to the left of geodesicLine k lies in the closed left half-plane of k.

theorem TauCeti.UpperHalfPlane.mem_leftHalfPlane_of_mem_extGeodesicSegment {g k : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} {p q : UpperHalfPlane ⊕ OnePoint ℝ} {z : UpperHalfPlane} (hg : IsGeodesicFromTo g p q) (hp : p ∈ extClosedLeftHalfPlane k) (hq : q ∈ extClosedLeftHalfPlane k) (hne : Set.range (geodesicLine g) ≠ Set.range (geodesicLine k)) (hz : z ∈ extGeodesicSegment p q) (hzp : p ≠ Sum.inl z) (hzq : q ≠ Sum.inl z) : z ∈ leftHalfPlane k

Away from its finite endpoints, a geodesic piece in a closed half-plane lies in the open half-plane, provided its supporting line is distinct from the boundary line. This includes segments, rays and lines with ideal endpoints.