The elementary Markoff surface

This file fixes the unscaled coordinates used in the introduction of Bourgain--Gamburd--Sarnak, arXiv:1607.01530v1. Later parts of the paper use trace coordinates obtained by multiplying each coordinate by three; that normalization is deliberately kept separate.

structure BGS.Markoff.Point (R : Type u) : Type u

A point of affine three-space over a type R.

• x1 : R

  The first coordinate.

• x2 : R

  The second coordinate.

• x3 : R

  The third coordinate.

theorem BGS.Markoff.Point.ext_iff {R : Type u} {x y : Point R} : x = y ↔ x.x1 = y.x1 ∧ x.x2 = y.x2 ∧ x.x3 = y.x3

theorem BGS.Markoff.Point.ext {R : Type u} {x y : Point R} (x1 : x.x1 = y.x1) (x2 : x.x2 = y.x2) (x3 : x.x3 = y.x3) : x = y

def BGS.Markoff.instDecidableEqPoint.decEq {R✝ : Type u_1} [DecidableEq R✝] (x✝ x✝¹ : Point R✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance BGS.Markoff.instDecidableEqPoint {R✝ : Type u_1} [DecidableEq R✝] : DecidableEq (Point R✝)

Equations

• BGS.Markoff.instDecidableEqPoint = BGS.Markoff.instDecidableEqPoint.decEq

@[instance_reducible]

instance BGS.Markoff.instReprPoint {R✝ : Type u_1} [Repr R✝] : Repr (Point R✝)

Equations

• BGS.Markoff.instReprPoint = { reprPrec := BGS.Markoff.instReprPoint.repr }

def BGS.Markoff.instReprPoint.repr {R✝ : Type u_1} [Repr R✝] : Point R✝ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance BGS.Markoff.instFintypePoint {R✝ : Type u_1} [Fintype R✝] : Fintype (Point R✝)

Equations

• BGS.Markoff.instFintypePoint = Fintype.ofEquiv ((_ : R✝) × (_ : R✝) × R✝) (BGS.Markoff.Point.proxyTypeEquiv R✝)

def BGS.Markoff.origin {R : Type u} [Zero R] : Point R

The origin in affine three-space.

Equations

• BGS.Markoff.origin = { x1 := 0, x2 := 0, x3 := 0 }

def BGS.Markoff.markoffPolynomial {R : Type u} [CommRing R] (x : Point R) : R

The polynomial whose zero locus is the Markoff surface.

Equations

• BGS.Markoff.markoffPolynomial x = x.x1 ^ 2 + x.x2 ^ 2 + x.x3 ^ 2 - 3 * x.x1 * x.x2 * x.x3

def BGS.Markoff.IsMarkoff {R : Type u} [CommRing R] (x : Point R) : Prop

The predicate that a point lies on the Markoff surface.

Equations

• BGS.Markoff.IsMarkoff x = (BGS.Markoff.markoffPolynomial x = 0)

def BGS.Markoff.surface (R : Type u) [CommRing R] : Set (Point R)

The Markoff surface as a set.

Equations

• BGS.Markoff.surface R = {x : BGS.Markoff.Point R | BGS.Markoff.IsMarkoff x}

def BGS.Markoff.puncturedSurface (R : Type u) [CommRing R] : Set (Point R)

The punctured Markoff surface, with the origin removed.

Equations

• BGS.Markoff.puncturedSurface R = BGS.Markoff.surface R \ {BGS.Markoff.origin}

def BGS.Markoff.vieta1 {R : Type u} [CommRing R] (x : Point R) : Point R

The first Vieta involution.

Equations

• BGS.Markoff.vieta1 x = { x1 := 3 * x.x2 * x.x3 - x.x1, x2 := x.x2, x3 := x.x3 }

def BGS.Markoff.vieta2 {R : Type u} [CommRing R] (x : Point R) : Point R

The second Vieta involution.

Equations

• BGS.Markoff.vieta2 x = { x1 := x.x1, x2 := 3 * x.x1 * x.x3 - x.x2, x3 := x.x3 }

def BGS.Markoff.vieta3 {R : Type u} [CommRing R] (x : Point R) : Point R

The third Vieta involution.

Equations

• BGS.Markoff.vieta3 x = { x1 := x.x1, x2 := x.x2, x3 := 3 * x.x1 * x.x2 - x.x3 }

def BGS.Markoff.swap12 {R : Type u} (x : Point R) : Point R

Exchange the first two coordinates.

Equations

• BGS.Markoff.swap12 x = { x1 := x.x2, x2 := x.x1, x3 := x.x3 }

def BGS.Markoff.swap23 {R : Type u} (x : Point R) : Point R

Exchange the last two coordinates.

Equations

• BGS.Markoff.swap23 x = { x1 := x.x1, x2 := x.x3, x3 := x.x2 }

def BGS.Markoff.rotate1 {R : Type u} [CommRing R] (x : Point R) : Point R

The fundamental rotation fixing the first coordinate.

Equations

• BGS.Markoff.rotate1 x = { x1 := x.x1, x2 := x.x3, x3 := 3 * x.x1 * x.x3 - x.x2 }

@[simp]

theorem BGS.Markoff.markoffPolynomial_origin {R : Type u} [CommRing R] : markoffPolynomial origin = 0

@[simp]

theorem BGS.Markoff.isMarkoff_origin {R : Type u} [CommRing R] : IsMarkoff origin

theorem BGS.Markoff.markoffPolynomial_vieta1 {R : Type u} [CommRing R] (x : Point R) : markoffPolynomial (vieta1 x) = markoffPolynomial x

theorem BGS.Markoff.markoffPolynomial_vieta2 {R : Type u} [CommRing R] (x : Point R) : markoffPolynomial (vieta2 x) = markoffPolynomial x

theorem BGS.Markoff.markoffPolynomial_vieta3 {R : Type u} [CommRing R] (x : Point R) : markoffPolynomial (vieta3 x) = markoffPolynomial x

theorem BGS.Markoff.markoffPolynomial_swap12 {R : Type u} [CommRing R] (x : Point R) : markoffPolynomial (swap12 x) = markoffPolynomial x

theorem BGS.Markoff.markoffPolynomial_swap23 {R : Type u} [CommRing R] (x : Point R) : markoffPolynomial (swap23 x) = markoffPolynomial x

theorem BGS.Markoff.markoffPolynomial_rotate1 {R : Type u} [CommRing R] (x : Point R) : markoffPolynomial (rotate1 x) = markoffPolynomial x

@[simp]

theorem BGS.Markoff.isMarkoff_vieta1 {R : Type u} [CommRing R] (x : Point R) : IsMarkoff (vieta1 x) ↔ IsMarkoff x

@[simp]

theorem BGS.Markoff.isMarkoff_vieta2 {R : Type u} [CommRing R] (x : Point R) : IsMarkoff (vieta2 x) ↔ IsMarkoff x

@[simp]

theorem BGS.Markoff.isMarkoff_vieta3 {R : Type u} [CommRing R] (x : Point R) : IsMarkoff (vieta3 x) ↔ IsMarkoff x

@[simp]

theorem BGS.Markoff.isMarkoff_rotate1 {R : Type u} [CommRing R] (x : Point R) : IsMarkoff (rotate1 x) ↔ IsMarkoff x

@[simp]

theorem BGS.Markoff.vieta1_involutive {R : Type u} [CommRing R] (x : Point R) : vieta1 (vieta1 x) = x

@[simp]

theorem BGS.Markoff.vieta2_involutive {R : Type u} [CommRing R] (x : Point R) : vieta2 (vieta2 x) = x

@[simp]

theorem BGS.Markoff.vieta3_involutive {R : Type u} [CommRing R] (x : Point R) : vieta3 (vieta3 x) = x

@[simp]

theorem BGS.Markoff.swap12_involutive {R : Type u} (x : Point R) : swap12 (swap12 x) = x

@[simp]

theorem BGS.Markoff.swap23_involutive {R : Type u} (x : Point R) : swap23 (swap23 x) = x

def BGS.Markoff.vieta1Equiv (R : Type u) [CommRing R] : Equiv.Perm (Point R)

The first Vieta move as a permutation of affine three-space.

Equations

• BGS.Markoff.vieta1Equiv R = { toFun := BGS.Markoff.vieta1, invFun := BGS.Markoff.vieta1, left_inv := ⋯, right_inv := ⋯ }

def BGS.Markoff.vieta2Equiv (R : Type u) [CommRing R] : Equiv.Perm (Point R)

The second Vieta move as a permutation of affine three-space.

Equations

• BGS.Markoff.vieta2Equiv R = { toFun := BGS.Markoff.vieta2, invFun := BGS.Markoff.vieta2, left_inv := ⋯, right_inv := ⋯ }

def BGS.Markoff.vieta3Equiv (R : Type u) [CommRing R] : Equiv.Perm (Point R)

The third Vieta move as a permutation of affine three-space.

Equations

• BGS.Markoff.vieta3Equiv R = { toFun := BGS.Markoff.vieta3, invFun := BGS.Markoff.vieta3, left_inv := ⋯, right_inv := ⋯ }

def BGS.Markoff.swap12Equiv (R : Type u) : Equiv.Perm (Point R)

The transposition of the first two coordinates as a permutation.

Equations

• BGS.Markoff.swap12Equiv R = { toFun := BGS.Markoff.swap12, invFun := BGS.Markoff.swap12, left_inv := ⋯, right_inv := ⋯ }

def BGS.Markoff.swap23Equiv (R : Type u) : Equiv.Perm (Point R)

The transposition of the last two coordinates as a permutation.

Equations

• BGS.Markoff.swap23Equiv R = { toFun := BGS.Markoff.swap23, invFun := BGS.Markoff.swap23, left_inv := ⋯, right_inv := ⋯ }