The disc coordinate centred at a point of the upper half-plane

For z ∈ ℍ, the Cayley transform τ ↦ (τ - z) / (τ - conj z) is a bijection from the upper half-plane onto the open unit disc sending z to 0, with inverse w ↦ (z - conj z * w) / (1 - w); its modulus is tanh (d / 2) for the hyperbolic distance d to z. In this coordinate every matrix of positive determinant fixing z is a rotation of the disc about 0: if g • z = z, then discCoordinate z (g • τ) = conj (denom g z) / denom g z * discCoordinate z τ.

This is the local linearizing coordinate at a point with nontrivial stabilizer: the multiplier conj (denom g z) / denom g z is a complex number of modulus one, and it is exactly the derivative Matrix.ProjectiveSpecialLinearGroup.smulDeriv of τ ↦ g • τ at its fixed point z.

Because the modulus of the disc coordinate is tanh of half the hyperbolic distance to z, the hyperbolic discs about z are precisely the preimages of the Euclidean discs about 0.

Main declarations

• UpperHalfPlane.discCoordinate: the Cayley transform centred at z.
• UpperHalfPlane.discCoordinate_eq_zero_iff and UpperHalfPlane.discCoordinate_injective.
• UpperHalfPlane.norm_discCoordinate: the modulus of the disc coordinate is tanh (dist τ z / 2), so the coordinate takes values in the unit disc.
• UpperHalfPlane.mdifferentiable_discCoordinate and UpperHalfPlane.analyticOnNhd_discCoordinateHomeomorph_symm: the coordinate and its explicit inverse are holomorphic.
• UpperHalfPlane.discCoordinateHomeomorph: the disc coordinate as a homeomorphism ℍ ≃ₜ 𝔻, with explicit inverse, and UpperHalfPlane.range_discCoordinate: its range is the open unit disc.
• UpperHalfPlane.mem_ball_iff_norm_discCoordinate_lt and UpperHalfPlane.image_discCoordinate_ball: the hyperbolic disc of radius ε about z is carried onto the Euclidean disc of radius tanh (ε / 2) about 0.
• UpperHalfPlane.discCoordinate_smul_of_smul_eq_self: a matrix of positive determinant fixing z acts in the disc coordinate by multiplication by conj (denom g z) / denom g z, with the SL(2, ℝ) specialization UpperHalfPlane.discCoordinate_specialLinearGroup_smul_of_smul_eq_self and the effective projective form UpperHalfPlane.discCoordinate_psl_smul_of_smul_eq_self.

References

• S. Katok, Fuchsian Groups, University of Chicago Press, 1992, §§1.1 and 2.1.
• H. Farkas and I. Kra, Riemann Surfaces, 2nd ed., Springer, 1992, Chapter I §4.

noncomputable def UpperHalfPlane.discCoordinate (z τ : UpperHalfPlane) : ℂ

The disc coordinate centred at z: the Cayley transform τ ↦ (τ - z) / (τ - conj z), which maps the upper half-plane injectively into the unit disc and sends z to 0.

Equations

• z.discCoordinate τ = (↑τ - ↑z) / (↑τ - (starRingEnd ℂ) ↑z)

theorem UpperHalfPlane.discCoordinate_def (z τ : UpperHalfPlane) : z.discCoordinate τ = (↑τ - ↑z) / (↑τ - (starRingEnd ℂ) ↑z)

theorem UpperHalfPlane.coe_sub_conj_ne_zero (z τ : UpperHalfPlane) : ↑τ - (starRingEnd ℂ) ↑z ≠ 0

The denominator of the disc coordinate does not vanish: conj z lies in the lower half-plane.

@[simp]

theorem UpperHalfPlane.discCoordinate_eq_zero_iff {z τ : UpperHalfPlane} : z.discCoordinate τ = 0 ↔ τ = z

The disc coordinate centred at z vanishes exactly at its centre z.

@[simp]

theorem UpperHalfPlane.discCoordinate_self (z : UpperHalfPlane) : z.discCoordinate z = 0

theorem UpperHalfPlane.discCoordinate_injective (z : UpperHalfPlane) : Function.Injective z.discCoordinate

The disc coordinate centred at any point is injective on the upper half-plane.

theorem UpperHalfPlane.norm_discCoordinate (z τ : UpperHalfPlane) : ‖z.discCoordinate τ‖ = Real.tanh (dist τ z / 2)

The modulus of the disc coordinate centred at z is tanh (d / 2), where d is the hyperbolic distance to z.

theorem UpperHalfPlane.norm_discCoordinate_lt_one (z τ : UpperHalfPlane) : ‖z.discCoordinate τ‖ < 1

The disc coordinate takes values in the open unit disc.

theorem UpperHalfPlane.continuous_discCoordinate (z : UpperHalfPlane) : Continuous z.discCoordinate

The disc coordinate centred at z is continuous.

