Geodesic lines in the upper half-plane, transported from the imaginary axis

Mathlib's UpperHalfPlane.isometry_vertical_line already exhibits the imaginary axis, in its upward unit-speed parametrisation t ↦ mk ⟨0, exp t⟩ _, as a geodesic line, and Tau Ceti's IsIsometricSMul PSL(2, ℝ) ℍ (ProperAction.lean) already gives the isometric action of the group Fuchsian groups are subgroups of. The first part of this file composes the two: the PSL(2, ℝ)-translate of the imaginary axis by any g is again a geodesic line, and every one of these is unit-speed (isometry_geodesicLine), hence injective (geodesicLine_injective) and at explicit distance |s - t| between its parameters (dist_geodesicLine).

This is the transport step behind the classical description of hyperbolic geodesics in ℍ as vertical lines and semicircles centred on the real axis: as a set, the image of the map geodesicLine g is the g-translate of the imaginary axis, which is a vertical line when the representing matrix's lower-left entry g 1 0 or lower-right entry g 1 1 is 0 (equivalently, g sends one of the imaginary axis's two boundary points, 0 and the point at infinity, to the point at infinity) and a semicircle centred on the real axis otherwise. That case split is not proved here.

The second part is two-point transitivity: any two points z, w lie on a common geodesic line, with z at parameter 0 and w at parameter dist z w (exists_geodesicLine_zero_eq_and_dist_eq). Transitivity of the action puts z at I; a rotation about I (Rotation.lean) then moves w onto the imaginary axis, which is the geodesic line of the identity (range_geodesicLine_one), and if w lands below I the involution pslS reverses the axis (geodesicLine_mul_pslS).

Main declarations

• TauCeti.UpperHalfPlane.geodesicLine g — the imaginary axis in its upward unit-speed parametrisation, moved by g: the map t ↦ g • UpperHalfPlane.mk ⟨0, exp t⟩ _. geodesicLine_one_apply and geodesicLine_zero give its value at g = 1 and at t = 0.
• TauCeti.UpperHalfPlane.isometry_geodesicLine — geodesicLine g is an isometric embedding of ℝ, hence injective (geodesicLine_injective).
• TauCeti.UpperHalfPlane.dist_geodesicLine — the distance between two of its points is |s - t|.
• TauCeti.UpperHalfPlane.smul_geodesicLine — further translating a geodesic line by h gives the geodesic line of h * g, pointwise; TauCeti.UpperHalfPlane.smul_range_geodesicLine is the same fact at the level of the line as a set, so these lines are permuted, not merely mapped into each other, by the PSL(2, ℝ)-action.
• TauCeti.UpperHalfPlane.exists_geodesicLine_zero_eq — a geodesic line through any prescribed point of ℍ.
• TauCeti.UpperHalfPlane.range_geodesicLine_one and TauCeti.UpperHalfPlane.range_geodesicLine — every geodesic line, as a set, is a g-translate of the imaginary axis {z | z.re = 0}.
• TauCeti.UpperHalfPlane.mem_range_geodesicLine_iff — membership test for a geodesic line, without unfolding the smul-image.
• TauCeti.UpperHalfPlane.geodesicLine_mul_pslS — multiplying the representative by pslS reverses the parametrisation of a geodesic line; range_geodesicLine_mul_pslS is the same fact at the level of the line as a set, which is unchanged.
• TauCeti.UpperHalfPlane.geodesicLine_mul_dilation — multiplying the representative by the dilation Matrix.SpecialLinearGroup.dilation s shifts the parameter by s; range_geodesicLine_mul_dilation is the same fact at the level of the line as a set, which is unchanged. geodesicLine_one_eq_dilation_smul_I is the underlying description of the imaginary axis as the orbit of I under the dilations.
• TauCeti.UpperHalfPlane.exists_geodesicLine_zero_eq_and_dist_eq — two-point transitivity: a geodesic line with z at parameter 0 and w at parameter dist z w, for any z, w; exists_mem_range_geodesicLine_and_mem_range is the same at the level of the line as a set.
• UpperHalfPlane.re_geodesicLine_toPoint, UpperHalfPlane.im_geodesicLine_toPoint: the upward vertical geodesicLine (toPoint A) keeps the real part of A and has height Im A · exp t.

Geodesic lines as translates of the imaginary axis

