Oriented geodesics between points of ℍ ∪ ∂ℍ #
Points of ℍ ∪ ∂ℍ are modelled as ℍ ⊕ OnePoint ℝ: a point of ℍ (Sum.inl) or an ideal
point (Sum.inr), on which PSL(2, ℝ) acts componentwise. Any two distinct such points lie on a
unique geodesic (Walkden §7.1). IsGeodesicFromTo g p q says that the geodesic line of g runs
from p to q: a point of ℍ lies on the line, an ideal point is its backward endpoint g • 0
(for p) or forward endpoint g • ∞ (for q), and two points of ℍ occur in this order.
Such a g exists for p ≠ q (exists_isGeodesicFromTo) and is unique up to reparametrisation
(IsGeodesicFromTo.exists_eq_mul_dilation), so geodesicFromTo p q, a choice of it, has
well-defined half-planes and ideal arcs.
extLeftHalfPlane g is the open left half-plane of g together with the open arc of ideal points
on its left, as a subset of ℍ ⊕ OnePoint ℝ: the points of ℍ ∪ ∂ℍ strictly to the left of the
line. Reading a point of ℍ ⊕ OnePoint ℝ other than ∞ as a complex number (toComplex, from
Extended.lean), the side form sideForm g of HalfPlane.lean can be evaluated at vertices: it
is negative at points strictly to the left of a line
(sideForm_toComplex_neg_of_mem_extLeftHalfPlane), and zero at the two points a line runs between
(IsGeodesicFromTo.sideForm_toComplex_left, IsGeodesicFromTo.sideForm_toComplex_right).
Geodesic lines with the same image have the same extended left half-plane, up to orientation
reversal (extLeftHalfPlane_eq_or_eq_mul_pslS_of_range_eq).
Main declarations #
TauCeti.UpperHalfPlane.IsGeodesicFromTo g p q: the geodesic line ofgruns fromptoq.TauCeti.UpperHalfPlane.geodesicFromTo p q: a geodesic line fromptoq(isGeodesicFromTo_geodesicFromTo).TauCeti.UpperHalfPlane.extLeftHalfPlane g: the points ofℍ ∪ ∂ℍstrictly to the left ofgeodesicLine g.TauCeti.UpperHalfPlane.extClosedLeftHalfPlane g: the points ofℍ ∪ ∂ℍweakly to the left ofgeodesicLine g, adding the line and its two endpoints.TauCeti.UpperHalfPlane.IsGeodesicFromTo.re_toComplex_lt: on a geodesic with∞on its left, points occur from left to right.TauCeti.UpperHalfPlane.IsGeodesicFromTo.re_toComplex_lt_iff: a geodesic line through two points with distinct real parts passes its points in order.TauCeti.UpperHalfPlane.IsGeodesicFromTo.sideForm_eq_of_inr_infty_left,TauCeti.UpperHalfPlane.IsGeodesicFromTo.sideForm_eq_of_inr_infty_right: a geodesic line running from or to∞is a vertical line.TauCeti.UpperHalfPlane.exists_sideForm_eq_of_infty_mem_boundaryLeftHalfPlane: a geodesic line with∞strictly on its left is a semicircle.
Source #
Walkden, Hyperbolic geometry (MATH32051 lecture notes, Manchester 2019), §7.1 (for
z, w ∈ ℍ ∪ ∂ℍ there is a unique geodesic through both; [z, w] is the part between them) and
§4.3 (geodesics are determined by their endpoints; Lemma 4.3.1, a semicircle with endpoints
ζ₋ < ζ₊); Katok, Fuchsian groups, geodesic flows on surfaces of constant negative curvature and
symbolic coding of geodesics, Clay Math. Proc. 10 (2010), Theorem 3.1 p. 10 (geodesics are
semicircles and vertical lines).
Geodesic lines running between two points of ℍ ∪ ∂ℍ #
The geodesic line of g runs from p to q, for points p, q of ℍ ∪ ∂ℍ: a point of ℍ
lies on the line, an ideal starting point is the backward endpoint g • 0, an ideal end point is
the forward endpoint g • ∞, and two points of ℍ occur in this order along the line.
Equations
- TauCeti.UpperHalfPlane.IsGeodesicFromTo g (Sum.inl z) (Sum.inl w) = ∃ (s : ℝ) (t : ℝ), s < t ∧ TauCeti.UpperHalfPlane.geodesicLine g s = z ∧ TauCeti.UpperHalfPlane.geodesicLine g t = w
- TauCeti.UpperHalfPlane.IsGeodesicFromTo g (Sum.inl z) (Sum.inr η) = (z ∈ Set.range (TauCeti.UpperHalfPlane.geodesicLine g) ∧ g • OnePoint.infty = η)
- TauCeti.UpperHalfPlane.IsGeodesicFromTo g (Sum.inr ξ) (Sum.inl w) = (g • ↑0 = ξ ∧ w ∈ Set.range (TauCeti.UpperHalfPlane.geodesicLine g))
- TauCeti.UpperHalfPlane.IsGeodesicFromTo g (Sum.inr ξ) (Sum.inr η) = (g • ↑0 = ξ ∧ g • OnePoint.infty = η)
Instances For
The two points a geodesic line runs between are distinct.
A point of ℍ from which a geodesic line runs lies on the line.
A point of ℍ to which a geodesic line runs lies on the line.
An ideal point from which a geodesic line runs is its backward endpoint.
An ideal point to which a geodesic line runs is its forward endpoint.
The geodesic from z to w runs from z to w.
Translating by h carries a geodesic line from p to q to one from h • p to h • q.
Reparametrising by a dilation does not change the points a geodesic line runs between.
Reversing the orientation of a geodesic line by pslS swaps the points it runs between.
Any two distinct points of ℍ ∪ ∂ℍ are joined by a geodesic line.
Uniqueness of the geodesic through two points of ℍ ∪ ∂ℍ: two geodesic lines running
from p to q differ by a reparametrisation.
Two geodesic lines running from p to q have the same left half-plane.
Two geodesic lines running from p to q have the same left ideal arc.
Two geodesic lines running from p to q have the same image.
The chosen geodesic from p to q #
A geodesic line from p to q, for distinct points p, q of ℍ ∪ ∂ℍ
(isGeodesicFromTo_geodesicFromTo); the identity if p = q.
Equations
- TauCeti.UpperHalfPlane.geodesicFromTo p q = if h : ∃ (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ), TauCeti.UpperHalfPlane.IsGeodesicFromTo g p q then h.choose else 1
Instances For
The junk value of geodesicFromTo on equal points.
geodesicFromTo p q runs from p to q.
Between two points of ℍ, geodesicFromTo has the half-planes of geodesicBetween.
The left half-plane of geodesicFromTo transforms naturally under the action.
Points of ℍ ∪ ∂ℍ strictly to the left of a geodesic line #
The points of ℍ ∪ ∂ℍ strictly to the left of geodesicLine g: the open left half-plane
together with the open arc of ideal points on its left.
Equations
Instances For
Translating the points strictly to the left of g by h gives those strictly to the left
of h * g.
Two geodesic lines running from p to q have the same points strictly on their left.
Geodesic lines with the same image have the same extended left half-plane, possibly after reversing the orientation of one of them.
The points strictly to the left of geodesicFromTo transform naturally under the action.
A point strictly to the left of a geodesic line is not one of the two points it runs between.
A point strictly to the left of a geodesic line is not one of the two points it runs between.
Points of ℍ ∪ ∂ℍ weakly to the left of a geodesic line #
The points of ℍ ∪ ∂ℍ weakly to the left of geodesicLine g: the closed left half-plane
together with the closed arc of ideal points on its left, which is the open arc
boundaryLeftHalfPlane g together with the two endpoints g • 0 and g • ∞ of the line.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A point of ℍ is weakly to the left of geodesicLine g exactly when it lies in the closed
left half-plane.
An ideal point is weakly to the left of geodesicLine g exactly when it is one of the two
endpoints g • 0, g • ∞ or lies on the open ideal arc to the left.
Translating the points weakly to the left of g by h gives those weakly to the left of
h * g.
A point strictly to the left of a geodesic line is weakly to its left.
The point a geodesic line runs from is weakly to its left.
The point a geodesic line runs to is weakly to its left.
The side form at points of ℍ ∪ ∂ℍ #
A point other than ∞ strictly to the left of a geodesic line is where its side form is
negative.
The side form of a geodesic line vanishes at the point it runs from, unless that point is
∞.
The side form of a geodesic line vanishes at the point it runs to, unless that point is
∞.
A point other than ∞ weakly to the left of a geodesic line is where its side form is
nonpositive.
On a geodesic line with ∞ strictly on its left, the points it runs between occur from left
to right.
For a geodesic line running from p to q and from p to r, where p and q are not ∞
and have distinct real parts, the real part of toComplex r lies on the same side of Re p as
Re q.
Geodesic lines with ∞ as an endpoint or strictly on their left #
A geodesic line running from ∞ to a point q ≠ ∞ is the vertical line through q, with
side form Re q - Re z.
A geodesic line running from a point p ≠ ∞ to ∞ is the vertical line through p, with
side form Re z - Re p.
A geodesic line with ∞ strictly on its left is a semicircle: its side form is a positive
multiple of ρ² - |z - m|² for its centre m and radius ρ > 0.