Normalized coordinates on the Markoff surface

The paper silently passes from the original coordinates x to trace coordinates u = 3x. This file gives the normalized affine space a distinct type, defines its Markoff equation and Vieta moves, and proves that coordinatewise scaling by three identifies the two theories whenever three is invertible.

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

A point in normalized trace coordinates. This is intentionally not definitionally equal to the original-coordinate type Point R.

• u1 : R

  The first normalized trace coordinate.

• u2 : R

  The second normalized trace coordinate.

• u3 : R

  The third normalized trace coordinate.

theorem BGS.Markoff.NormalizedPoint.ext {R : Type u} {x y : NormalizedPoint R} (u1 : x.u1 = y.u1) (u2 : x.u2 = y.u2) (u3 : x.u3 = y.u3) : x = y

theorem BGS.Markoff.NormalizedPoint.ext_iff {R : Type u} {x y : NormalizedPoint R} : x = y ↔ x.u1 = y.u1 ∧ x.u2 = y.u2 ∧ x.u3 = y.u3

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

Equations

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

@[instance_reducible]

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

Equations

• BGS.Markoff.instDecidableEqNormalizedPoint = BGS.Markoff.instDecidableEqNormalizedPoint.decEq

@[instance_reducible]

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

Equations

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

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

Equations

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

@[instance_reducible]

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

Equations

• BGS.Markoff.instFintypeNormalizedPoint = Fintype.ofEquiv ((_ : R✝) × (_ : R✝) × R✝) (BGS.Markoff.NormalizedPoint.proxyTypeEquiv R✝)

def BGS.Markoff.normalizedOrigin {R : Type u} [Zero R] : NormalizedPoint R

The origin in normalized trace coordinates.

Equations

• BGS.Markoff.normalizedOrigin = { u1 := 0, u2 := 0, u3 := 0 }

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

The normalized Markoff polynomial u₁² + u₂² + u₃² - u₁u₂u₃.

Equations

• BGS.Markoff.normalizedPolynomial x = x.u1 ^ 2 + x.u2 ^ 2 + x.u3 ^ 2 - x.u1 * x.u2 * x.u3

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

The predicate that a normalized point lies on the normalized Markoff surface.

Equations

• BGS.Markoff.IsNormalizedMarkoff x = (BGS.Markoff.normalizedPolynomial x = 0)

def BGS.Markoff.normalizedSurface (R : Type u) [CommRing R] : Set (NormalizedPoint R)

The normalized Markoff surface.

Equations

• BGS.Markoff.normalizedSurface R = {x : BGS.Markoff.NormalizedPoint R | BGS.Markoff.IsNormalizedMarkoff x}

def BGS.Markoff.normalizedPuncturedSurface (R : Type u) [CommRing R] : Set (NormalizedPoint R)

The normalized Markoff surface with the origin removed.

Equations

• BGS.Markoff.normalizedPuncturedSurface R = BGS.Markoff.normalizedSurface R \ {BGS.Markoff.normalizedOrigin}

def BGS.Markoff.normalizedFiber1 {R : Type u} [CommRing R] (a : R) : Set (NormalizedPoint R)

The normalized Markoff fiber obtained by fixing the first coordinate.

Equations

• BGS.Markoff.normalizedFiber1 a = {x : BGS.Markoff.NormalizedPoint R | BGS.Markoff.IsNormalizedMarkoff x ∧ x.u1 = a}

def BGS.Markoff.normalizedFiber2 {R : Type u} [CommRing R] (a : R) : Set (NormalizedPoint R)

The normalized Markoff fiber obtained by fixing the second coordinate.

Equations

• BGS.Markoff.normalizedFiber2 a = {x : BGS.Markoff.NormalizedPoint R | BGS.Markoff.IsNormalizedMarkoff x ∧ x.u2 = a}

def BGS.Markoff.normalizedFiber3 {R : Type u} [CommRing R] (a : R) : Set (NormalizedPoint R)

The normalized Markoff fiber obtained by fixing the third coordinate.

Equations

• BGS.Markoff.normalizedFiber3 a = {x : BGS.Markoff.NormalizedPoint R | BGS.Markoff.IsNormalizedMarkoff x ∧ x.u3 = a}

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