theorem UpperHalfPlane.mdifferentiable_discCoordinate (z : UpperHalfPlane) : MDiff z.discCoordinate

The disc coordinate centred at z is holomorphic.

theorem UpperHalfPlane.analyticOnNhd_discCoordinateHomeomorph_symm (z : UpperHalfPlane) : AnalyticOnNhd ℂ (fun (w : ℂ) => (↑z - (starRingEnd ℂ) ↑z * w) / (1 - w)) (Metric.ball 0 1)

The explicit inverse of the disc coordinate is holomorphic on the open unit disc.

noncomputable def UpperHalfPlane.discCoordinateHomeomorph (z : UpperHalfPlane) : UpperHalfPlane ≃ₜ Complex.UnitDisc

The disc coordinate centred at z as a homeomorphism between the upper half-plane and the open unit disc 𝔻, with inverse w ↦ (z - conj z * w) / (1 - w). Both directions are holomorphic, by UpperHalfPlane.mdifferentiable_discCoordinate and UpperHalfPlane.analyticOnNhd_discCoordinateHomeomorph_symm.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem UpperHalfPlane.coe_discCoordinateHomeomorph_apply (z τ : UpperHalfPlane) : ↑(z.discCoordinateHomeomorph τ) = z.discCoordinate τ

@[simp]

theorem UpperHalfPlane.coe_discCoordinateHomeomorph_symm_apply (z : UpperHalfPlane) (w : Complex.UnitDisc) : ↑(z.discCoordinateHomeomorph.symm w) = (↑z - (starRingEnd ℂ) ↑z * ↑w) / (1 - ↑w)

@[simp]

theorem UpperHalfPlane.discCoordinate_discCoordinateHomeomorph_symm (z : UpperHalfPlane) (w : Complex.UnitDisc) : z.discCoordinate (z.discCoordinateHomeomorph.symm w) = ↑w

The disc coordinate recovers the point of the unit disc it came from.

theorem UpperHalfPlane.range_discCoordinate (z : UpperHalfPlane) : Set.range z.discCoordinate = Metric.ball 0 1

The range of the disc coordinate centred at any point is the open unit disc.

theorem UpperHalfPlane.mem_ball_iff_norm_discCoordinate_lt {z τ : UpperHalfPlane} {ε : ℝ} : τ ∈ Metric.ball z ε ↔ ‖z.discCoordinate τ‖ < Real.tanh (ε / 2)

A point lies in the hyperbolic disc of radius ε about z exactly when its disc coordinate has modulus less than tanh (ε / 2).

theorem UpperHalfPlane.image_discCoordinate_ball (z : UpperHalfPlane) (ε : ℝ) : z.discCoordinate '' Metric.ball z ε = Metric.ball 0 (Real.tanh (ε / 2))

The disc coordinate carries hyperbolic discs to Euclidean discs: the hyperbolic disc of radius ε about z is mapped onto the Euclidean disc of radius tanh (ε / 2) about 0.

theorem UpperHalfPlane.discCoordinate_smul_of_smul_eq_self {g : GL (Fin 2) ℝ} (hdet : 0 < ↑(Matrix.GeneralLinearGroup.det g)) {z : UpperHalfPlane} (hg : g • z = z) (τ : UpperHalfPlane) : z.discCoordinate (g • τ) = (starRingEnd ℂ) (denom g ↑z) / denom g ↑z * z.discCoordinate τ

A matrix of positive determinant fixing z is a rotation in the disc coordinate centred at z, by the unimodular multiplier conj (denom g z) / denom g z.

Positive determinant is what makes the Möbius transformation holomorphic; the determinant itself cancels, since it scales the displacements from z and from conj z alike.

theorem UpperHalfPlane.discCoordinate_specialLinearGroup_smul_of_smul_eq_self {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} {z : UpperHalfPlane} (hg : g • z = z) (τ : UpperHalfPlane) : z.discCoordinate (g • τ) = (starRingEnd ℂ) (denom (Matrix.SpecialLinearGroup.toGL g) ↑z) / denom (Matrix.SpecialLinearGroup.toGL g) ↑z * z.discCoordinate τ

An element of SL(2, ℝ) fixing z is a rotation in the disc coordinate centred at z, by the unimodular multiplier conj (denom g z) / denom g z: the determinant-one case of UpperHalfPlane.discCoordinate_smul_of_smul_eq_self.

theorem UpperHalfPlane.discCoordinate_psl_smul_of_smul_eq_self {q : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} {z : UpperHalfPlane} (hq : q • z = z) (τ : UpperHalfPlane) : z.discCoordinate (q • τ) = q.smulDeriv z * z.discCoordinate τ

An element of PSL(2, ℝ) fixing z is a rotation in the disc coordinate centred at z, by its derivative Matrix.ProjectiveSpecialLinearGroup.smulDeriv at z, which is a complex number of modulus one. This is the linearization of a point stabilizer of the effective projective action.