Real 2 × 2 matrices with trace 2 cos θ

A real 2 × 2 matrix A of determinant one and trace 2 cos θ has powers given by the Chebyshev form of the Cayley–Hamilton recurrence, sin θ • A ^ n = sin (n θ) • A - sin ((n - 1) θ) • 1. At θ = π / k with 2 ≤ k this gives A ^ k = -1, so an element of PSL(2, ℝ) whose representatives have trace ± 2 cos (π / k) is elliptic of order dividing k.

The rotation !![cos θ, sin θ; -sin θ, cos θ] conjugated by diag (exp (t / 2), exp (-t / 2)) is the matrix !![cos θ, exp t * sin θ; -(exp (-t) * sin θ), cos θ] of SL(2, ℝ), of trace 2 cos θ. Two such matrices with parameters (θ₁, 0) and (θ₂, t) have a product of trace 2 cos θ₁ cos θ₂ - 2 cosh t sin θ₁ sin θ₂ and, by the Fricke trace identity, a commutator of trace 2 + 4 (sin θ₁ sin θ₂ sinh t) ^ 2. These are the matrices of the representation of a hyperbolic triangle group in PSL(2, ℝ).

Main results

• Matrix.sin_smul_pow_fin_two: the powers of a determinant-one matrix of trace 2 cos θ.
• Matrix.pow_eq_neg_one_of_trace_eq_two_mul_cos_pi_div: a determinant-one real matrix of trace 2 cos (π / k), with 2 ≤ k, has k-th power -1.
• Matrix.ProjectiveSpecialLinearGroup.mk_pow_eq_one_of_trace_sq_eq_two_mul_cos_pi_div_sq: if trace A ^ 2 = (2 cos (π / k)) ^ 2 with 2 ≤ k, then the class of A has k-th power 1.
• Matrix.SpecialLinearGroup.rotation: the rotation matrix !![cos θ, sin θ; -sin θ, cos θ]; rotation_zero, rotation_add and rotation_inv make the family a one-parameter subgroup, continuous_rotation a continuous one, and pslMk_rotation_pi_div_two identifies the class of the quarter turn in PSL(2, ℝ) with TauCeti.pslS.
• Matrix.SpecialLinearGroup.conjRotation: the conjugated rotation matrix (conjRotation_zero_right identifies the unconjugated case with rotation), with its trace trace_conjRotation, the trace trace_conjRotation_mul_conjRotation of a product, and the trace trace_commutatorElement_conjRotation of a commutator.

References

• Svetlana Katok, Fuchsian Groups, Chicago Lectures in Mathematics, University of Chicago Press, 1992, §2.1 (elliptic elements of PSL(2, ℝ) and their traces).

theorem Matrix.sin_smul_pow_fin_two {A : Matrix (Fin 2) (Fin 2) ℝ} {θ : ℝ} (hdet : A.det = 1) (htr : A.trace = 2 * Real.cos θ) (n : ℕ) : Real.sin θ • A ^ n = Real.sin (↑n * θ) • A - Real.sin ((↑n - 1) * θ) • 1

The powers of a real 2 × 2 matrix of determinant one and trace 2 cos θ: sin θ • A ^ n = sin (n θ) • A - sin ((n - 1) θ) • 1. The coefficients are the values of the Chebyshev polynomials of the second kind at cos θ, multiplied by sin θ.

theorem Matrix.pow_eq_neg_one_of_trace_eq_two_mul_cos_pi_div {A : Matrix (Fin 2) (Fin 2) ℝ} {k : ℕ} (hdet : A.det = 1) (hk : 2 ≤ k) (htr : A.trace = 2 * Real.cos (Real.pi / ↑k)) : A ^ k = -1

A real 2 × 2 matrix of determinant one and trace 2 cos (π / k), with 2 ≤ k, has k-th power -1. Its image in PSL(2, ℝ) has order dividing k.

theorem Matrix.ProjectiveSpecialLinearGroup.mk_pow_eq_one_of_trace_sq_eq_two_mul_cos_pi_div_sq {A : SpecialLinearGroup (Fin 2) ℝ} {k : ℕ} (hk : 2 ≤ k) (h : (↑A).trace ^ 2 = (2 * Real.cos (Real.pi / ↑k)) ^ 2) : ↑A ^ k = 1

If a matrix of SL(2, ℝ) has trace ± 2 cos (π / k) with 2 ≤ k, then its class in PSL(2, ℝ) has k-th power 1: the matrix itself, or its negative, has k-th power -1. The hypothesis is stated on the square of the trace, which depends only on the class in PSL(2, ℝ).

