Heights after moving a real boundary point to ∞ #
If g ∈ PSL(2, ℝ) carries the real boundary point ξ to ∞, then a lift of g has lower row
proportional to (1, -ξ), so g acts as z ↦ (az + b) / (c (z - ξ)). Its effect on heights is
therefore Im (g • z) = Im z / (c² |z - ξ|²). For A > 0 the set {z | A < Im (g • z)} is a
horodisc at ξ, a Euclidean disc tangent to ℝ at ξ (for A ≤ 0 it is all of ℍ), and this
formula is how a horodisc at a real point is compared with Euclidean distances to that point.
Main result #
TauCeti.UpperHalfPlane.exists_im_smul_eq_div_of_smul_coe_eq_infty: the height formula above.
theorem
TauCeti.UpperHalfPlane.exists_im_smul_eq_div_of_smul_coe_eq_infty
{g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ}
{ξ : ℝ}
(hg : g • ↑ξ = OnePoint.infty)
:
If g ∈ PSL(2, ℝ) carries the real boundary point ξ to ∞, then there is c > 0 such that
Im (g • z) = Im z / (c |z - ξ|²) for every z ∈ ℍ; here c is the square of the lower-left
entry of a lift of g.