The geodesic line through two points of the upper half-plane

geodesicBetween z w is a parametrised geodesic line with z at parameter 0 and w at parameter dist z w. For distinct z and w it is the unique such line (eq_geodesicBetween_of_geodesicLine_eq), because an element of PSL(2, ℝ) fixing two distinct points is the identity, and so it transforms naturally under the action (geodesicBetween_smul). For z = w the two conditions only fix the starting point, and geodesicBetween z z is an arbitrary chosen line through z; every statement about direction therefore assumes z ≠ w. Reparametrisation is right multiplication by the dilations dilation s : z ↦ exp s * z (geodesicLine_mul_dilation) and by pslS (geodesicLine_mul_pslS); together they give the reversed line geodesicBetween w z.

Source: Katok, Fuchsian groups, geodesic flows on surfaces of constant negative curvature and symbolic coding of geodesics, Clay Math. Proc. 10 (2010), §3 p. 10 (Theorem 3.1 and the remark after it: any two points of ℍ are joined by a unique geodesic).

noncomputable def TauCeti.UpperHalfPlane.geodesicBetween (z w : UpperHalfPlane) : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ

A geodesic line from z to w: z sits at parameter 0 and w at parameter dist z w. For z ≠ w this determines the line (eq_geodesicBetween_of_geodesicLine_eq); for z = w it is an arbitrary chosen line through z.

Equations

• TauCeti.UpperHalfPlane.geodesicBetween z w = Classical.choose ⋯

@[simp]

theorem TauCeti.UpperHalfPlane.geodesicLine_geodesicBetween_zero (z w : UpperHalfPlane) : geodesicLine (geodesicBetween z w) 0 = z

The geodesic line from z to w starts at z.

@[simp]

theorem TauCeti.UpperHalfPlane.geodesicLine_geodesicBetween_dist (z w : UpperHalfPlane) : geodesicLine (geodesicBetween z w) (dist z w) = w

The geodesic line from z to w reaches w at parameter dist z w.

theorem TauCeti.UpperHalfPlane.mem_range_geodesicLine_geodesicBetween_left (z w : UpperHalfPlane) : z ∈ Set.range (geodesicLine (geodesicBetween z w))

z lies on the geodesic line from z to w.

theorem TauCeti.UpperHalfPlane.mem_range_geodesicLine_geodesicBetween_right (z w : UpperHalfPlane) : w ∈ Set.range (geodesicLine (geodesicBetween z w))

w lies on the geodesic line from z to w.

theorem TauCeti.UpperHalfPlane.eq_geodesicBetween_of_geodesicLine_eq {g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} {z w : UpperHalfPlane} (hzw : z ≠ w) (h0 : geodesicLine g 0 = z) (hd : geodesicLine g (dist z w) = w) : g = geodesicBetween z w

Uniqueness of the geodesic through two distinct points: for z ≠ w, a parametrised geodesic line with z at parameter 0 and w at parameter dist z w is geodesicBetween z w. (For z = w the two conditions coincide and do not determine the line.)

theorem TauCeti.UpperHalfPlane.geodesicBetween_smul (h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) {z w : UpperHalfPlane} (hzw : z ≠ w) : geodesicBetween (h • z) (h • w) = h * geodesicBetween z w

The geodesic line through two distinct points transforms naturally under the action.

theorem TauCeti.UpperHalfPlane.geodesicBetween_swap {z w : UpperHalfPlane} (hzw : z ≠ w) : geodesicBetween w z = geodesicBetween z w * ↑(Matrix.SpecialLinearGroup.dilation (dist z w)) * pslS

The geodesic line from w back to z is the line from z to w, shifted to start at w and reversed.

theorem TauCeti.UpperHalfPlane.range_geodesicLine_geodesicBetween_swap (z w : UpperHalfPlane) : Set.range (geodesicLine (geodesicBetween w z)) = Set.range (geodesicLine (geodesicBetween z w))

The geodesic lines from z to w and from w to z have the same image.

theorem TauCeti.UpperHalfPlane.geodesicBetween_geodesicLine_of_lt (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) {s t : ℝ} (hst : s < t) : geodesicBetween (geodesicLine g s) (geodesicLine g t) = g * ↑(Matrix.SpecialLinearGroup.dilation s)

The geodesic line from geodesicLine g s to a later point geodesicLine g t of the same line is the line g, reparametrised to start at parameter s.

theorem TauCeti.UpperHalfPlane.range_geodesicLine_geodesicBetween_of_mem {g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} {z w : UpperHalfPlane} (hz : z ∈ Set.range (geodesicLine g)) (hw : w ∈ Set.range (geodesicLine g)) (hzw : z ≠ w) : Set.range (geodesicLine (geodesicBetween z w)) = Set.range (geodesicLine g)

Two distinct points of a geodesic line determine it: the geodesic line through them has the same image.

theorem TauCeti.UpperHalfPlane.geodesicBetween_I_geodesicLine_one {d : ℝ} (hd : 0 < d) : geodesicBetween UpperHalfPlane.I (geodesicLine 1 d) = 1

The geodesic line from I up the imaginary axis is the identity's.

theorem TauCeti.UpperHalfPlane.exists_geodesicBetween_I_eq_rotation (z : UpperHalfPlane) : ∃ (θ : ℝ), geodesicBetween UpperHalfPlane.I z = ↑(Matrix.SpecialLinearGroup.rotation θ)

The geodesic line from I to any point is a rotation of the imaginary axis.

theorem TauCeti.UpperHalfPlane.eq_of_mem_range_geodesicLine {g k : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} {C : UpperHalfPlane} (hC : C ∉ Set.range (geodesicLine g)) (hCk : C ∈ Set.range (geodesicLine k)) {t₀ s : ℝ} (h₀ : geodesicLine g t₀ ∈ Set.range (geodesicLine k)) (hs : geodesicLine g s ∈ Set.range (geodesicLine k)) : s = t₀

A line through a point geodesicLine g t₀ of the line g and a point C off it meets the line g only at the parameter t₀.