The Markoff surface and its Vieta moves

For a commutative ring R, the Markoff surface is the set X(R) of triples x = (x₀, x₁, x₂) ∈ R³ with x₀² + x₁² + x₂² = 3 x₀ x₁ x₂. Triples are functions Fin 3 → R, so that coordinate permutations are precompositions. The equation is quadratic in each coordinate, and replacing one coordinate by the other root of that quadratic is the Vieta move R_i x, which replaces x_i by 3 x_{i+1} x_{i+2} - x_i. The positive Markoff triples M are the points of X(ℤ) with positive coordinates; the moves preserve them, and the Markoff graph joins two positive triples related by a move.

Main definitions

• TauCeti.markoffForm: the polynomial Φ(x) = x₀² + x₁² + x₂² - 3 x₀ x₁ x₂.
• TauCeti.markoffSet R: the Markoff surface X(R), the zero set of Φ.
• TauCeti.markoffSetNonzero R: its nonzero locus X*(R) = X(R) ∖ {0}.
• TauCeti.markoffVieta i: the Vieta move R_i, defined on all of R³.
• TauCeti.positiveMarkoffTriples: the ordered positive Markoff triples M ⊆ ℤ³.
• TauCeti.markoffGraph: the simple graph on M whose edges are the Vieta moves.

Main results

• TauCeti.markoffForm_markoffVieta: the moves preserve Φ, over every commutative ring.
• TauCeti.markoffVieta_involutive: each move is an involution of R³.
• TauCeti.bijOn_markoffVieta_markoffSetNonzero: each move permutes X*(R).
• TauCeti.markoffVieta_comp_perm: coordinate permutations normalise the moves.
• TauCeti.markoffVieta_apply_self_mul_self: the two roots in the moved coordinate multiply to x_{i+1}² + x_{i+2}².
• TauCeti.markoffVieta_mem_positiveMarkoffTriples_iff: the moves preserve M, in both directions.

References

• J. Bourgain, A. Gamburd and P. Sarnak, Markoff surfaces and strong approximation: 1, arXiv:1607.01530, §1.
• D. E. Martin, A new proof of Chen's theorem for Markoff graphs, §1, equations (1.1)–(1.2).
• Y. Zhang, Congruence and uniqueness of certain Markoff numbers, Acta Arith. 128 (2007), §1.

The Markoff form and the Markoff surface

def TauCeti.markoffForm {R : Type u_1} [CommRing R] (x : Fin 3 → R) : R

The Markoff form Φ(x) = x₀² + x₁² + x₂² - 3 x₀ x₁ x₂ of a triple x : Fin 3 → R, written symmetrically as ∑ i, x i ^ 2 - 3 * ∏ i, x i.

theorem TauCeti.markoffForm_eq {R : Type u_1} [CommRing R] (x : Fin 3 → R) : markoffForm x = x 0 ^ 2 + x 1 ^ 2 + x 2 ^ 2 - 3 * x 0 * x 1 * x 2

The Markoff form in coordinates.

@[simp]

theorem TauCeti.markoffForm_comp_perm {R : Type u_1} [CommRing R] (x : Fin 3 → R) (σ : Equiv.Perm (Fin 3)) : markoffForm (x ∘ ⇑σ) = markoffForm x

The Markoff form is symmetric.

