Fixed points of isometries of the upper half-plane #

In this file we show that the scalar multiplication by an element g : GL (Fin 2) ℝ has the following set of fixed points, depending on g.

if g preserves orientation (i.e., has positive determinant) and is an elliptic matrix, then z ↦ g • z has a unique fixed point;
if g is a scalar matrix, then it acts by the identity map (proved upstream of this file);
if g preserves orientation, and is a parabolic or a hyperbolic matrix, then it has no fixed points;
if g reverses orientation and has zero trace, then it has a geodesic line of fixed points;
- if g 1 0 = 0, then this is the vertical line re z = g 0 1 / (2 * g 1 1);
- otherwise, it's a half-circle with its center on the real axis;
if g reverses orientation and has nonzero trace, then it has no fixed points.

As a corollary of this classification, we conclude that PSL(2, ℝ) acts faithfully on the upper half-plane.

source

theorem UpperHalfPlane.gl_smul_eq_iff_num_eq {g : GL (Fin 2) ℝ} {z w : UpperHalfPlane} :

g • z = w ↔ num g ↑z = (σ g) ↑w * denom g ↑z

source

theorem UpperHalfPlane.gl_smul_eq_self_iff_re_eq {g : GL (Fin 2) ℝ} {z : UpperHalfPlane} (htrace : (↑g).trace = 0) (hc : ↑g 1 0 = 0) :

g • z = z ↔ z.re = ↑g 0 1 / (2 * ↑g 1 1)

If g is an upper triangular matrix with trace zero, then g fixes the vertical line re z = b / (2 * d).

source

theorem UpperHalfPlane.gl_smul_eq_self_iff_dist_sq_eq {g : GL (Fin 2) ℝ} {z : UpperHalfPlane} (h : (↑g).det < 0) (htrace : (↑g).trace = 0) (hc : ↑g 1 0 ≠ 0) :

g • z = z ↔ dist (↑z) (-↑(↑g 1 1) / ↑(↑g 1 0)) ^ 2 = -(↑g).det / ↑g 1 0 ^ 2

If g is an orientation reversing matrix with trace zero and c ≠ 0, then its action on the upper half plane has a half-circle of fixed points. In the hyperbolic geometry, this half-circle is a line. If c = 0, then this line is a vertical half-line in the usual geometry, see gl_smul_eq_self_iff_re_eq.

source

theorem UpperHalfPlane.gl_smul_eq_self_iff_dist_eq {g : GL (Fin 2) ℝ} {z : UpperHalfPlane} (h : (↑g).det < 0) (htrace : (↑g).trace = 0) (hc : ↑g 1 0 ≠ 0) :

g • z = z ↔ dist (↑z) (-↑(↑g 1 1) / ↑(↑g 1 0)) = √(-(↑g).det) / |↑g 1 0|

source

theorem UpperHalfPlane.exists_gl_smul_eq_self_iff_trace_eq_zero {g : GL (Fin 2) ℝ} (h : (↑g).det < 0) :

(∃ (z : UpperHalfPlane), g • z = z) ↔ (↑g).trace = 0

An orientation-reversing isometry of the hyperbolic plane has a fixed point iff the corresponding matrix has zero trace.

source

theorem UpperHalfPlane.gl_smul_eq_self_iff_quadratic {g : GL (Fin 2) ℝ} {z : UpperHalfPlane} (h : 0 < (↑g).det) :

g • z = z ↔ ↑(↑g 1 0) * (↑z * ↑z) + (↑(↑g 1 1) - ↑(↑g 0 0)) * ↑z + -↑(↑g 0 1) = 0

If g is an orientation-preserving map, then the fixed points of its action on the upper half-plane can be found from a quadratic equation.

If c ≠ 0, then this equation has a unique solution in the upper half-plane given by UpperHalfPlane.fixedPt. If c = 0, then the equation degenerates to a linear equation, which has no solutions in the upper half-plane unless g is a scalar matrix.

See also Matrix.GeneralLinearGroup.fixpointPolynomial_aeval_eq_zero_iff for a similar lemma about the action on the projective line, encoded as OnePoint R, where R is the ring of coefficients.

source

theorem UpperHalfPlane.isElliptic_of_exists_smul_eq_self {g : GL (Fin 2) ℝ} (h : 0 < (↑g).det) (hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)) (hfix : ∃ (z : UpperHalfPlane), g • z = z) :

g.IsElliptic

If g is a non-scalar orientation perserving matrix with a fixed point in ℍ, then it's an elliptic matrix.

source

noncomputable def UpperHalfPlane.fixedPt (g : GL (Fin 2) ℝ) (hell : g.IsElliptic) :

UpperHalfPlane

The unique fixed point of an orientation-preserving elliptic matrix acting on ℍ.

Equations

UpperHalfPlane.fixedPt g hell = { coe := (↑(↑g 0 0) - ↑(↑g 1 1)) / (2 * ↑(↑g 1 0)) + Complex.I * (↑√(-(↑g).discr) / (2 * ↑|↑g 1 0|)), coe_im_pos := ⋯ }