The first Vieta involution in normalized coordinates.

Equations

• BGS.Markoff.normalizedVieta1 x = { u1 := x.u2 * x.u3 - x.u1, u2 := x.u2, u3 := x.u3 }

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

The second Vieta involution in normalized coordinates.

Equations

• BGS.Markoff.normalizedVieta2 x = { u1 := x.u1, u2 := x.u1 * x.u3 - x.u2, u3 := x.u3 }

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

The third Vieta involution in normalized coordinates.

Equations

• BGS.Markoff.normalizedVieta3 x = { u1 := x.u1, u2 := x.u2, u3 := x.u1 * x.u2 - x.u3 }

def BGS.Markoff.normalizedSwap12 {R : Type u} (x : NormalizedPoint R) : NormalizedPoint R

Exchange the first two normalized coordinates.

Equations

• BGS.Markoff.normalizedSwap12 x = { u1 := x.u2, u2 := x.u1, u3 := x.u3 }

def BGS.Markoff.normalizedSwap23 {R : Type u} (x : NormalizedPoint R) : NormalizedPoint R

Exchange the last two normalized coordinates.

Equations

• BGS.Markoff.normalizedSwap23 x = { u1 := x.u1, u2 := x.u3, u3 := x.u2 }

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

The fundamental rotation fixing the first normalized coordinate.

Equations

• BGS.Markoff.normalizedRotate1 x = { u1 := x.u1, u2 := x.u3, u3 := x.u1 * x.u3 - x.u2 }

@[simp]

theorem BGS.Markoff.normalizedPolynomial_origin {R : Type u} [CommRing R] : normalizedPolynomial normalizedOrigin = 0

@[simp]

theorem BGS.Markoff.isNormalizedMarkoff_origin {R : Type u} [CommRing R] : IsNormalizedMarkoff normalizedOrigin

theorem BGS.Markoff.normalizedPolynomial_vieta1 {R : Type u} [CommRing R] (x : NormalizedPoint R) : normalizedPolynomial (normalizedVieta1 x) = normalizedPolynomial x

theorem BGS.Markoff.normalizedPolynomial_vieta2 {R : Type u} [CommRing R] (x : NormalizedPoint R) : normalizedPolynomial (normalizedVieta2 x) = normalizedPolynomial x

theorem BGS.Markoff.normalizedPolynomial_vieta3 {R : Type u} [CommRing R] (x : NormalizedPoint R) : normalizedPolynomial (normalizedVieta3 x) = normalizedPolynomial x

theorem BGS.Markoff.normalizedPolynomial_swap12 {R : Type u} [CommRing R] (x : NormalizedPoint R) : normalizedPolynomial (normalizedSwap12 x) = normalizedPolynomial x

theorem BGS.Markoff.normalizedPolynomial_swap23 {R : Type u} [CommRing R] (x : NormalizedPoint R) : normalizedPolynomial (normalizedSwap23 x) = normalizedPolynomial x

theorem BGS.Markoff.normalizedPolynomial_rotate1 {R : Type u} [CommRing R] (x : NormalizedPoint R) : normalizedPolynomial (normalizedRotate1 x) = normalizedPolynomial x

@[simp]

theorem BGS.Markoff.isNormalizedMarkoff_vieta1 {R : Type u} [CommRing R] (x : NormalizedPoint R) : IsNormalizedMarkoff (normalizedVieta1 x) ↔ IsNormalizedMarkoff x

@[simp]

theorem BGS.Markoff.isNormalizedMarkoff_vieta2 {R : Type u} [CommRing R] (x : NormalizedPoint R) : IsNormalizedMarkoff (normalizedVieta2 x) ↔ IsNormalizedMarkoff x

@[simp]

theorem BGS.Markoff.isNormalizedMarkoff_vieta3 {R : Type u} [CommRing R] (x : NormalizedPoint R) : IsNormalizedMarkoff (normalizedVieta3 x) ↔ IsNormalizedMarkoff x

@[simp]

theorem BGS.Markoff.isNormalizedMarkoff_rotate1 {R : Type u} [CommRing R] (x : NormalizedPoint R) : IsNormalizedMarkoff (normalizedRotate1 x) ↔ IsNormalizedMarkoff x