theorem TauCeti.markoffForm_comp_ringHom {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (x : Fin 3 → R) (f : R →+* S) : markoffForm (⇑f ∘ x) = f (markoffForm x)

The Markoff form commutes with ring homomorphisms.

def TauCeti.markoffSet (R : Type u_3) [CommRing R] : Set (Fin 3 → R)

The Markoff surface X(R): the triples x : Fin 3 → R with x₀² + x₁² + x₂² = 3 x₀ x₁ x₂.

theorem TauCeti.mem_markoffSet_iff_markoffForm_eq_zero {R : Type u_1} [CommRing R] {x : Fin 3 → R} : x ∈ markoffSet R ↔ markoffForm x = 0

A triple lies on the Markoff surface exactly when the Markoff form vanishes at it.

theorem TauCeti.mem_markoffSet {R : Type u_1} [CommRing R] {x : Fin 3 → R} : x ∈ markoffSet R ↔ x 0 ^ 2 + x 1 ^ 2 + x 2 ^ 2 = 3 * x 0 * x 1 * x 2

A triple lies on the Markoff surface exactly when x₀² + x₁² + x₂² = 3 x₀ x₁ x₂.

@[simp]

theorem TauCeti.zero_mem_markoffSet {R : Type u_1} [CommRing R] : 0 ∈ markoffSet R

The origin lies on the Markoff surface.

@[simp]

theorem TauCeti.one_mem_markoffSet {R : Type u_1} [CommRing R] : 1 ∈ markoffSet R

The triple (1, 1, 1) lies on the Markoff surface over every commutative ring.

theorem TauCeti.comp_mem_markoffSet {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {x : Fin 3 → R} (hx : x ∈ markoffSet R) (f : R →+* S) : ⇑f ∘ x ∈ markoffSet S

Ring homomorphisms map the Markoff surface X(R) into X(S).

@[simp]

theorem TauCeti.comp_perm_mem_markoffSet_iff {R : Type u_1} [CommRing R] {x : Fin 3 → R} {σ : Equiv.Perm (Fin 3)} : x ∘ ⇑σ ∈ markoffSet R ↔ x ∈ markoffSet R

The Markoff surface is stable under coordinate permutations.

def TauCeti.markoffSetNonzero (R : Type u_3) [CommRing R] : Set (Fin 3 → R)

The nonzero locus X*(R) = X(R) ∖ {0} of the Markoff surface. Nonzero refers to the whole triple: individual coordinates of a point of X*(R) may vanish.

theorem TauCeti.mem_markoffSetNonzero {R : Type u_1} [CommRing R] {x : Fin 3 → R} : x ∈ markoffSetNonzero R ↔ x ∈ markoffSet R ∧ x ≠ 0

The points of X*(R) are the nonzero points of X(R).

theorem TauCeti.markoffSetNonzero_subset_markoffSet {R : Type u_1} [CommRing R] : markoffSetNonzero R ⊆ markoffSet R

The nonzero locus is contained in the Markoff surface.

@[simp]

theorem TauCeti.comp_perm_mem_markoffSetNonzero_iff {R : Type u_1} [CommRing R] {x : Fin 3 → R} {σ : Equiv.Perm (Fin 3)} : x ∘ ⇑σ ∈ markoffSetNonzero R ↔ x ∈ markoffSetNonzero R

The nonzero locus is stable under coordinate permutations.

The Vieta moves

def TauCeti.markoffVieta {R : Type u_1} [CommRing R] (i : Fin 3) (x : Fin 3 → R) : Fin 3 → R

The Vieta move R_i: replace the i-th coordinate x_i of a triple by 3 x_{i+1} x_{i+2} - x_i, the other root of the Markoff equation viewed as a quadratic in that coordinate, and keep the other two coordinates. It is defined on all of R³.

@[simp]

theorem TauCeti.markoffVieta_apply_self {R : Type u_1} [CommRing R] (i : Fin 3) (x : Fin 3 → R) : markoffVieta i x i = 3 * x (i + 1) * x (i + 2) - x i

The Vieta move R_i replaces x_i by 3 x_{i+1} x_{i+2} - x_i.

@[simp]

theorem TauCeti.markoffVieta_apply_of_ne {R : Type u_1} [CommRing R] {i j : Fin 3} (h : j ≠ i) (x : Fin 3 → R) : markoffVieta i x j = x j

The Vieta move R_i keeps every coordinate other than the i-th.

theorem TauCeti.markoffVieta_apply_self_add_self {R : Type u_1} [CommRing R] (i : Fin 3) (x : Fin 3 → R) : markoffVieta i x i + x i = 3 * x (i + 1) * x (i + 2)

The old and the new i-th coordinate are the two roots of a quadratic, so they sum to 3 x_{i+1} x_{i+2}.

theorem TauCeti.sum_markoffVieta {R : Type u_1} [CommRing R] (i : Fin 3) (x : Fin 3 → R) : ∑ j : Fin 3, markoffVieta i x j = ∑ j : Fin 3, x j + (markoffVieta i x i - x i)

A Vieta move changes the sum of the coordinates by the change in the moved coordinate.

@[simp]

theorem TauCeti.markoffVieta_zero {R : Type u_1} [CommRing R] (i : Fin 3) : markoffVieta i 0 = 0

The Vieta moves fix the origin.

theorem TauCeti.comp_markoffVieta {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (i : Fin 3) (x : Fin 3 → R) : ⇑f ∘ markoffVieta i x = markoffVieta i (⇑f ∘ x)

The Vieta moves commute with ring homomorphisms.

@[simp]

theorem TauCeti.markoffVieta_markoffVieta {R : Type u_1} [CommRing R] (i : Fin 3) (x : Fin 3 → R) : markoffVieta i (markoffVieta i x) = x

Applying the same Vieta move twice gives back the original triple.

theorem TauCeti.markoffVieta_involutive {R : Type u_1} [CommRing R] (i : Fin 3) : Function.Involutive (markoffVieta i)

Each Vieta move is an involution of R³, with no hypothesis on the ring or the triple.

@[simp]

theorem TauCeti.markoffVieta_inj {R : Type u_1} [CommRing R] {i : Fin 3} {x y : Fin 3 → R} : markoffVieta i x = markoffVieta i y ↔ x = y

Each Vieta move is injective.

@[simp]

theorem TauCeti.markoffVieta_eq_zero_iff {R : Type u_1} [CommRing R] {i : Fin 3} {x : Fin 3 → R} : markoffVieta i x = 0 ↔ x = 0

A Vieta move sends a triple to the origin only if the triple is the origin.

@[simp]

theorem TauCeti.markoffForm_markoffVieta {R : Type u_1} [CommRing R] (i : Fin 3) (x : Fin 3 → R) : markoffForm (markoffVieta i x) = markoffForm x

The Vieta moves preserve the Markoff form. This is a polynomial identity, valid before imposing the Markoff equation.

@[simp]

theorem TauCeti.markoffVieta_mem_markoffSet_iff {R : Type u_1} [CommRing R] {i : Fin 3} {x : Fin 3 → R} : markoffVieta i x ∈ markoffSet R ↔ x ∈ markoffSet R

The Vieta moves preserve the Markoff surface, in both directions.

@[simp]

theorem TauCeti.markoffVieta_mem_markoffSetNonzero_iff {R : Type u_1} [CommRing R] {i : Fin 3} {x : Fin 3 → R} : markoffVieta i x ∈ markoffSetNonzero R ↔ x ∈ markoffSetNonzero R

The Vieta moves preserve the nonzero locus X*(R), in both directions.

theorem TauCeti.bijOn_markoffVieta_markoffSetNonzero {R : Type u_1} [CommRing R] (i : Fin 3) : Set.BijOn (markoffVieta i) (markoffSetNonzero R) (markoffSetNonzero R)

Each Vieta move restricts to a bijection of the nonzero locus X*(R), which is its own inverse by markoffVieta_involutive.

theorem TauCeti.markoffVieta_comp_perm {R : Type u_1} [CommRing R] (σ : Equiv.Perm (Fin 3)) (i : Fin 3) (x : Fin 3 → R) : markoffVieta (σ i) (x ∘ ⇑(Equiv.symm σ)) = markoffVieta i x ∘ ⇑(Equiv.symm σ)

Coordinate permutations normalise the Vieta moves: with P_σ x = x ∘ σ⁻¹, so that (P_σ x) (σ i) = x i, one has P_σ ∘ R_i = R_{σ i} ∘ P_σ.

theorem TauCeti.markoffVieta_apply_self_mul_self {R : Type u_1} [CommRing R] {x : Fin 3 → R} (hx : x ∈ markoffSet R) (i : Fin 3) : markoffVieta i x i * x i = x (i + 1) ^ 2 + x (i + 2) ^ 2

If x lies on the Markoff surface, the two roots in the i-th coordinate multiply to x_{i+1}² + x_{i+2}² (Vieta's formula for the constant term).

Positive Markoff triples and the Markoff graph

def TauCeti.positiveMarkoffTriples : Set (Fin 3 → ℤ)

The positive Markoff triples M: the integer points of the Markoff surface all of whose coordinates are positive, kept as ordered triples.

theorem TauCeti.mem_positiveMarkoffTriples {x : Fin 3 → ℤ} : x ∈ positiveMarkoffTriples ↔ x ∈ markoffSet ℤ ∧ ∀ (i : Fin 3), 0 < x i

A positive Markoff triple is a point of X(ℤ) with positive coordinates.

theorem TauCeti.positiveMarkoffTriples_subset_markoffSet : positiveMarkoffTriples ⊆ markoffSet ℤ

Positive Markoff triples lie on the Markoff surface.

theorem TauCeti.positiveMarkoffTriples_subset_markoffSetNonzero : positiveMarkoffTriples ⊆ markoffSetNonzero ℤ

Positive Markoff triples lie in the nonzero locus X*(ℤ).

@[simp]

theorem TauCeti.one_mem_positiveMarkoffTriples : 1 ∈ positiveMarkoffTriples

The positive Markoff triple (1, 1, 1).

@[simp]

theorem TauCeti.comp_perm_mem_positiveMarkoffTriples_iff {x : Fin 3 → ℤ} {σ : Equiv.Perm (Fin 3)} : x ∘ ⇑σ ∈ positiveMarkoffTriples ↔ x ∈ positiveMarkoffTriples

The positive Markoff triples are stable under coordinate permutations.

theorem TauCeti.mem_positiveMarkoffTriples_iff_nat {x : Fin 3 → ℤ} : x ∈ positiveMarkoffTriples ↔ ∃ (a : ℕ) (b : ℕ) (c : ℕ), 0 < a ∧ 0 < b ∧ 0 < c ∧ a ^ 2 + b ^ 2 + c ^ 2 = 3 * a * b * c ∧ x = ![↑a, ↑b, ↑c]

Positive Markoff triples are the triples of positive natural numbers (a, b, c) with a² + b² + c² = 3abc; the equation has no subtraction, so it can be read in ℕ.

theorem TauCeti.markoffVieta_mem_positiveMarkoffTriples {x : Fin 3 → ℤ} (hx : x ∈ positiveMarkoffTriples) (i : Fin 3) : markoffVieta i x ∈ positiveMarkoffTriples

The Vieta moves preserve the positive Markoff triples: the new coordinate 3 x_{i+1} x_{i+2} - x_i is positive, because its product with x_i > 0 is x_{i+1}² + x_{i+2}² > 0.

@[simp]

theorem TauCeti.markoffVieta_mem_positiveMarkoffTriples_iff {i : Fin 3} {x : Fin 3 → ℤ} : markoffVieta i x ∈ positiveMarkoffTriples ↔ x ∈ positiveMarkoffTriples

The Vieta moves preserve the positive Markoff triples, in both directions.

def TauCeti.markoffGraph : SimpleGraph ↑positiveMarkoffTriples

The integer Markoff graph: the simple graph on the positive Markoff triples in which x and y are adjacent when they are distinct and y is obtained from x by a Vieta move.

theorem TauCeti.markoffGraph_adj {x y : ↑positiveMarkoffTriples} : markoffGraph.Adj x y ↔ x ≠ y ∧ ∃ (i : Fin 3), markoffVieta i ↑x = ↑y

Two positive Markoff triples are adjacent in the Markoff graph exactly when they are distinct and related by a Vieta move. Adjacency is symmetric because the moves are involutions.