Parabolic fibers of the normalized Markoff surface

This module exposes the elementary algebra suppressed in Lemma 3 of Bourgain--Gamburd--Sarnak. The parameter fixed in the first coordinate is a normalized trace, so the exceptional values are 2 and -2, not the original-coordinate values 2 / 3 and -2 / 3.

def BGS.Markoff.parabolicLineAtTwo {R : Type u} [CommRing R] (i t : R) : NormalizedPoint R

One of the two affine lines above the normalized parabolic trace 2. Replacing i by -i gives the other line.

Equations

• BGS.Markoff.parabolicLineAtTwo i t = { u1 := 2, u2 := t, u3 := t + 2 * i }

def BGS.Markoff.parabolicLineAtNegTwo {R : Type u} [CommRing R] (i t : R) : NormalizedPoint R

One of the two affine lines above the normalized parabolic trace -2. Replacing i by -i gives the other line.

Equations

• BGS.Markoff.parabolicLineAtNegTwo i t = { u1 := -2, u2 := t, u3 := -t + 2 * i }

theorem BGS.Markoff.normalizedPolynomial_at_two {R : Type u} [CommRing R] (t s : R) : normalizedPolynomial { u1 := 2, u2 := t, u3 := s } = (s - t) ^ 2 + 4

At normalized trace 2, the Markoff equation is the factorized equation (u₃ - u₂)² = -4.

theorem BGS.Markoff.normalizedPolynomial_at_neg_two {R : Type u} [CommRing R] (t s : R) : normalizedPolynomial { u1 := -2, u2 := t, u3 := s } = (s + t) ^ 2 + 4

At normalized trace -2, the Markoff equation is the factorized equation (u₃ + u₂)² = -4.

theorem BGS.Markoff.isNormalizedMarkoff_at_two_iff {R : Type u} [CommRing R] (t s : R) : IsNormalizedMarkoff { u1 := 2, u2 := t, u3 := s } ↔ (s - t) ^ 2 = -2 ^ 2

theorem BGS.Markoff.isNormalizedMarkoff_at_neg_two_iff {R : Type u} [CommRing R] (t s : R) : IsNormalizedMarkoff { u1 := -2, u2 := t, u3 := s } ↔ (s + t) ^ 2 = -2 ^ 2

theorem BGS.Markoff.isNormalizedMarkoff_at_two_iff_on_parabolic_lines {R : Type u} [CommRing R] [NoZeroDivisors R] {i t s : R} (hi : i ^ 2 = -1) : IsNormalizedMarkoff { u1 := 2, u2 := t, u3 := s } ↔ s = t + 2 * i ∨ s = t + 2 * -i

Once a square root i of -1 is fixed, the trace-2 equation has exactly the two displayed line solutions.

theorem BGS.Markoff.isNormalizedMarkoff_at_neg_two_iff_on_parabolic_lines {R : Type u} [CommRing R] [NoZeroDivisors R] {i t s : R} (hi : i ^ 2 = -1) : IsNormalizedMarkoff { u1 := -2, u2 := t, u3 := s } ↔ s = -t + 2 * i ∨ s = -t + 2 * -i

Once a square root i of -1 is fixed, the trace--2 equation has exactly the two displayed line solutions.

theorem BGS.Markoff.normalizedFiber1_two_eq_parabolic_lines {R : Type u} [CommRing R] [NoZeroDivisors R] (i : R) (hi : i ^ 2 = -1) : normalizedFiber1 2 = Set.range (parabolicLineAtTwo i) ∪ Set.range (parabolicLineAtTwo (-i))

Set-theoretic classification of the normalized trace-2 fiber as two affine lines.

theorem BGS.Markoff.normalizedFiber1_neg_two_eq_parabolic_lines {R : Type u} [CommRing R] [NoZeroDivisors R] (i : R) (hi : i ^ 2 = -1) : normalizedFiber1 (-2) = Set.range (parabolicLineAtNegTwo i) ∪ Set.range (parabolicLineAtNegTwo (-i))

Set-theoretic classification of the normalized trace--2 fiber as two affine lines.

theorem BGS.Markoff.parabolicLineAtTwo_injective {R : Type u} [CommRing R] (i : R) : Function.Injective (parabolicLineAtTwo i)

Each parabolic-line parametrization is injective because its second coordinate is the parameter.

theorem BGS.Markoff.parabolicLineAtNegTwo_injective {R : Type u} [CommRing R] (i : R) : Function.Injective (parabolicLineAtNegTwo i)

Each trace--2 parabolic-line parametrization is injective.

theorem BGS.Markoff.parabolicLineAtTwo_disjoint {R : Type u} [CommRing R] (i : R) (hfourI : 4 * i ≠ 0) : Disjoint (Set.range (parabolicLineAtTwo i)) (Set.range (parabolicLineAtTwo (-i)))

The two trace-2 lines are disjoint whenever 4i is nonzero.

theorem BGS.Markoff.parabolicLineAtNegTwo_disjoint {R : Type u} [CommRing R] (i : R) (hfourI : 4 * i ≠ 0) : Disjoint (Set.range (parabolicLineAtNegTwo i)) (Set.range (parabolicLineAtNegTwo (-i)))