noncomputable def TauCeti.UpperHalfPlane.geodesicLine (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (t : ℝ) : UpperHalfPlane

The geodesic line obtained by moving the (upward, unit-speed) imaginary axis by g.

Equations

• TauCeti.UpperHalfPlane.geodesicLine g t = g • { coe := { re := 0, im := Real.exp t }, coe_im_pos := ⋯ }

theorem TauCeti.UpperHalfPlane.geodesicLine_def (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (t : ℝ) : geodesicLine g t = g • { coe := { re := 0, im := Real.exp t }, coe_im_pos := ⋯ }

theorem TauCeti.UpperHalfPlane.geodesicLine_one_apply (t : ℝ) : geodesicLine 1 t = { coe := { re := 0, im := Real.exp t }, coe_im_pos := ⋯ }

The geodesic line of the identity is the upward unit-speed imaginary axis.

theorem TauCeti.UpperHalfPlane.isometry_geodesicLine (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) : Isometry (geodesicLine g)

theorem TauCeti.UpperHalfPlane.geodesicLine_injective (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) : Function.Injective (geodesicLine g)

@[simp]

theorem TauCeti.UpperHalfPlane.dist_geodesicLine (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (s t : ℝ) : dist (geodesicLine g s) (geodesicLine g t) = |s - t|

theorem TauCeti.UpperHalfPlane.geodesicLine_zero (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) : geodesicLine g 0 = g • UpperHalfPlane.I

@[simp]

theorem TauCeti.UpperHalfPlane.smul_geodesicLine (h g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (t : ℝ) : h • geodesicLine g t = geodesicLine (h * g) t

Translating a geodesic line by h gives the geodesic line of h * g, pointwise.

@[simp]

theorem TauCeti.UpperHalfPlane.smul_range_geodesicLine (h g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) : h • Set.range (geodesicLine g) = Set.range (geodesicLine (h * g))

The same fact as smul_geodesicLine, at the level of the line as a set: the PSL(2, ℝ)-action permutes these lines rather than merely mapping into their union.

theorem TauCeti.UpperHalfPlane.exists_geodesicLine_zero_eq (z : UpperHalfPlane) : ∃ (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ), geodesicLine g 0 = z

A geodesic line through any prescribed point, at its own parameter 0.

theorem TauCeti.UpperHalfPlane.range_geodesicLine_one : Set.range (geodesicLine 1) = {z : UpperHalfPlane | z.re = 0}

The geodesic line of the identity, as a set, is the imaginary axis {z | z.re = 0}.

theorem TauCeti.UpperHalfPlane.range_geodesicLine (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) : Set.range (geodesicLine g) = g • {z : UpperHalfPlane | z.re = 0}

Every geodesic line, as a set, is a g-translate of the imaginary axis.

theorem TauCeti.UpperHalfPlane.mem_range_geodesicLine_iff (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (z : UpperHalfPlane) : z ∈ Set.range (geodesicLine g) ↔ (g⁻¹ • z).re = 0

A point z lies on the geodesic line of g iff g⁻¹ • z lies on the imaginary axis.

@[simp]

theorem TauCeti.UpperHalfPlane.geodesicLine_mul_pslS (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (t : ℝ) : geodesicLine (g * pslS) t = geodesicLine g (-t)

Multiplying the representative by pslS reverses the parametrisation of a geodesic line: z ↦ -1/z runs the upward imaginary axis downward.

@[simp]

theorem TauCeti.UpperHalfPlane.range_geodesicLine_mul_pslS (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) : Set.range (geodesicLine (g * pslS)) = Set.range (geodesicLine g)

The geodesic lines of g and g * pslS have the same image: z ↦ -1/z fixes the imaginary axis setwise, reversing its direction. (The two half-planes it bounds are swapped instead.)

Dilations along a geodesic line

theorem TauCeti.UpperHalfPlane.geodesicLine_one_eq_dilation_smul_I (t : ℝ) : geodesicLine 1 t = Matrix.SpecialLinearGroup.dilation t • UpperHalfPlane.I

The imaginary axis is the orbit of I under the dilations.

@[simp]

theorem TauCeti.UpperHalfPlane.geodesicLine_mul_dilation (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (s t : ℝ) : geodesicLine (g * ↑(Matrix.SpecialLinearGroup.dilation s)) t = geodesicLine g (s + t)

Right multiplication by a dilation shifts the parameter of a geodesic line.

@[simp]

theorem TauCeti.UpperHalfPlane.range_geodesicLine_mul_dilation (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (s : ℝ) : Set.range (geodesicLine (g * ↑(Matrix.SpecialLinearGroup.dilation s))) = Set.range (geodesicLine g)

Shifting the parameter does not change a geodesic line as a set.

Two-point transitivity

theorem TauCeti.UpperHalfPlane.exists_geodesicLine_zero_eq_and_dist_eq (z w : UpperHalfPlane) : ∃ (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ), geodesicLine g 0 = z ∧ geodesicLine g (dist z w) = w

Two-point transitivity on parametrised geodesic lines. Any two points z, w lie on a common geodesic line, with z at parameter 0 and w at parameter dist z w.

theorem TauCeti.UpperHalfPlane.exists_mem_range_geodesicLine_and_mem_range (z w : UpperHalfPlane) : ∃ (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ), z ∈ Set.range (geodesicLine g) ∧ w ∈ Set.range (geodesicLine g)

Any two points lie on a common geodesic line.

@[simp]

theorem UpperHalfPlane.re_geodesicLine_toPoint (A : UpperHalfPlane) (t : ℝ) : (TauCeti.UpperHalfPlane.geodesicLine A.toPoint t).re = A.re

The upward vertical through A keeps the real part of A.

@[simp]

theorem UpperHalfPlane.im_geodesicLine_toPoint (A : UpperHalfPlane) (t : ℝ) : (TauCeti.UpperHalfPlane.geodesicLine A.toPoint t).im = A.im * Real.exp t

The upward vertical through A reaches height Im A · exp t at parameter t.