Rays to points of ℍ ∪ ∂ℍ

UpperHalfPlane.rayToward A p is the geodesic line leaving A ∈ ℍ at parameter 0 towards a point p ≠ A of ℍ ∪ ∂ℍ: geodesicBetween A B for p = B ∈ ℍ, and for an ideal point ξ the unique geodesic line with A at parameter 0 and forward endpoint ξ. For p = A it is an arbitrary geodesic line through A, and the ray interpretation needs .inl A ≠ p. The ray towards ∞ is the upward vertical UpperHalfPlane.toPoint A through A, a ray runs from its base point to its target, and rays are equivariant under PSL(2, ℝ).

Main declarations

• UpperHalfPlane.rayToward A p: the geodesic ray from A ∈ ℍ towards p ∈ ℍ ∪ ∂ℍ, p ≠ A.
• UpperHalfPlane.rayToward_inr_infty, UpperHalfPlane.isGeodesicFromTo_rayToward, TauCeti.UpperHalfPlane.rayToward_smul: the ray towards ∞ is the upward vertical; a ray runs from its base point to its target; rays are equivariant.
• UpperHalfPlane.rayToward_eq_geodesicBetween: a ray is the geodesic from its base point to its point at parameter 1.

Source

Walkden, Hyperbolic geometry (MATH32051 lecture notes, Manchester 2019), §7.1 (the unique geodesic through two points of ℍ ∪ ∂ℍ).

noncomputable def UpperHalfPlane.rayToward (A : UpperHalfPlane) (p : UpperHalfPlane ⊕ OnePoint ℝ) : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ

The geodesic line leaving A at parameter 0 towards a point p ≠ A of ℍ ∪ ∂ℍ: geodesicBetween A B for p = B ∈ ℍ, and for an ideal point ξ the geodesic line with A at parameter 0 and forward endpoint ξ. For p = A it is geodesicBetween A A, an arbitrary geodesic line through A, with no direction towards the target.

Equations

• A.rayToward p = Sum.elim (TauCeti.UpperHalfPlane.geodesicBetween A) (fun (ξ : OnePoint ℝ) => ⋯.choose) p

@[simp]

theorem UpperHalfPlane.rayToward_inl (A B : UpperHalfPlane) : A.rayToward (Sum.inl B) = TauCeti.UpperHalfPlane.geodesicBetween A B

@[simp]

theorem UpperHalfPlane.geodesicLine_rayToward_zero (A : UpperHalfPlane) (p : UpperHalfPlane ⊕ OnePoint ℝ) : TauCeti.UpperHalfPlane.geodesicLine (A.rayToward p) 0 = A

A ray starts at its base point.

@[simp]

theorem UpperHalfPlane.rayToward_inr_smul_infty (A : UpperHalfPlane) (ξ : OnePoint ℝ) : A.rayToward (Sum.inr ξ) • OnePoint.infty = ξ

A ray towards an ideal point has it as forward endpoint.

@[simp]

theorem UpperHalfPlane.rayToward_inr_infty (A : UpperHalfPlane) : A.rayToward (Sum.inr OnePoint.infty) = A.toPoint

The ray from A towards ∞ is the upward vertical through A.

theorem UpperHalfPlane.isGeodesicFromTo_rayToward {A : UpperHalfPlane} {p : UpperHalfPlane ⊕ OnePoint ℝ} (hAp : Sum.inl A ≠ p) : TauCeti.UpperHalfPlane.IsGeodesicFromTo (A.rayToward p) (Sum.inl A) p

A ray from A towards p ≠ A runs from A to p.

theorem UpperHalfPlane.rayToward_eq_geodesicBetween (A : UpperHalfPlane) (p : UpperHalfPlane ⊕ OnePoint ℝ) : A.rayToward p = TauCeti.UpperHalfPlane.geodesicBetween A (TauCeti.UpperHalfPlane.geodesicLine (A.rayToward p) 1)

A ray is the geodesic from its base point to its point at parameter 1.

theorem TauCeti.UpperHalfPlane.rayToward_smul (h : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) {A : UpperHalfPlane} {p : UpperHalfPlane ⊕ OnePoint ℝ} (hAp : Sum.inl A ≠ p) : (h • A).rayToward (h • p) = h * A.rayToward p

Rays transform naturally under the action.