Points of ℍ ∪ ∂ℍ as complex numbers

Points of ℍ ∪ ∂ℍ are modelled as ℍ ⊕ OnePoint ℝ: a point of ℍ (Sum.inl) or an ideal point (Sum.inr). Every such point other than ∞ is a complex number of nonnegative imaginary part, toComplex p, and toComplex is injective away from ∞ (toComplex_injOn).

Main declarations

• TauCeti.UpperHalfPlane.toComplex: a point of ℍ ⊕ OnePoint ℝ as a complex number, with im_toComplex_nonneg and toComplex_injOn.

Source

Walkden, Hyperbolic geometry (MATH32051 lecture notes, Manchester 2019), §7.1 (the closure ℍ ∪ ∂ℍ of the upper half-plane, with ∂ℍ = ℝ ∪ {∞}).

def TauCeti.UpperHalfPlane.toComplex : UpperHalfPlane ⊕ OnePoint ℝ → ℂ

A point of ℍ ∪ ∂ℍ other than ∞, as a complex number of nonnegative imaginary part: a point of ℍ is itself and a real ideal point x is x. The value at ∞ is 0 (toComplex_inr_infty), and carries no meaning.

Equations

• TauCeti.UpperHalfPlane.toComplex = Sum.elim UpperHalfPlane.coe fun (ξ : OnePoint ℝ) => ↑(ξ.elim 0 id)

@[simp]

theorem TauCeti.UpperHalfPlane.toComplex_inl (z : UpperHalfPlane) : toComplex (Sum.inl z) = ↑z

@[simp]

theorem TauCeti.UpperHalfPlane.toComplex_inr_coe (x : ℝ) : toComplex (Sum.inr ↑x) = ↑x

@[simp]

theorem TauCeti.UpperHalfPlane.toComplex_inr_infty : toComplex (Sum.inr OnePoint.infty) = 0

The junk value of toComplex at ∞.

theorem TauCeti.UpperHalfPlane.im_toComplex_nonneg (p : UpperHalfPlane ⊕ OnePoint ℝ) : 0 ≤ (toComplex p).im

The imaginary part of a point of ℍ ∪ ∂ℍ is nonnegative.

theorem TauCeti.UpperHalfPlane.toComplex_injOn : Set.InjOn toComplex {p : UpperHalfPlane ⊕ OnePoint ℝ | p ≠ Sum.inr OnePoint.infty}

Two points of ℍ ∪ ∂ℍ other than ∞ with the same complex value are equal.