The ideal endpoints of a geodesic line #
The geodesic line geodesicLine g is the g-translate of the upward imaginary axis, which runs
from the boundary point 0 to the boundary point ∞. Its ideal endpoints are therefore
g • 0 (backward) and g • ∞ (forward), for the action of PSL(2, ℝ) on OnePoint ℝ
(OnePoint.instMulActionPSL). This file describes the arc of ideal points on each side of a
geodesic line, and determines from the endpoints the side form sideForm g of HalfPlane.lean,
whose sign on ℍ is the side of the line. The open arc of ideal points to the left of the line,
boundaryLeftHalfPlane g = g • {x : ℝ | x < 0}, is described on its finite part by the same form
(coe_mem_boundaryLeftHalfPlane_iff).
In terms of the endpoints: a geodesic line from ∞ down to the real point e has
sideForm g z = e - Re z (sideForm_eq_of_smul_zero_eq_infty), one from e up to ∞ has
sideForm g z = Re z - e (sideForm_eq_of_smul_infty_eq_infty), and one between two real
points e₀ and e₁ is the semicircle on the diameter [e₀, e₁], with sideForm g a positive
multiple of (e₁ - e₀) (ρ² - |z - m|²) for the midpoint m and the half-length ρ
(exists_sideForm_eq_of_smul_zero_of_smul_infty); its left side contains ∞ exactly when
e₀ < e₁ (infty_mem_boundaryLeftHalfPlane_iff).
Finally, the endpoints determine the oriented geodesic up to reparametrisation: two elements with
the same backward and forward endpoints differ by a dilation on the right
(exists_eq_mul_dilation_of_smul_zero_eq_of_smul_infty_eq), and an element is determined by the
point at parameter 0 and the forward endpoint
(eq_of_geodesicLine_zero_eq_of_smul_infty_eq).
Main declarations #
TauCeti.UpperHalfPlane.sideForm_eq_of_smul_zero_eq_infty,sideForm_eq_of_smul_infty_eq_infty,exists_sideForm_eq_of_smul_zero_of_smul_infty: the side form of a geodesic line in terms of its endpoints.TauCeti.UpperHalfPlane.boundaryLeftHalfPlane g: the open arc of ideal points to the left ofgeodesicLine g, withcoe_mem_boundaryLeftHalfPlane_iffandinfty_mem_boundaryLeftHalfPlane_iff.TauCeti.UpperHalfPlane.exists_smul_zero_eq_and_smul_infty_eq: every ordered pair of distinct ideal points are the endpoints of a geodesic line.TauCeti.UpperHalfPlane.exists_geodesicLine_zero_eq_and_smul_infty_eq: a geodesic line from any point ofℍto any ideal point.TauCeti.UpperHalfPlane.strictMono_re_geodesicLine: along a semicircle frome₀toe₁ > e₀, the real part increases strictly, betweene₀ande₁.UpperHalfPlane.toPoint_smul_infty: the affine maptoPoint Afixes the ideal point∞.
Source #
Walkden, Hyperbolic geometry (MATH32051 lecture notes, Manchester 2019), §4.1 (the action of a
Möbius transformation on ∂ℍ, γ(∞) = a/c, γ(-d/c) = ∞) and §4.3 (geodesics are determined by
their endpoints; Lemma 4.3.1, the semicircle with endpoints ζ₋ < ζ₊ is carried to the imaginary
axis by z ↦ (z - ζ₊)/(z - ζ₋)); 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).
Dilations and pslS on the ideal boundary #
A dilation fixes the ideal point 0.
A dilation fixes the ideal point ∞.
A dilation acts on the real ideal points as multiplication by exp s.
pslS, the class of z ↦ -1/z, sends the ideal point 0 to ∞.
pslS, the class of z ↦ -1/z, sends the ideal point ∞ to 0.
Conjugating a dilation by pslS inverts it.
The endpoints of a representative #
The ideal arc on the left of a geodesic line #
The open arc of ideal points to the left of geodesicLine g: the g-translate of the
negative real numbers.
Equations
Instances For
Restatement of the body of boundaryLeftHalfPlane, unfolded from the def.
Translating the left ideal arc of g by h gives the left ideal arc of h * g.
Reparametrising a geodesic line by a dilation does not change its left ideal arc.
A real ideal point lies on the left ideal arc of g exactly when the side form is negative
there.
The backward endpoint of a geodesic line is not on its left ideal arc.
The forward endpoint of a geodesic line is not on its left ideal arc.
The backward endpoint of a geodesic line is a zero of its side form.
The forward endpoint of a geodesic line is a zero of its side form.
The side form in terms of the endpoints #
A geodesic line running from ∞ down to the real point e is the vertical line Re z = e,
with side form e - Re z: its left half-plane is {Re z > e}.
A geodesic line running from the real point e up to ∞ is the vertical line Re z = e,
with side form Re z - e: its left half-plane is {Re z < e}.
A geodesic line running from the real point e₀ to the real point e₁ is the semicircle on
the diameter [e₀, e₁]: its side form is a positive multiple of (e₁ - e₀) (ρ² - |z - m|²), for
the midpoint m = (e₀ + e₁) / 2 and the half-length ρ = (e₁ - e₀) / 2.
The ideal point ∞ lies on the left of the semicircle from e₀ to e₁ exactly when the
semicircle runs from left to right, e₀ < e₁.
Along a semicircle running from e₀ to e₁ > e₀, the real part increases strictly.
Along a semicircle running from e₀ to e₁ > e₀, the real part stays above e₀.
Along a semicircle running from e₀ to e₁ > e₀, the real part stays below e₁.
Existence and uniqueness from the endpoints #
Every ordered pair of distinct ideal points are the backward and forward endpoints of a geodesic line.
An element of PSL(2, ℝ) fixing the ideal points 0 and ∞ is a dilation.
Two elements with the same backward and the same forward endpoint differ by a dilation on the right: their geodesic lines are reparametrisations of each other.
A geodesic line from any point of ℍ to any ideal point, starting at parameter 0.
An element of PSL(2, ℝ) is determined by the point of its geodesic line at parameter 0
together with its forward endpoint.
The affine map toPoint A, z ↦ Re A + Im A · z, fixes the ideal point ∞.