The group GL (Fin 2) R

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.

Equations

• m.IsParabolic = (m ∉ Set.range ⇑(Matrix.scalar (Fin 2)) ∧ m.disc = 0)

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

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

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

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

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.disc / 4)

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).

Equations

• m.parabolicEigenvalue = m.trace / 2

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.

Equations

• m.IsHyperbolic = (0 < m.disc)

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.

Equations

• m.IsElliptic = (m.disc < 0)

theorem Matrix.isHyperbolic_conj_iff {R : Type u_1} [CommRing R] [Nontrivial 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] [Nontrivial 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] [Nontrivial 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] [Nontrivial R] [Preorder R] {m : Matrix (Fin 2) (Fin 2) R} (g : GL (Fin 2) R) : (↑g⁻¹ * m * ↑g).IsElliptic ↔ m.IsElliptic

@[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.

Equations

• g.IsParabolic = (↑g).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.

Equations

• g.IsElliptic = (↑g).IsElliptic

@[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.

Equations

• g.IsHyperbolic = (↑g).IsHyperbolic

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.

Equations

• g.fixpointPolynomial = Polynomial.C (↑g 1 0) * Polynomial.X ^ 2 + Polynomial.C (↑g 1 1 - ↑g 0 0) * Polynomial.X - Polynomial.C (↑g 0 1)

theorem Matrix.GeneralLinearGroup.fixpointPolynomial_eq_zero_iff {R : Type u_1} [CommRing R] {g : GL (Fin 2) R} : g.fixpointPolynomial = 0 ↔ ↑g ∈ Set.range ⇑(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.