Classification of elements of GL (Fin 2) R

Here we classify 2 × 2 matrices over the reals (or more generally over R where R is a suitable ring, but ℝ is the motivating case), into the following classes:

• scalars
• parabolic elements (Matrix.IsParabolic) - one eigenvalue with non-semisimple generalized eigenspace
• hyperbolic elements (Matrix.IsHyperbolic) - two distinct real eigenvalues
• elliptic elements (Matrix.IsElliptic) - two distinct non-real complex eigenvalues

This classification is used (among other places) in classifying the fixed points of elements of GL(2, ℝ)⁺ acting on the upper half-plane. See [Wikipedia:SL2(R)#Classification_of_elements] (https://en.wikipedia.org/wiki/SL2(R)#Classification_of_elements).

def Matrix.IsParabolic {R : Type u_1} [CommRing R] (m : Matrix (Fin 2) (Fin 2) R) : Prop

A 2 × 2 matrix is parabolic if it is non-scalar and its discriminant is 0.

@[simp]

theorem Matrix.discr_conj {R : Type u_1} [CommRing R] {m : Matrix (Fin 2) (Fin 2) R} (g : GL (Fin 2) R) : (↑g * m * (↑g)⁻¹).discr = m.discr

@[simp]

theorem Matrix.discr_conj' {R : Type u_1} [CommRing R] {m : Matrix (Fin 2) (Fin 2) R} (g : GL (Fin 2) R) : ((↑g)⁻¹ * m * ↑g).discr = m.discr

@[deprecated Matrix.discr_conj (since := "2025-10-20")]

theorem Matrix.disc_conj {R : Type u_1} [CommRing R] {m : Matrix (Fin 2) (Fin 2) R} (g : GL (Fin 2) R) : (↑g * m * (↑g)⁻¹).discr = m.discr

Alias of Matrix.discr_conj.

@[deprecated Matrix.discr_conj' (since := "2025-10-20")]

theorem Matrix.disc_conj' {R : Type u_1} [CommRing R] {m : Matrix (Fin 2) (Fin 2) R} (g : GL (Fin 2) R) : ((↑g)⁻¹ * m * ↑g).discr = m.discr

Alias of Matrix.discr_conj'.

@[simp]

theorem Matrix.isParabolic_conj_iff {R : Type u_1} [CommRing R] {m : Matrix (Fin 2) (Fin 2) R} (g : GL (Fin 2) R) : (↑g * m * (↑g)⁻¹).IsParabolic ↔ m.IsParabolic

@[simp]

theorem Matrix.isParabolic_conj'_iff {R : Type u_1} [CommRing R] {m : Matrix (Fin 2) (Fin 2) R} (g : GL (Fin 2) R) : ((↑g)⁻¹ * m * ↑g).IsParabolic ↔ m.IsParabolic

theorem Matrix.isParabolic_iff_of_upperTriangular {R : Type u_1} [CommRing R] {m : Matrix (Fin 2) (Fin 2) R} [IsReduced R] (hm : m 1 0 = 0) : m.IsParabolic ↔ m 0 0 = m 1 1 ∧ m 0 1 ≠ 0

theorem Matrix.sub_scalar_sq_eq_discr {K : Type u_1} [Field K] {m : Matrix (Fin 2) (Fin 2) K} [NeZero 2] : (m - (scalar (Fin 2)) (m.trace / 2)) ^ 2 = (scalar (Fin 2)) (m.discr / 4)

@[deprecated Matrix.sub_scalar_sq_eq_discr (since := "2025-10-20")]

theorem Matrix.sub_scalar_sq_eq_disc {K : Type u_1} [Field K] {m : Matrix (Fin 2) (Fin 2) K} [NeZero 2] : (m - (scalar (Fin 2)) (m.trace / 2)) ^ 2 = (scalar (Fin 2)) (m.discr / 4)

Alias of Matrix.sub_scalar_sq_eq_discr.

def Matrix.parabolicEigenvalue {K : Type u_1} [Field K] (m : Matrix (Fin 2) (Fin 2) K) : K

The unique eigenvalue of a parabolic matrix (junk if m is not parabolic).

theorem Matrix.IsParabolic.sub_eigenvalue_sq_eq_zero {K : Type u_1} [Field K] {m : Matrix (Fin 2) (Fin 2) K} [NeZero 2] (hm : m.IsParabolic) : (m - (scalar (Fin 2)) m.parabolicEigenvalue) ^ 2 = 0

theorem Matrix.isParabolic_iff_exists {K : Type u_1} [Field K] {m : Matrix (Fin 2) (Fin 2) K} [NeZero 2] : m.IsParabolic ↔ ∃ (a : K) (n : Matrix (Fin 2) (Fin 2) K), m = (scalar (Fin 2)) a + n ∧ n ≠ 0 ∧ n ^ 2 = 0

Characterization of parabolic elements: they have the form a + m where a is scalar and m is nonzero and nilpotent.

def Matrix.IsHyperbolic {R : Type u_1} [CommRing R] [Preorder R] (m : Matrix (Fin 2) (Fin 2) R) : Prop

A 2 × 2 matrix is hyperbolic if its discriminant is strictly positive.

def Matrix.IsElliptic {R : Type u_1} [CommRing R] [Preorder R] (m : Matrix (Fin 2) (Fin 2) R) : Prop

A 2 × 2 matrix is elliptic if its discriminant is strictly negative.

theorem Matrix.isHyperbolic_conj_iff {R : Type u_1} [CommRing R] [Preorder R] {m : Matrix (Fin 2) (Fin 2) R} (g : GL (Fin 2) R) : (↑g * m * (↑g)⁻¹).IsHyperbolic ↔ m.IsHyperbolic

theorem Matrix.isHyperbolic_conj'_iff {R : Type u_1} [CommRing R] [Preorder R] {m : Matrix (Fin 2) (Fin 2) R} (g : GL (Fin 2) R) : ((↑g)⁻¹ * m * ↑g).IsHyperbolic ↔ m.IsHyperbolic

theorem Matrix.isElliptic_conj_iff {R : Type u_1} [CommRing R] [Preorder R] {m : Matrix (Fin 2) (Fin 2) R} (g : GL (Fin 2) R) : (↑g * m * (↑g)⁻¹).IsElliptic ↔ m.IsElliptic

theorem Matrix.isElliptic_conj'_iff {R : Type u_1} [CommRing R] [Preorder R] {m : Matrix (Fin 2) (Fin 2) R} (g : GL (Fin 2) R) : ((↑g)⁻¹ * m * ↑g).IsElliptic ↔ m.IsElliptic

def Matrix.GeneralLinearGroup.upperRightHom {R : Type u_1} [Ring R] : AddChar R (GL (Fin 2) R)

The map sending x to [1, x; 0, 1] (bundled as an AddChar).

@[simp]

theorem Matrix.GeneralLinearGroup.upperRightHom_apply {R : Type u_1} [Ring R] (x : R) : upperRightHom x = { val := !![1, x; 0, 1], inv := !![1, -x; 0, 1], val_inv := ⋯, inv_val := ⋯ }

theorem Matrix.GeneralLinearGroup.injective_upperRightHom {R : Type u_1} [Ring R] : Function.Injective ⇑upperRightHom

@[reducible, inline]

abbrev Matrix.GeneralLinearGroup.IsParabolic {R : Type u_1} [CommRing R] (g : GL (Fin 2) R) : Prop

Synonym of Matrix.IsParabolic, for dot-notation.

@[simp]

theorem Matrix.GeneralLinearGroup.isParabolic_conj_iff {R : Type u_1} [CommRing R] (g h : GL (Fin 2) R) : (g * h * g⁻¹).IsParabolic ↔ h.IsParabolic

@[simp]

theorem Matrix.GeneralLinearGroup.isParabolic_conj_iff' {R : Type u_1} [CommRing R] (g h : GL (Fin 2) R) : (g⁻¹ * h * g).IsParabolic ↔ h.IsParabolic

@[reducible, inline]

abbrev Matrix.GeneralLinearGroup.IsElliptic {R : Type u_1} [CommRing R] [Preorder R] (g : GL (Fin 2) R) : Prop

Synonym of Matrix.IsElliptic, for dot-notation.

@[reducible, inline]

abbrev Matrix.GeneralLinearGroup.IsHyperbolic {R : Type u_1} [CommRing R] [Preorder R] (g : GL (Fin 2) R) : Prop

Synonym of Matrix.IsHyperbolic, for dot-notation.

noncomputable def Matrix.GeneralLinearGroup.fixpointPolynomial {R : Type u_1} [CommRing R] (g : GL (Fin 2) R) : Polynomial R

Polynomial whose roots are the fixed points of g considered as a Möbius transformation.

See Matrix.GeneralLinearGroup.fixpointPolynomial_aeval_eq_zero_iff.

theorem Matrix.GeneralLinearGroup.fixpointPolynomial_eq_zero_iff {R : Type u_1} [CommRing R] {g : GL (Fin 2) R} : g.fixpointPolynomial = 0 ↔ ↑g ∈ Set.range ⇑(Matrix.scalar (Fin 2))

The fixed-point polynomial is identically zero iff g is scalar.

theorem Matrix.GeneralLinearGroup.parabolicEigenvalue_ne_zero {K : Type u_2} [Field K] {g : GL (Fin 2) K} [NeZero 2] (hg : g.IsParabolic) : (↑g).parabolicEigenvalue ≠ 0

theorem Matrix.GeneralLinearGroup.IsParabolic.pow {K : Type u_2} [Field K] {g : GL (Fin 2) K} (hg : g.IsParabolic) [CharZero K] {n : ℕ} (hn : n ≠ 0) : (g ^ n).IsParabolic

A non-zero power of a parabolic element is parabolic.

theorem Matrix.GeneralLinearGroup.isParabolic_iff_of_upperTriangular {K : Type u_2} [Field K] {g : GL (Fin 2) K} (hg : ↑g 1 0 = 0) : g.IsParabolic ↔ ↑g 0 0 = ↑g 1 1 ∧ ↑g 0 1 ≠ 0

theorem Matrix.GeneralLinearGroup.isParabolic_iff_of_upperTriangular_of_det {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {g : GL (Fin 2) K} (h_det : det g = 1 ∨ det g = -1) (hg10 : ↑g 1 0 = 0) : g.IsParabolic ↔ (∃ (x : K), x ≠ 0 ∧ g = upperRightHom x) ∨ ∃ (x : K), x ≠ 0 ∧ g = -upperRightHom x

Specialized version of isParabolic_iff_of_upperTriangular intended for use with discrete subgroups of GL(2, ℝ).