Trace identities for 2 × 2 matrices

By the Cayley–Hamilton theorem in size two, a 2 × 2 matrix A satisfies A ^ 2 = (trace A) • A - (det A) • 1, so its powers obey the linear recurrence A ^ (n + 2) = (trace A) • A ^ (n + 1) - (det A) • A ^ n, and so do their traces. Over a linearly ordered commutative ring this controls the powers of a hyperbolic matrix of determinant one: if 2 < trace A then the traces of the powers of A increase strictly, so 2 < trace (A ^ n) for every n ≠ 0; hence if 2 < |trace A| then 2 < |trace (A ^ n)| for every n ≠ 0. In particular no nonzero power of such a matrix is ± 1. For determinant one, 2 < |trace A| is equivalent to Mathlib's Matrix.IsHyperbolic A, whose discriminant is trace A ^ 2 - 4.

The Fricke trace identity expresses the trace of a commutator in SL(2, R) through the traces of the two matrices and of their product: tr ⁅A, B⁆ = tr A ^ 2 + tr B ^ 2 + tr (A B) ^ 2 - tr A tr B tr (A B) - 2.

These are the matrix inputs for reading off the order of an element of SL(2, R) or PSL(2, R) from its trace, and for recognizing a commutator as hyperbolic. The real elliptic case, where the trace is 2 cos θ, is in TauCeti.Analysis.SpecialFunctions.Trigonometric.MatrixFinTwo.

Main results

• Matrix.sq_eq_trace_smul_sub_det_smul_one_fin_two: the Cayley–Hamilton identity in size two.
• Matrix.pow_add_two_fin_two, Matrix.trace_pow_add_two_fin_two: the Cayley–Hamilton recurrence for the powers of a 2 × 2 matrix and for their traces.
• Matrix.two_lt_trace_pow, Matrix.two_lt_abs_trace_pow: the nonzero powers of a determinant-one matrix of trace (respectively absolute trace) greater than 2 again have that property.
• Matrix.isHyperbolic_iff_two_lt_abs_trace: a determinant-one matrix is hyperbolic exactly when its trace has absolute value greater than 2.
• Matrix.SpecialLinearGroup.trace_commutatorElement_fin_two: the Fricke trace identity.

References

• Svetlana Katok, Fuchsian Groups, Chicago Lectures in Mathematics, University of Chicago Press, 1992, §2.1 (the classification of elements of PSL(2, ℝ) by their trace).
• William M. Goldman, Trace coordinates on Fricke spaces of some simple hyperbolic surfaces, in Handbook of Teichmüller theory, Vol. II, EMS, 2009, §2 (the trace of a commutator).

theorem Matrix.sq_eq_trace_smul_sub_det_smul_one_fin_two {R : Type u_1} [CommRing R] (A : Matrix (Fin 2) (Fin 2) R) : A ^ 2 = A.trace • A - A.det • 1

Cayley–Hamilton in size two: a 2 × 2 matrix A satisfies A ^ 2 = (trace A) • A - (det A) • 1.

theorem Matrix.pow_add_two_fin_two {R : Type u_1} [CommRing R] (A : Matrix (Fin 2) (Fin 2) R) (n : ℕ) : A ^ (n + 2) = A.trace • A ^ (n + 1) - A.det • A ^ n

Cayley–Hamilton in size two, as a recurrence for the powers of a 2 × 2 matrix.

theorem Matrix.trace_pow_add_two_fin_two {R : Type u_1} [CommRing R] (A : Matrix (Fin 2) (Fin 2) R) (n : ℕ) : (A ^ (n + 2)).trace = A.trace * (A ^ (n + 1)).trace - A.det * (A ^ n).trace

The traces of the powers of a 2 × 2 matrix satisfy the Cayley–Hamilton recurrence.

theorem Matrix.two_lt_trace_pow {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {A : Matrix (Fin 2) (Fin 2) R} (hdet : A.det = 1) (htr : 2 < A.trace) {n : ℕ} (hn : n ≠ 0) : 2 < (A ^ n).trace

If a 2 × 2 matrix of determinant one has trace greater than 2, then so does every nonzero power of it: the traces of the powers increase strictly.

theorem Matrix.two_lt_abs_trace_pow {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {A : Matrix (Fin 2) (Fin 2) R} (hdet : A.det = 1) (htr : 2 < |A.trace|) {n : ℕ} (hn : n ≠ 0) : 2 < |(A ^ n).trace|

If a 2 × 2 matrix of determinant one has trace of absolute value greater than 2, then so does every nonzero power of it. In particular no nonzero power of it is 1 or -1.

theorem Matrix.isHyperbolic_iff_two_lt_abs_trace {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {A : Matrix (Fin 2) (Fin 2) R} (hdet : A.det = 1) : A.IsHyperbolic ↔ 2 < |A.trace|

A 2 × 2 matrix of determinant one is hyperbolic, in the sense of Matrix.IsHyperbolic, exactly when its trace has absolute value greater than 2: its discriminant is trace A ^ 2 - 4.

theorem Matrix.SpecialLinearGroup.trace_commutatorElement_fin_two {R : Type u_1} [CommRing R] (A B : SpecialLinearGroup (Fin 2) R) : (↑⁅A, B⁆).trace = (↑A).trace ^ 2 + (↑B).trace ^ 2 + (↑(A * B)).trace ^ 2 - (↑A).trace * (↑B).trace * (↑(A * B)).trace - 2

The Fricke trace identity: the trace of the commutator A * B * A⁻¹ * B⁻¹ of two matrices of SL(2, R) is tr A ^ 2 + tr B ^ 2 + tr (A * B) ^ 2 - tr A * tr B * tr (A * B) - 2.