Markoff components in normalized coordinates

The Markoff group is defined on the original-coordinate surface. This file transports its permutations and component relation through normalizationSurfaceEquiv. It also records the specific group word for the fundamental rotation and proves that every iterate of the normalized rotation stays in the same transported component.

@[reducible, inline]

abbrev BGS.Markoff.NormalizedMarkoffSurface (R : Type u) [CommRing R] : Type u

The normalized Markoff surface as a subtype.

Equations

• BGS.Markoff.NormalizedMarkoffSurface R = { x : BGS.Markoff.NormalizedPoint R // BGS.Markoff.IsNormalizedMarkoff x }

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

The fundamental rotation, restricted to the original-coordinate Markoff surface.

Equations

• BGS.Markoff.rotate1Surface x = ⟨BGS.Markoff.rotate1 ↑x, ⋯⟩

@[simp]

theorem BGS.Markoff.coe_rotate1Surface {R : Type u} [CommRing R] (x : MarkoffSurface R) : ↑(rotate1Surface x) = rotate1 ↑x

theorem BGS.Markoff.rotate1Surface_eq_swap23_after_vieta2 {R : Type u} [CommRing R] (x : MarkoffSurface R) : rotate1Surface x = (swap23SurfacePerm R) ((vieta2SurfacePerm R) x)

The rotation fixing the first coordinate is swap23 after the second Vieta involution.

def BGS.Markoff.gammaRotate1 (R : Type u) [CommRing R] : ↥(Gamma R)

The explicit element of Gamma realizing the fundamental rotation.

Equations

• BGS.Markoff.gammaRotate1 R = BGS.Markoff.gammaSwap23 R * BGS.Markoff.gammaVieta2 R

@[simp]

theorem BGS.Markoff.gammaRotate1_smul_surface {R : Type u} [CommRing R] (x : MarkoffSurface R) : gammaRotate1 R • x = rotate1Surface x

theorem BGS.Markoff.sameComponent_rotate1Surface {R : Type u} [CommRing R] (x : MarkoffSurface R) : SameComponent x (rotate1Surface x)

A fundamental rotation is an honest move in the Markoff group.

def BGS.Markoff.normalizedGammaPerm (R : Type u) [CommRing R] [Invertible 3] (g : ↥(Gamma R)) : Equiv.Perm (NormalizedMarkoffSurface R)

Conjugate an element of the original Markoff group to normalized coordinates.

Equations

• BGS.Markoff.normalizedGammaPerm R g = (BGS.Markoff.normalizationSurfaceEquiv R).symm.trans (Equiv.trans (↑g) (BGS.Markoff.normalizationSurfaceEquiv R))

@[simp]

theorem BGS.Markoff.normalizedGammaPerm_apply {R : Type u} [CommRing R] [Invertible 3] (g : ↥(Gamma R)) (x : NormalizedMarkoffSurface R) : (normalizedGammaPerm R g) x = (normalizationSurfaceEquiv R) (↑g ((normalizationSurfaceEquiv R).symm x))

@[instance_reducible]

instance BGS.Markoff.normalizedGammaMulAction {R : Type u} [CommRing R] [Invertible 3] : MulAction (↥(Gamma R)) (NormalizedMarkoffSurface R)

The conjugated permutations give the transported Gamma action on the normalized surface.

Equations

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

@[simp]

theorem BGS.Markoff.normalizedGamma_smul_eq_perm {R : Type u} [CommRing R] [Invertible 3] (g : ↥(Gamma R)) (x : NormalizedMarkoffSurface R) : g • x = (normalizedGammaPerm R g) x

def BGS.Markoff.normalizedGammaOrbit {R : Type u} [CommRing R] [Invertible 3] (x : NormalizedMarkoffSurface R) : Set (NormalizedMarkoffSurface R)

The orbit of a normalized point under the transported Gamma action.

Equations

• BGS.Markoff.normalizedGammaOrbit x = MulAction.orbit (↥(BGS.Markoff.Gamma R)) x

def BGS.Markoff.SameNormalizedComponent {R : Type u} [CommRing R] [Invertible 3] (x y : NormalizedMarkoffSurface R) : Prop

Two normalized points are in the same component exactly when their inverse normalizations are in one original-coordinate Gamma-orbit.

Equations

• BGS.Markoff.SameNormalizedComponent x y = BGS.Markoff.SameComponent ((BGS.Markoff.normalizationSurfaceEquiv R).symm x) ((BGS.Markoff.normalizationSurfaceEquiv R).symm y)

theorem BGS.Markoff.sameNormalizedComponent_iff_exists_gamma {R : Type u} [CommRing R] [Invertible 3] (x y : NormalizedMarkoffSurface R) : SameNormalizedComponent x y ↔ ∃ (g : ↥(Gamma R)), (normalizedGammaPerm R g) x = y

Orbit membership in normalized coordinates is witnessed by a conjugated element of Gamma.

theorem BGS.Markoff.sameNormalizedComponent_iff_mem_normalizedGammaOrbit {R : Type u} [CommRing R] [Invertible 3] (x y : NormalizedMarkoffSurface R) : SameNormalizedComponent x y ↔ y ∈ normalizedGammaOrbit x

The transported component relation agrees with the orbit of the transported action.

theorem BGS.Markoff.sameNormalizedComponent_refl {R : Type u} [CommRing R] [Invertible 3] (x : NormalizedMarkoffSurface R) : SameNormalizedComponent x x

theorem BGS.Markoff.sameNormalizedComponent_symm {R : Type u} [CommRing R] [Invertible 3] {x y : NormalizedMarkoffSurface R} (h : SameNormalizedComponent x y) : SameNormalizedComponent y x

theorem BGS.Markoff.sameNormalizedComponent_trans {R : Type u} [CommRing R] [Invertible 3] {x y z : NormalizedMarkoffSurface R} (hxy : SameNormalizedComponent x y) (hyz : SameNormalizedComponent y z) : SameNormalizedComponent x z

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

Exchange the first two normalized coordinates on the normalized surface.

Equations

• BGS.Markoff.normalizedSwap12Surface x = ⟨BGS.Markoff.normalizedSwap12 ↑x, ⋯⟩

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

Exchange the last two normalized coordinates on the normalized surface.

Equations

• BGS.Markoff.normalizedSwap23Surface x = ⟨BGS.Markoff.normalizedSwap23 ↑x, ⋯⟩

@[simp]

theorem BGS.Markoff.coe_normalizedSwap12Surface {R : Type u} [CommRing R] (x : NormalizedMarkoffSurface R) : ↑(normalizedSwap12Surface x) = normalizedSwap12 ↑x

@[simp]

theorem BGS.Markoff.coe_normalizedSwap23Surface {R : Type u} [CommRing R] (x : NormalizedMarkoffSurface R) : ↑(normalizedSwap23Surface x) = normalizedSwap23 ↑x

theorem BGS.Markoff.normalizedSwap12Surface_eq_transport {R : Type u} [CommRing R] [Invertible 3] (x : NormalizedMarkoffSurface R) : normalizedSwap12Surface x = (normalizationSurfaceEquiv R) ((swap12SurfacePerm R) ((normalizationSurfaceEquiv R).symm x))

The first normalized transposition is transported from the original surface.

theorem BGS.Markoff.normalizedSwap23Surface_eq_transport {R : Type u} [CommRing R] [Invertible 3] (x : NormalizedMarkoffSurface R) : normalizedSwap23Surface x = (normalizationSurfaceEquiv R) ((swap23SurfacePerm R) ((normalizationSurfaceEquiv R).symm x))

The second normalized transposition is transported from the original surface.

theorem BGS.Markoff.gammaSwap12_smul_normalizedSurface {R : Type u} [CommRing R] [Invertible 3] (x : NormalizedMarkoffSurface R) : gammaSwap12 R • x = normalizedSwap12Surface x

The transported first coordinate transposition is the normalized swap.

theorem BGS.Markoff.gammaSwap23_smul_normalizedSurface {R : Type u} [CommRing R] [Invertible 3] (x : NormalizedMarkoffSurface R) : gammaSwap23 R • x = normalizedSwap23Surface x

The transported second coordinate transposition is the normalized swap.

theorem BGS.Markoff.sameNormalizedComponent_swap12Surface {R : Type u} [CommRing R] [Invertible 3] (x : NormalizedMarkoffSurface R) : SameNormalizedComponent x (normalizedSwap12Surface x)

Swapping the first two normalized coordinates stays in the same component.

theorem BGS.Markoff.sameNormalizedComponent_swap23Surface {R : Type u} [CommRing R] [Invertible 3] (x : NormalizedMarkoffSurface R) : SameNormalizedComponent x (normalizedSwap23Surface x)

Swapping the last two normalized coordinates stays in the same component.

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

The fundamental normalized rotation, restricted to the normalized surface.

Equations

• BGS.Markoff.normalizedRotate1Surface x = ⟨BGS.Markoff.normalizedRotate1 ↑x, ⋯⟩

@[simp]

theorem BGS.Markoff.coe_normalizedRotate1Surface {R : Type u} [CommRing R] (x : NormalizedMarkoffSurface R) : ↑(normalizedRotate1Surface x) = normalizedRotate1 ↑x

theorem BGS.Markoff.normalizedRotate1Surface_eq_transport {R : Type u} [CommRing R] [Invertible 3] (x : NormalizedMarkoffSurface R) : normalizedRotate1Surface x = (normalizationSurfaceEquiv R) (rotate1Surface ((normalizationSurfaceEquiv R).symm x))

Normalized rotation is the normalization of the original surface rotation.

theorem BGS.Markoff.gammaRotate1_smul_normalizedSurface {R : Type u} [CommRing R] [Invertible 3] (x : NormalizedMarkoffSurface R) : gammaRotate1 R • x = normalizedRotate1Surface x

The transported explicit rotation element acts by normalized rotation.

theorem BGS.Markoff.sameNormalizedComponent_rotate1Surface {R : Type u} [CommRing R] [Invertible 3] (x : NormalizedMarkoffSurface R) : SameNormalizedComponent x (normalizedRotate1Surface x)

One normalized rotation stays in the transported Markoff component.

theorem BGS.Markoff.sameNormalizedComponent_iterate_normalizedRotate1Surface {R : Type u} [CommRing R] [Invertible 3] (x : NormalizedMarkoffSurface R) (n : ℕ) : SameNormalizedComponent x (normalizedRotate1Surface^[n] x)

Every natural iterate of the normalized rotation stays in the same transported component.

theorem BGS.Markoff.sameNormalizedComponent_positive_iterate_normalizedRotate1Surface {R : Type u} [CommRing R] [Invertible 3] (x : NormalizedMarkoffSurface R) (n : ℕ) (_hn : 0 < n) : SameNormalizedComponent x (normalizedRotate1Surface^[n] x)

In particular, every positive iterate stays in the same transported component.