The elliptic points i, ρ and ρ + 1 on the fundamental domain boundary

Mathlib gives ρ its square (UpperHalfPlane.ρ_sq) and its norm (UpperHalfPlane.norm_ρ). This file adds how ρ behaves under the inversion z ↦ -1/z, which is what the two ρ-corners of the standard fundamental domain need: the inversion swaps them, carrying ρ to ρ + 1 and back.

Both identities fall straight out of ρ_sq : (ρ : ℂ) ^ 2 = -ρ - 1, once the relevant denominator is known to be nonzero — and ρ + 1 ≠ 0 is itself read off from -1 / ρ = ρ + 1.

The file also collects the elementary values every consumer of the fundamental domain's boundary needs for its three elliptic points — the corners ρ, ρ + 1 and the arc midpoint i: the real part of ρ, the pairwise distinctness of the three points, their common unit modulus, the coercion identity for the translated corner, and the unit-circle/real-part characterizations that classify a boundary point as one of the three.

Main results

• UpperHalfPlane.neg_one_div_ρ: the inversion carries ρ to ρ + 1.
• UpperHalfPlane.neg_one_div_ρ_add_one: the inversion carries ρ + 1 to ρ.
• UpperHalfPlane.ρ_add_one_eq_exp, UpperHalfPlane.isPrimitiveRoot_ρ_add_one: the second corner ρ + 1 = e^{πi/3} is a primitive sixth root of unity.
• UpperHalfPlane.re_ρ, UpperHalfPlane.norm_eq_one_of_mem_ellipticPoints and the pairwise distinctness of i, ρ, ρ + 1.
• UpperHalfPlane.coe_vadd_one_ρ: the translated corner (1 : ℝ) +ᵥ ρ is ρ + 1 in ℂ.
• UpperHalfPlane.eq_I_of_re_eq_zero, UpperHalfPlane.eq_ρ_of_re_eq_neg_half, UpperHalfPlane.eq_vadd_one_ρ_of_re_eq_half: a unit-circle point of ℍ with real part 0, -1/2, 1/2 is i, ρ, ρ + 1 respectively.

@[simp]

theorem UpperHalfPlane.neg_one_div_ρ : -1 / ↑ρ = ↑ρ + 1

The inversion carries ρ to ρ + 1.

@[simp]

theorem UpperHalfPlane.norm_ρ_add_one : ‖↑ρ + 1‖ = 1

The second ρ-corner has unit modulus, like ρ itself: the inversion carries one to the other and preserves the norm.

@[simp]

theorem UpperHalfPlane.neg_one_div_ρ_add_one : -1 / (↑ρ + 1) = ↑ρ

The inversion carries ρ + 1 to ρ.

theorem UpperHalfPlane.ρ_add_one_eq_exp : ↑ρ + 1 = Complex.exp (↑(Real.pi / 3) * Complex.I)

The second corner ρ + 1 is the unit-circle point of angle π/3.

theorem UpperHalfPlane.isPrimitiveRoot_ρ_add_one : IsPrimitiveRoot (↑ρ + 1) 6

The second corner ρ + 1 = e^{πi/3} is a primitive sixth root of unity.

@[simp]

theorem UpperHalfPlane.re_ρ : ρ.re = -(1 / 2)

The real part of the corner ρ.

@[simp]

theorem UpperHalfPlane.I_ne_ρ : I ≠ ρ

The elliptic points i and ρ are distinct.

@[simp]

theorem UpperHalfPlane.I_ne_vadd_ρ : I ≠ 1 +ᵥ ρ

The elliptic points i and ρ + 1 are distinct.

@[simp]

theorem UpperHalfPlane.ρ_ne_vadd_ρ : ρ ≠ 1 +ᵥ ρ

The elliptic points ρ and ρ + 1 are distinct.

theorem UpperHalfPlane.coe_vadd_one_ρ : ↑(1 +ᵥ ρ) = ↑ρ + 1

The second corner ρ + 1 as a point of ℍ, computed into ℂ.

theorem UpperHalfPlane.eq_I_of_re_eq_zero {p : UpperHalfPlane} (hnorm : ‖↑p‖ = 1) (hre : (↑p).re = 0) : p = I

A point of the unit circle with real part 0 is the elliptic point i.

theorem UpperHalfPlane.eq_ρ_of_re_eq_neg_half {p : UpperHalfPlane} (hnorm : ‖↑p‖ = 1) (hre : (↑p).re = -(1 / 2)) : p = ρ

A point of the unit circle with real part -1/2 is the corner ρ.

theorem UpperHalfPlane.eq_vadd_one_ρ_of_re_eq_half {p : UpperHalfPlane} (hnorm : ‖↑p‖ = 1) (hre : (↑p).re = 1 / 2) : p = 1 +ᵥ ρ

A point of the unit circle with real part 1/2 is the corner ρ + 1.

theorem UpperHalfPlane.norm_eq_one_of_mem_ellipticPoints {z : ℂ} (hz : z ∈ {Complex.I, ↑ρ, ↑ρ + 1}) : ‖z‖ = 1

The three elliptic points on the boundary of the fundamental domain — the corners ρ, ρ + 1 and the arc midpoint i — all lie on the unit circle.