The normalized Markoff rotation

This file isolates the elementary two-dimensional linear algebra behind the fundamental rotation. The parameter of rho is a normalized trace coordinate. Thus the rotation fixing an original Markoff coordinate x.x1 is obtained by specializing the parameter to 3 * x.x1.

def BGS.Markoff.rho {R : Type u} [CommRing R] (t : R) : Matrix (Fin 2) (Fin 2) R

The normalized rotation matrix rho(t) = [[0, 1], [-1, t]].

Equations

• BGS.Markoff.rho t = !![0, 1; -1, t]

@[simp]

theorem BGS.Markoff.rho_det {R : Type u} [CommRing R] (t : R) : (rho t).det = 1

Every normalized rotation matrix has determinant one.

@[simp]

theorem BGS.Markoff.rho_trace {R : Type u} [CommRing R] (t : R) : (rho t).trace = t

The matrix parameter is exactly the trace of the normalized rotation.

@[simp]

theorem BGS.Markoff.rho_charpoly {R : Type u} [CommRing R] [Nontrivial R] (t : R) : (rho t).charpoly = Polynomial.X ^ 2 - Polynomial.C t * Polynomial.X + 1

The characteristic polynomial is T² - tT + 1.

@[simp]

theorem BGS.Markoff.rho_mulVec {R : Type u} [CommRing R] (t a b : R) : (rho t).mulVec ![a, b] = ![b, t * b - a]

On a coordinate pair, rho(t) sends (a, b) to (b, t * b - a).

def BGS.Markoff.rhoSL {R : Type u} [CommRing R] (t : R) : Matrix.SpecialLinearGroup (Fin 2) R

The normalized rotation, regarded as an element of the special linear group.

Equations

• BGS.Markoff.rhoSL t = ⟨BGS.Markoff.rho t, ⋯⟩

@[simp]

theorem BGS.Markoff.rhoSL_coe {R : Type u} [CommRing R] (t : R) : ↑(rhoSL t) = rho t

noncomputable def BGS.Markoff.rotationOrder {R : Type u} [CommRing R] (t : R) : ℕ

The group-theoretic order of the normalized rotation.

By the convention of orderOf, this is zero when the rotation has infinite order.

Equations

• BGS.Markoff.rotationOrder t = orderOf (BGS.Markoff.rhoSL t)

theorem BGS.Markoff.rhoSL_pow_rotationOrder {R : Type u} [CommRing R] (t : R) : rhoSL t ^ rotationOrder t = 1

Raising the rotation to rotationOrder gives the identity in SL₂.

theorem BGS.Markoff.rotationOrder_pos {R : Type u} [CommRing R] [Finite R] (t : R) : 0 < rotationOrder t

Over a finite coefficient ring, every normalized rotation has positive order.

def BGS.Markoff.movingCoordinates {R : Type u} (x : Point R) : Fin 2 → R

The two coordinates moved by the fundamental rotation fixing the first coordinate.

Equations

• BGS.Markoff.movingCoordinates x = ![x.x2, x.x3]

theorem BGS.Markoff.rho_mulVec_movingCoordinates {R : Type u} [CommRing R] (x : Point R) : (rho (3 * x.x1)).mulVec (movingCoordinates x) = movingCoordinates (rotate1 x)

The fundamental rotation is the action of rho(3 * x.x1) on the moving coordinates.

theorem BGS.Markoff.rho_trace_fundamentalRotation {R : Type u} [CommRing R] (x : Point R) : (rho (3 * x.x1)).trace = 3 * x.x1

The normalized trace parameter for the fundamental rotation is 3 * x.x1.

theorem BGS.Markoff.rotate1_eq_rho {R : Type u} [CommRing R] (x : Point R) : rotate1 x = { x1 := x.x1, x2 := (rho (3 * x.x1)).mulVec (movingCoordinates x) 0, x3 := (rho (3 * x.x1)).mulVec (movingCoordinates x) 1 }

Reconstruct the full fundamental rotation from the fixed coordinate and the matrix action.