Theorems · Theorem · number theory

UpperHalfPlane.gl_smul_eq_self_iff_quadratic

∀ {g : GL (Fin 2) ℝ} {z : UpperHalfPlane},
  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.

Defined in

Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Cited by

2 results in Mathlib

Foundations

Depth 175 from the axioms · uses propext, Classical.choice, Quot.sound