theorem BGS.Markoff.normalizedRotate1_mem_fiber1_iff {R : Type u} [CommRing R] (a : R) (x : NormalizedPoint R) : normalizedRotate1 x ∈ normalizedFiber1 a ↔ x ∈ normalizedFiber1 a

The normalized rotation fixes, and therefore preserves, its first-coordinate fiber.

@[simp]

theorem BGS.Markoff.normalizedVieta1_involutive {R : Type u} [CommRing R] (x : NormalizedPoint R) : normalizedVieta1 (normalizedVieta1 x) = x

@[simp]

theorem BGS.Markoff.normalizedVieta2_involutive {R : Type u} [CommRing R] (x : NormalizedPoint R) : normalizedVieta2 (normalizedVieta2 x) = x

@[simp]

theorem BGS.Markoff.normalizedVieta3_involutive {R : Type u} [CommRing R] (x : NormalizedPoint R) : normalizedVieta3 (normalizedVieta3 x) = x

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

Coordinatewise multiplication by three, from original to normalized coordinates.

Equations

• BGS.Markoff.toNormalized x = { u1 := 3 * x.x1, u2 := 3 * x.x2, u3 := 3 * x.x3 }

def BGS.Markoff.fromNormalized {R : Type u} [CommRing R] [Invertible 3] (x : NormalizedPoint R) : Point R

Coordinatewise multiplication by the specified inverse of three.

Equations

• BGS.Markoff.fromNormalized x = { x1 := ⅟3 * x.u1, x2 := ⅟3 * x.u2, x3 := ⅟3 * x.u3 }

@[simp]

theorem BGS.Markoff.toNormalized_origin {R : Type u} [CommRing R] : toNormalized origin = normalizedOrigin

@[simp]

theorem BGS.Markoff.fromNormalized_origin {R : Type u} [CommRing R] [Invertible 3] : fromNormalized normalizedOrigin = origin

theorem BGS.Markoff.normalizedPolynomial_toNormalized {R : Type u} [CommRing R] (x : Point R) : normalizedPolynomial (toNormalized x) = 3 ^ 2 * markoffPolynomial x

Scaling multiplies the Markoff polynomial by 3². This identity itself does not need three to be invertible.

@[simp]

theorem BGS.Markoff.isNormalizedMarkoff_toNormalized_iff {R : Type u} [CommRing R] [Invertible 3] (x : Point R) : IsNormalizedMarkoff (toNormalized x) ↔ IsMarkoff x

When three is invertible, scaling takes the original Markoff equation to the normalized one and reflects it.

def BGS.Markoff.normalizationEquiv (R : Type u) [CommRing R] [Invertible 3] : Point R ≃ NormalizedPoint R

Coordinatewise scaling by three as an equivalence of the two ambient affine spaces.

Equations

• BGS.Markoff.normalizationEquiv R = { toFun := BGS.Markoff.toNormalized, invFun := BGS.Markoff.fromNormalized, left_inv := ⋯, right_inv := ⋯ }

def BGS.Markoff.normalizationSurfaceEquiv (R : Type u) [CommRing R] [Invertible 3] : { x : Point R // IsMarkoff x } ≃ { x : NormalizedPoint R // IsNormalizedMarkoff x }

Scaling by three restricts to an equivalence of the original and normalized Markoff surfaces.

Equations

• BGS.Markoff.normalizationSurfaceEquiv R = (BGS.Markoff.normalizationEquiv R).subtypeEquiv ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem BGS.Markoff.toNormalized_swap12 {R : Type u} [CommRing R] (x : Point R) : toNormalized (swap12 x) = normalizedSwap12 (toNormalized x)

@[simp]

theorem BGS.Markoff.toNormalized_swap23 {R : Type u} [CommRing R] (x : Point R) : toNormalized (swap23 x) = normalizedSwap23 (toNormalized x)

@[simp]

theorem BGS.Markoff.toNormalized_rotate1 {R : Type u} [CommRing R] (x : Point R) : toNormalized (rotate1 x) = normalizedRotate1 (toNormalized x)