Finite-order Markoff rotations have torsion eigenvalues

This file isolates the algebraic kernel used in the opening argument of Bourgain--Gamburd--Sarnak. Over an algebraically closed field, a finite-order normalized rotation has an eigenvalue of finite multiplicative order, and its trace is the sum of that eigenvalue and its inverse.

The passage from a finite orbit of a point to finite order of the rotation matrix is deliberately not assumed here. It is a separate geometric step, and is delicate at the parabolic traces 2 and -2.

theorem BGS.Markoff.finiteOrderRotation_has_torsion_eigenvalue {K : Type u_1} [Field K] [IsAlgClosed K] (t : K) (hfinite : IsOfFinOrder (rhoSL t)) : ∃ (w : Kˣ), IsOfFinOrder w ∧ t = splitTorusTrace w

A finite-order normalized rotation has a torsion eigenvalue whose eigenvalue trace is the rotation parameter.

This includes the parabolic eigenvalues. In that case the eigenvalue squares to one, so it is visibly torsion; away from that case the existing diagonalization theorem transfers finite order from the rotation to the eigenvalue.

theorem BGS.Markoff.rhoSL_two_not_finiteOrder {R : Type u_2} [CommRing R] [CharZero R] : ¬IsOfFinOrder (rhoSL 2)

The trace-2 unipotent rotation has infinite order in characteristic zero.

theorem BGS.Markoff.exists_nonzero_fixedVector_with_infiniteOrder_rotation {R : Type u_2} [CommRing R] [CharZero R] : ∃ (v : Fin 2 → R), v ≠ 0 ∧ (rho 2).mulVec v = v ∧ ¬IsOfFinOrder (rhoSL 2)

Periodicity of one vector under a coordinate rotation does not by itself imply finite order of the rotation matrix. The nonzero vector (1,1) is fixed by the trace-2 rotation, while that matrix has infinite order in characteristic zero.

This is the parabolic obstruction that must be handled before the paper's finite-orbit discussion can invoke finiteOrderRotation_has_torsion_eigenvalue.