The two trace--2 lines are disjoint whenever 4i is nonzero.

@[simp]

theorem BGS.Markoff.normalizedRotate1_parabolicLineAtTwo {R : Type u} [CommRing R] (i t : R) : normalizedRotate1 (parabolicLineAtTwo i t) = parabolicLineAtTwo i (t + 2 * i)

The normalized rotation at trace 2 acts by translation on either parabolic line.

@[simp]

theorem BGS.Markoff.normalizedRotate1_parabolicLineAtNegTwo {R : Type u} [CommRing R] (i t : R) : normalizedRotate1 (parabolicLineAtNegTwo i t) = parabolicLineAtNegTwo (-i) (-t + 2 * i)

The normalized rotation at trace -2 exchanges the two parabolic lines.

theorem BGS.Markoff.normalizedRotate1_twice_parabolicLineAtNegTwo {R : Type u} [CommRing R] (i t : R) : normalizedRotate1 (normalizedRotate1 (parabolicLineAtNegTwo i t)) = parabolicLineAtNegTwo i (t - 4 * i)

Two steps of the trace--2 rotation return to the same line and translate its parameter.

theorem BGS.Markoff.normalizedFiber1_two_eq_empty_of_mod_four_eq_three (p : ℕ) [Fact (Nat.Prime p)] (hmod : p % 4 = 3) : normalizedFiber1 2 = ∅

If p ≡ 3 (mod 4), the normalized trace-2 fiber is empty.

theorem BGS.Markoff.normalizedFiber1_neg_two_eq_empty_of_mod_four_eq_three (p : ℕ) [Fact (Nat.Prime p)] (hmod : p % 4 = 3) : normalizedFiber1 (-2) = ∅

If p ≡ 3 (mod 4), the normalized trace--2 fiber is empty.

theorem BGS.Markoff.exists_parabolic_line_decomposition_of_mod_four_eq_one (p : ℕ) [Fact (Nat.Prime p)] (hmod : p % 4 = 1) : ∃ (i : ZMod p), i ^ 2 = -1 ∧ normalizedFiber1 2 = Set.range (parabolicLineAtTwo i) ∪ Set.range (parabolicLineAtTwo (-i)) ∧ normalizedFiber1 (-2) = Set.range (parabolicLineAtNegTwo i) ∪ Set.range (parabolicLineAtNegTwo (-i))

If p ≡ 1 (mod 4), a square root of -1 exists and simultaneously supplies the two-line descriptions of both normalized parabolic fibers.

theorem BGS.Markoff.iterate_normalizedRotate1_parabolicLineAtTwo {R : Type u} [CommRing R] (n : ℕ) (i t : R) : normalizedRotate1^[n] (parabolicLineAtTwo i t) = parabolicLineAtTwo i (t + ↑n * (2 * i))

Iterating the trace-2 rotation translates the line parameter by 2ni.

theorem BGS.Markoff.iterate_normalizedRotate1_parabolicLineAtTwo_eq_self_iff (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (n : ℕ) (i t : ZMod p) (hi : i ^ 2 = -1) : normalizedRotate1^[n] (parabolicLineAtTwo i t) = parabolicLineAtTwo i t ↔ p ∣ n

On either trace-2 parabolic line over ZMod p, a rotation iterate returns to its starting point exactly when the exponent is divisible by p.

theorem BGS.Markoff.rho_two_pow {R : Type u} [CommRing R] (n : ℕ) : rho 2 ^ n = !![1 - ↑n, ↑n; -↑n, 1 + ↑n]

Closed formula for powers of the unipotent normalized rotation with trace 2.

theorem BGS.Markoff.rhoSL_two_pow_eq_one_iff (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : rhoSL 2 ^ n = 1 ↔ p ∣ n

A power of the trace-2 rotation over ZMod p is the identity exactly at multiples of the characteristic.

theorem BGS.Markoff.rotationOrder_two (p : ℕ) [Fact (Nat.Prime p)] : rotationOrder 2 = p

The normalized trace-2 rotation has exact group-theoretic order p.

theorem BGS.Markoff.rho_neg_two_pow {R : Type u} [CommRing R] (n : ℕ) : rho (-2) ^ n = !![(-1) ^ n * (1 - ↑n), (-1) ^ n * -↑n; (-1) ^ n * ↑n, (-1) ^ n * (1 + ↑n)]

Closed formula for powers of the nontrivial parabolic normalized rotation with trace -2. The scalar factor records its eigenvalue -1; the remaining matrix is unipotent.

theorem BGS.Markoff.rhoSL_neg_two_pow_eq_one_iff (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (n : ℕ) : rhoSL (-2) ^ n = 1 ↔ 2 * p ∣ n

A power of the trace--2 rotation over an odd prime field is the identity exactly at multiples of 2p.

theorem BGS.Markoff.rotationOrder_neg_two (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) : rotationOrder (-2) = 2 * p

The normalized trace--2 rotation has exact group-theoretic order 2p for odd p.