noncomputable def Matrix.SpecialLinearGroup.rotation (θ : ℝ) : SpecialLinearGroup (Fin 2) ℝ

The rotation !![cos θ, sin θ; -sin θ, cos θ], an element of SL(2, ℝ).

Equations

• Matrix.SpecialLinearGroup.rotation θ = ⟨!![Real.cos θ, Real.sin θ; -Real.sin θ, Real.cos θ], ⋯⟩

@[simp]

theorem Matrix.SpecialLinearGroup.coe_rotation (θ : ℝ) : ↑(rotation θ) = !![Real.cos θ, Real.sin θ; -Real.sin θ, Real.cos θ]

The entries of rotation θ.

@[simp]

theorem Matrix.SpecialLinearGroup.rotation_zero : rotation 0 = 1

The rotation by 0 is the identity.

theorem Matrix.SpecialLinearGroup.rotation_add (θ φ : ℝ) : rotation (θ + φ) = rotation θ * rotation φ

The rotations form a one-parameter subgroup: rotation (θ + φ) = rotation θ * rotation φ.

@[simp]

theorem Matrix.SpecialLinearGroup.rotation_inv (θ : ℝ) : (rotation θ)⁻¹ = rotation (-θ)

The inverse of rotation θ is rotation (-θ).

theorem Matrix.SpecialLinearGroup.continuous_rotation : Continuous rotation

The rotations θ ↦ rotation θ form a continuous family in SL(2, ℝ).

@[simp]

theorem Matrix.SpecialLinearGroup.pslMk_rotation_pi_div_two : ↑(rotation (Real.pi / 2)) = TauCeti.pslS

The class of rotation (π/2) = !![0, 1; -1, 0] in PSL(2, ℝ) is pslS, the image of ModularGroup.S = !![0, -1; 1, 0]: the two matrices differ by a sign.

noncomputable def Matrix.SpecialLinearGroup.conjRotation (θ t : ℝ) : SpecialLinearGroup (Fin 2) ℝ

The matrix !![cos θ, exp t * sin θ; -(exp (-t) * sin θ), cos θ] of SL(2, ℝ): the rotation rotation θ = !![cos θ, sin θ; -sin θ, cos θ] conjugated by diag (exp (t / 2), exp (-t / 2)).

Equations

• Matrix.SpecialLinearGroup.conjRotation θ t = ⟨!![Real.cos θ, Real.exp t * Real.sin θ; -(Real.exp (-t) * Real.sin θ), Real.cos θ], ⋯⟩

@[simp]

theorem Matrix.SpecialLinearGroup.coe_conjRotation (θ t : ℝ) : ↑(conjRotation θ t) = !![Real.cos θ, Real.exp t * Real.sin θ; -(Real.exp (-t) * Real.sin θ), Real.cos θ]

The entries of conjRotation θ t.

theorem Matrix.SpecialLinearGroup.conjRotation_zero_right (θ : ℝ) : conjRotation θ 0 = rotation θ

The unconjugated case of conjRotation is rotation.

theorem Matrix.SpecialLinearGroup.trace_conjRotation (θ t : ℝ) : (↑(conjRotation θ t)).trace = 2 * Real.cos θ

The conjugated rotation conjRotation θ t has the trace 2 cos θ of the rotation.

theorem Matrix.SpecialLinearGroup.trace_conjRotation_mul_conjRotation (θ₁ θ₂ t : ℝ) : (↑(conjRotation θ₂ t * conjRotation θ₁ 0)).trace = 2 * Real.cos θ₁ * Real.cos θ₂ - 2 * Real.cosh t * (Real.sin θ₁ * Real.sin θ₂)

The product of the conjugated rotations with parameters (θ₂, t) and (θ₁, 0) has trace 2 cos θ₁ cos θ₂ - 2 cosh t sin θ₁ sin θ₂.

@[simp]

theorem Matrix.SpecialLinearGroup.trace_commutatorElement_conjRotation (θ₁ θ₂ t : ℝ) : (↑⁅conjRotation θ₁ 0, conjRotation θ₂ t⁆).trace = 2 + 4 * (Real.sin θ₁ * Real.sin θ₂ * Real.sinh t) ^ 2

The commutator of the conjugated rotations with parameters (θ₁, 0) and (θ₂, t) has trace 2 + 4 (sin θ₁ sin θ₂ sinh t) ^ 2, by the Fricke trace identity.