Transporting the characteristic-zero opening through an algebraic closure

The archimedean argument is proved over ℂ, while the paper formulates the opening over an algebraic closure of ℚ. This file records the missing functorial step. A field embedding sends normalized Markoff points coordinatewise and intertwines the five generators. Closure induction on Gamma then shows that a finite orbit over the source field has finite image orbit over ℂ.

def BGS.Markoff.NormalizedPoint.map {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) (x : NormalizedPoint R) : NormalizedPoint S

Apply a ring homomorphism coordinatewise to a normalized trace point.

Equations

• BGS.Markoff.NormalizedPoint.map f x = { u1 := f x.u1, u2 := f x.u2, u3 := f x.u3 }

@[simp]

theorem BGS.Markoff.NormalizedPoint.map_u1 {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) (x : NormalizedPoint R) : (map f x).u1 = f x.u1

@[simp]

theorem BGS.Markoff.NormalizedPoint.map_u2 {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) (x : NormalizedPoint R) : (map f x).u2 = f x.u2

@[simp]

theorem BGS.Markoff.NormalizedPoint.map_u3 {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) (x : NormalizedPoint R) : (map f x).u3 = f x.u3

@[simp]

theorem BGS.Markoff.NormalizedPoint.map_origin {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) : map f normalizedOrigin = normalizedOrigin

@[simp]

theorem BGS.Markoff.normalizedPolynomial_map {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) (x : NormalizedPoint R) : normalizedPolynomial (NormalizedPoint.map f x) = f (normalizedPolynomial x)

def BGS.Markoff.normalizedSurfaceMap {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) (x : NormalizedMarkoffSurface R) : NormalizedMarkoffSurface S

A ring homomorphism sends the normalized Markoff surface to the normalized Markoff surface.

Equations

• BGS.Markoff.normalizedSurfaceMap f x = ⟨BGS.Markoff.NormalizedPoint.map f ↑x, ⋯⟩

@[simp]

theorem BGS.Markoff.coe_normalizedSurfaceMap {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) (x : NormalizedMarkoffSurface R) : ↑(normalizedSurfaceMap f x) = NormalizedPoint.map f ↑x

theorem BGS.Markoff.normalizedSurfaceMap_injective {R : Type u} {S : Type v} [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Injective ⇑f) : Function.Injective (normalizedSurfaceMap f)

theorem BGS.Markoff.exists_normalizedGamma_lift_along_fieldHom {K : Type u} {L : Type v} [Field K] [Field L] [Invertible 3] [Invertible 3] (f : K →+* L) (g : ↥(Gamma L)) : ∃ (h : ↥(Gamma K)), ∀ (x : NormalizedMarkoffSurface K), normalizedSurfaceMap f (h • x) = g • normalizedSurfaceMap f x

Every normalized Gamma word over the target field has a source-field word with the same action after applying a field embedding.

theorem BGS.Markoff.normalizedGammaOrbit_map_subset {K : Type u} {L : Type v} [Field K] [Field L] [Invertible 3] [Invertible 3] (f : K →+* L) (x : NormalizedMarkoffSurface K) : normalizedGammaOrbit (normalizedSurfaceMap f x) ⊆ normalizedSurfaceMap f '' normalizedGammaOrbit x

The target-field orbit of the mapped point is contained in the image of the source orbit.

theorem BGS.Markoff.finite_normalizedGammaOrbit_map {K : Type u} {L : Type v} [Field K] [Field L] [Invertible 3] [Invertible 3] (f : K →+* L) (x : NormalizedMarkoffSurface K) (hfinite : (normalizedGammaOrbit x).Finite) : (normalizedGammaOrbit (normalizedSurfaceMap f x)).Finite

A finite normalized orbit stays finite after applying a field embedding.

theorem BGS.Markoff.normalizedGammaOrbit_infinite_of_ne_origin_of_complexEmbedding {K : Type u} [Field K] [Invertible 3] (f : K →+* ℂ) (x : NormalizedMarkoffSurface K) (hx : ↑x ≠ normalizedOrigin) : (normalizedGammaOrbit x).Infinite

The complex opening theorem descends along any field embedding into ℂ.

noncomputable def BGS.Markoff.algebraicClosureRatComplexEmbedding : AlgebraicClosure ℚ →+* ℂ

A chosen embedding of the canonical algebraic closure of ℚ into ℂ.

Equations

• BGS.Markoff.algebraicClosureRatComplexEmbedding = IsAlgClosed.lift.toRingHom

theorem BGS.Markoff.algebraicClosureRat_normalizedGammaOrbit_infinite_of_ne_origin (x : NormalizedMarkoffSurface (AlgebraicClosure ℚ)) (hx : ↑x ≠ normalizedOrigin) : (normalizedGammaOrbit x).Infinite

The published characteristic-zero opening: every nonzero normalized Markoff point over the canonical algebraic closure of ℚ has infinite Gamma-orbit.