Split-torus traces and normalized Markoff rotations

This module makes explicit the elementary diagonalization used when a normalized rotation has split characteristic polynomial. The two parabolic parameters are excluded by the mathematical hypothesis w ^ 2 ≠ 1; at those parameters the matrix need not have the same order as w.

def BGS.Markoff.splitTorusTrace {F : Type u_1} [Field F] (w : Fˣ) : F

The trace of the determinant-one diagonal matrix with eigenvalues w and w⁻¹.

Equations

• BGS.Markoff.splitTorusTrace w = ↑w + ↑w⁻¹

noncomputable def BGS.Markoff.splitDiagonalSL {F : Type u_1} [Field F] (w : Fˣ) : Matrix.SpecialLinearGroup (Fin 2) F

The determinant-one diagonal matrix with eigenvalues w and w⁻¹.

Equations

• BGS.Markoff.splitDiagonalSL w = Matrix.SpecialLinearGroup.diag2 ↑w ⋯

@[simp]

theorem BGS.Markoff.splitDiagonalSL_coe {F : Type u_1} [Field F] (w : Fˣ) : ↑(splitDiagonalSL w) = !![↑w, 0; 0, ↑w⁻¹]

def BGS.Markoff.splitEigenbasis {F : Type u_1} [Field F] (w : Fˣ) : Matrix (Fin 2) (Fin 2) F

An eigenbasis for a non-parabolic split trace.

Equations

• BGS.Markoff.splitEigenbasis w = !![1, 1; ↑w, ↑w⁻¹]

theorem BGS.Markoff.splitEigenbasis_det {F : Type u_1} [Field F] (w : Fˣ) : (splitEigenbasis w).det = ↑w⁻¹ - ↑w

theorem BGS.Markoff.splitEigenbasis_det_ne_zero {F : Type u_1} [Field F] (w : Fˣ) (hw : ↑w ^ 2 ≠ 1) : (splitEigenbasis w).det ≠ 0

noncomputable def BGS.Markoff.splitEigenbasisGL {F : Type u_1} [Field F] (w : Fˣ) (hw : ↑w ^ 2 ≠ 1) : GL (Fin 2) F

The eigenbasis, regarded as an invertible matrix.

Equations

• BGS.Markoff.splitEigenbasisGL w hw = Matrix.GeneralLinearGroup.mkOfDetNeZero (BGS.Markoff.splitEigenbasis w) ⋯

@[simp]

theorem BGS.Markoff.splitEigenbasisGL_coe {F : Type u_1} [Field F] (w : Fˣ) (hw : ↑w ^ 2 ≠ 1) : ↑(splitEigenbasisGL w hw) = splitEigenbasis w

theorem BGS.Markoff.splitEigenbasis_semiconj {F : Type u_1} [Field F] (w : Fˣ) (hw : ↑w ^ 2 ≠ 1) : SemiconjBy (splitEigenbasisGL w hw) (Matrix.SpecialLinearGroup.toGL (splitDiagonalSL w)) (Matrix.SpecialLinearGroup.toGL (rhoSL (splitTorusTrace w)))

In the split eigenbasis, rho (w + w⁻¹) is diagonal.

@[simp]

theorem BGS.Markoff.splitDiagonalSL_mul {F : Type u_1} [Field F] (w z : Fˣ) : splitDiagonalSL (w * z) = splitDiagonalSL w * splitDiagonalSL z

Diagonal determinant-one matrices multiply by multiplying their first eigenvalues.

noncomputable def BGS.Markoff.splitDiagonalSLHom {F : Type u_1} [Field F] : Fˣ →* Matrix.SpecialLinearGroup (Fin 2) F

Diagonal determinant-one matrices form the split-torus homomorphism into SL₂.

Equations

• BGS.Markoff.splitDiagonalSLHom = { toFun := BGS.Markoff.splitDiagonalSL, map_one' := ⋯, map_mul' := ⋯ }

theorem BGS.Markoff.splitDiagonalSLHom_injective {F : Type u_1} [Field F] : Function.Injective ⇑splitDiagonalSLHom

theorem BGS.Markoff.splitDiagonalSL_orderOf {F : Type u_1} [Field F] (w : Fˣ) : orderOf (splitDiagonalSL w) = orderOf w

The diagonal SL₂ element has exactly the multiplicative order of its first eigenvalue.

theorem BGS.Markoff.rotationOrder_splitTorusTrace {F : Type u_1} [Field F] (w : Fˣ) (hw : ↑w ^ 2 ≠ 1) : rotationOrder (splitTorusTrace w) = orderOf w

A non-parabolic split trace has rotation order equal to the order of either eigenvalue.

theorem BGS.Markoff.splitTorusTrace_mem_boundedOrderTraceSet_of_rotationOrder_lt {F : Type u_1} [Field F] [Fintype Fˣ] [DecidableEq F] (w : Fˣ) (hw : ↑w ^ 2 ≠ 1) (bound : ℕ) (hsmall : rotationOrder (splitTorusTrace w) < bound) : splitTorusTrace w ∈ boundedOrderTraceSet splitTorusTrace bound

A small non-parabolic split rotation parameter belongs to the canonical bounded-order split-trace set used by the giant-orbit count.

theorem BGS.Markoff.extensionEigenbasis_semiconj {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] (t : F) (w : Eˣ) (hw : ↑w ^ 2 ≠ 1) (htrace : (algebraMap F E) t = splitTorusTrace w) : SemiconjBy (splitEigenbasisGL w hw) (Matrix.SpecialLinearGroup.toGL (splitDiagonalSL w)) ((Matrix.SpecialLinearGroup.mapGL E) (rhoSL t))

Diagonalization after extending scalars. This is the common kernel for both split eigenvalues and eigenvalues in a quadratic nonsplit torus.

theorem BGS.Markoff.rotationOrder_eq_orderOf_extensionEigenvalue {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] [FaithfulSMul F E] (t : F) (w : Eˣ) (hw : ↑w ^ 2 ≠ 1) (htrace : (algebraMap F E) t = splitTorusTrace w) : rotationOrder t = orderOf w

If the eigenvalues of a non-parabolic normalized rotation lie in an injective scalar extension, its rotation order is exactly the multiplicative order of either eigenvalue.

theorem BGS.Markoff.extensionTrace_mem_boundedOrderTraceSet_of_rotationOrder_lt {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] [FaithfulSMul F E] {H : Type u_3} [Group H] [Fintype H] [DecidableEq F] (includeEigenvalue : H →* Eˣ) (hinclude : Function.Injective ⇑includeEigenvalue) (trace : H → F) (g : H) (hw : ↑(includeEigenvalue g) ^ 2 ≠ 1) (htrace : (algebraMap F E) (trace g) = splitTorusTrace (includeEigenvalue g)) (bound : ℕ) (hsmall : rotationOrder (trace g) < bound) : trace g ∈ boundedOrderTraceSet trace bound

The scalar-extension order calculation feeds directly into the canonical bounded-order trace set for any honestly embedded torus. In the nonsplit application, H is the norm-one subgroup of a quadratic extension and includeEigenvalue is its subtype map.

@[reducible, inline]

abbrev BGS.Markoff.quadraticFiniteField (p : ℕ) [Fact (Nat.Prime p)] : Type

The canonical quadratic extension of ZMod p supplied by Mathlib.

Equations

• BGS.Markoff.quadraticFiniteField p = GaloisField p 2

noncomputable def BGS.Markoff.quadraticNormOneTorus (p : ℕ) [Fact (Nat.Prime p)] : Subgroup (quadraticFiniteField p)ˣ

The norm-one subgroup of the multiplicative group of the quadratic finite field.

Equations

• BGS.Markoff.quadraticNormOneTorus p = (Units.map (Algebra.norm (ZMod p))).ker

@[instance_reducible]

noncomputable instance BGS.Markoff.quadraticNormOneTorusFintype (p : ℕ) [Fact (Nat.Prime p)] : Fintype ↥(quadraticNormOneTorus p)

Equations

• BGS.Markoff.quadraticNormOneTorusFintype p = Fintype.ofFinite ↥(BGS.Markoff.quadraticNormOneTorus p)

noncomputable def BGS.Markoff.quadraticNormOneTrace (p : ℕ) [Fact (Nat.Prime p)] (w : ↥(quadraticNormOneTorus p)) : ZMod p

The base-field trace on the quadratic norm-one torus.

Equations

• BGS.Markoff.quadraticNormOneTrace p w = (Algebra.trace (ZMod p) (BGS.Markoff.quadraticFiniteField p)) ↑↑w

theorem BGS.Markoff.algebraMap_quadraticNormOneTrace (p : ℕ) [Fact (Nat.Prime p)] (w : ↥(quadraticNormOneTorus p)) : (algebraMap (ZMod p) (quadraticFiniteField p)) (quadraticNormOneTrace p w) = splitTorusTrace ↑w

For a norm-one element in the quadratic extension, its field trace is the eigenvalue trace w + w⁻¹.

theorem BGS.Markoff.rotationOrder_quadraticNormOneTrace (p : ℕ) [Fact (Nat.Prime p)] (w : ↥(quadraticNormOneTorus p)) (hw : ↑↑w ^ 2 ≠ 1) : rotationOrder (quadraticNormOneTrace p w) = orderOf w

Away from the two parabolic eigenvalues, the normalized rotation order equals the order of the corresponding norm-one element in the quadratic extension.

theorem BGS.Markoff.quadraticNormOneTrace_mem_boundedOrderTraceSet_of_rotationOrder_lt (p : ℕ) [Fact (Nat.Prime p)] (w : ↥(quadraticNormOneTorus p)) (hw : ↑↑w ^ 2 ≠ 1) (bound : ℕ) (hsmall : rotationOrder (quadraticNormOneTrace p w) < bound) : quadraticNormOneTrace p w ∈ boundedOrderTraceSet (quadraticNormOneTrace p) bound

A small non-parabolic nonsplit rotation trace belongs to the canonical bounded-order trace set of the quadratic norm-one torus.

theorem BGS.Markoff.quadraticNormOneTraceSet_card_le_bound_sq (p : ℕ) [Fact (Nat.Prime p)] (bound : ℕ) : (boundedOrderTraceSet (quadraticNormOneTrace p) bound).card ≤ bound ^ 2

The nonsplit bounded-order trace set has the same crude quadratic bound used by the final giant-orbit count.