The Markoff surface on commutative semirings

The usual polynomial presentation by subtraction only makes sense over rings. For strong approximation from natural-number solutions, the equation itself is the more fundamental definition:

x₁² + x₂² + x₃² = 3 * x₁ * x₂ * x₃.

This file defines that solution type over every commutative semiring and its covariant map along semiring homomorphisms. It also records the canonical reduction from ℕ to ZMod p and compares the semiring definition with the existing ring-level MarkoffSurface.

def BGS.Markoff : CategoryTheory.Functor CommSemiRingCat Type

The Markoff surface, functorially evaluated on commutative semirings.

Equations

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

def BGS.Markoff.StrongApproximationAt (p : ℕ) : Prop

Strong approximation at modulus p: every Markoff solution modulo p is the reduction of a natural-number solution.

Equations

• BGS.Markoff.StrongApproximationAt p = Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (BGS.Markoff.map (CommSemiRingCat.ofHom (Nat.castRingHom (ZMod p)))))

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

A point satisfies the Markoff equation over a commutative semiring.

Equations

• BGS.Markoff.IsSemiringMarkoff x = (x.x1 ^ 2 + x.x2 ^ 2 + x.x3 ^ 2 = 3 * x.x1 * x.x2 * x.x3)

@[reducible, inline]

abbrev BGS.Markoff.SemiringMarkoffSurface (R : Type u) [CommSemiring R] : Type u

Markoff solutions over a commutative semiring.

Equations

• BGS.Markoff.SemiringMarkoffSurface R = { x : BGS.Markoff.Point R // BGS.Markoff.IsSemiringMarkoff x }

@[reducible, inline]

abbrev BGS.Markoff.MarkoffSolutions (R : Type u) [CommSemiring R] : Type u

A concise name for the semiring-valued solution type of the Markoff equation.

Equations

• BGS.Markoff.MarkoffSolutions R = BGS.Markoff.SemiringMarkoffSurface R

def BGS.Markoff.semiringPointMap {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) (x : Point R) : Point S

Apply a semiring homomorphism coordinatewise to a point of affine three-space.

Equations

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

@[simp]

theorem BGS.Markoff.semiringPointMap_x1 {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) (x : Point R) : (semiringPointMap f x).x1 = f x.x1

@[simp]

theorem BGS.Markoff.semiringPointMap_x2 {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) (x : Point R) : (semiringPointMap f x).x2 = f x.x2

@[simp]

theorem BGS.Markoff.semiringPointMap_x3 {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) (x : Point R) : (semiringPointMap f x).x3 = f x.x3

theorem BGS.Markoff.isSemiringMarkoff_semiringPointMap {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) {x : Point R} (hx : IsSemiringMarkoff x) : IsSemiringMarkoff (semiringPointMap f x)

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

Map a Markoff solution along a homomorphism of commutative semirings.

Equations

• BGS.Markoff.SemiringMarkoffSurface.map f x = ⟨BGS.Markoff.semiringPointMap f ↑x, ⋯⟩

@[simp]

theorem BGS.Markoff.SemiringMarkoffSurface.map_coe {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) (x : SemiringMarkoffSurface R) : ↑(map f x) = semiringPointMap f ↑x

@[simp]

theorem BGS.Markoff.SemiringMarkoffSurface.map_x1 {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) (x : SemiringMarkoffSurface R) : (↑(map f x)).x1 = f (↑x).x1

@[simp]

theorem BGS.Markoff.SemiringMarkoffSurface.map_x2 {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) (x : SemiringMarkoffSurface R) : (↑(map f x)).x2 = f (↑x).x2

@[simp]

theorem BGS.Markoff.SemiringMarkoffSurface.map_x3 {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) (x : SemiringMarkoffSurface R) : (↑(map f x)).x3 = f (↑x).x3

@[simp]

theorem BGS.Markoff.SemiringMarkoffSurface.map_id {R : Type u} [CommSemiring R] (x : SemiringMarkoffSurface R) : map (RingHom.id R) x = x

@[simp]

theorem BGS.Markoff.SemiringMarkoffSurface.map_comp {R : Type u} {S : Type v} {T : Type w} [CommSemiring R] [CommSemiring S] [CommSemiring T] (g : S →+* T) (f : R →+* S) (x : SemiringMarkoffSurface R) : map (g.comp f) x = map g (map f x)

def BGS.Markoff.markoffFunctor : CategoryTheory.Functor CommSemiRingCat (Type u)

The covariant functor of Markoff solutions on commutative semirings.

Equations

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

def BGS.Markoff.markoffEquivSemiringMarkoffSurface (R : Type) [CommSemiring R] : Markoff.obj ↧R ≃ SemiringMarkoffSurface R

The public triple presentation of Markoff agrees with the structured presentation used internally by the dynamical development.

Equations

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

@[simp]

theorem BGS.Markoff.markoffEquivSemiringMarkoffSurface_map {R S : Type} [CommSemiring R] [CommSemiring S] (f : R →+* S) (x : Markoff.obj ↧R) : (markoffEquivSemiringMarkoffSurface S) ((CategoryTheory.ConcreteCategory.hom (Markoff.map (CommSemiRingCat.ofHom f))) x) = SemiringMarkoffSurface.map f ((markoffEquivSemiringMarkoffSurface R) x)

@[simp]

theorem BGS.Markoff.markoffFunctor_obj (R : CommSemiRingCat) : markoffFunctor.obj R = SemiringMarkoffSurface ↑R

theorem BGS.Markoff.markoffFunctor_map {R S : CommSemiRingCat} (f : R ⟶ S) (x : SemiringMarkoffSurface ↑R) : (CategoryTheory.ConcreteCategory.hom (markoffFunctor.map f)) x = SemiringMarkoffSurface.map (CommSemiRingCat.Hom.hom f) x

def BGS.Markoff.semiringSurfaceOrigin (R : Type u) [CommSemiring R] : SemiringMarkoffSurface R

The origin as a Markoff solution over a commutative semiring.

Equations

• BGS.Markoff.semiringSurfaceOrigin R = ⟨BGS.Markoff.origin, ⋯⟩

def BGS.Markoff.semiringSurfaceRoot (R : Type u) [CommSemiring R] : SemiringMarkoffSurface R

The distinguished positive Markoff solution (1, 1, 1).

Equations

• BGS.Markoff.semiringSurfaceRoot R = ⟨{ x1 := 1, x2 := 1, x3 := 1 }, ⋯⟩

@[simp]

theorem BGS.Markoff.SemiringMarkoffSurface.map_origin {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) : map f (semiringSurfaceOrigin R) = semiringSurfaceOrigin S

@[simp]

theorem BGS.Markoff.SemiringMarkoffSurface.map_root {R : Type u} {S : Type v} [CommSemiring R] [CommSemiring S] (f : R →+* S) : map f (semiringSurfaceRoot R) = semiringSurfaceRoot S

def BGS.Markoff.markoffReduction (p : ℕ) : SemiringMarkoffSurface ℕ → SemiringMarkoffSurface (ZMod p)

Coordinatewise reduction of natural-number Markoff solutions modulo p.

Equations

• BGS.Markoff.markoffReduction p = BGS.Markoff.SemiringMarkoffSurface.map (Nat.castRingHom (ZMod p))

theorem BGS.Markoff.strongApproximationAt_iff_markoffReduction_surjective (p : ℕ) : StrongApproximationAt p ↔ Function.Surjective (markoffReduction p)

The public functor formulation of strong approximation agrees with the structured reduction map used internally.

@[simp]

theorem BGS.Markoff.markoffReduction_eq_markoffFunctor_map (p : ℕ) (x : SemiringMarkoffSurface ℕ) : markoffReduction p x = (CategoryTheory.ConcreteCategory.hom (markoffFunctor.map (CommSemiRingCat.ofHom (Nat.castRingHom (ZMod p))))) x

theorem BGS.Markoff.markoffReduction_x1 (p : ℕ) (x : SemiringMarkoffSurface ℕ) : (↑(markoffReduction p x)).x1 = ↑(↑x).x1

theorem BGS.Markoff.markoffReduction_x2 (p : ℕ) (x : SemiringMarkoffSurface ℕ) : (↑(markoffReduction p x)).x2 = ↑(↑x).x2

theorem BGS.Markoff.markoffReduction_x3 (p : ℕ) (x : SemiringMarkoffSurface ℕ) : (↑(markoffReduction p x)).x3 = ↑(↑x).x3

theorem BGS.Markoff.markoffReduction_origin (p : ℕ) : markoffReduction p (semiringSurfaceOrigin ℕ) = semiringSurfaceOrigin (ZMod p)

theorem BGS.Markoff.markoffReduction_root (p : ℕ) : markoffReduction p (semiringSurfaceRoot ℕ) = semiringSurfaceRoot (ZMod p)

def BGS.Markoff.semiringMarkoffSurfaceEquiv (R : Type u) [CommRing R] : SemiringMarkoffSurface R ≃ MarkoffSurface R

Over a commutative ring, the equation-based semiring surface agrees with the existing zero-locus definition using markoffPolynomial.

Equations

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

@[simp]

theorem BGS.Markoff.semiringMarkoffSurfaceEquiv_apply_coe {R : Type u} [CommRing R] (x : SemiringMarkoffSurface R) : ↑((semiringMarkoffSurfaceEquiv R) x) = ↑x

@[simp]

theorem BGS.Markoff.semiringMarkoffSurfaceEquiv_symm_apply_coe {R : Type u} [CommRing R] (x : MarkoffSurface R) : ↑((semiringMarkoffSurfaceEquiv R).symm x) = ↑x

def BGS.Markoff.surfaceRoot (R : Type u) [CommRing R] : MarkoffSurface R

The distinguished solution (1, 1, 1) on the existing ring-level Markoff surface.

Equations

• BGS.Markoff.surfaceRoot R = ⟨{ x1 := 1, x2 := 1, x3 := 1 }, ⋯⟩

@[simp]

theorem BGS.Markoff.surfaceRoot_coe (R : Type u) [CommRing R] : ↑(surfaceRoot R) = { x1 := 1, x2 := 1, x3 := 1 }

@[simp]

theorem BGS.Markoff.semiringMarkoffSurfaceEquiv_origin (R : Type u) [CommRing R] : (semiringMarkoffSurfaceEquiv R) (semiringSurfaceOrigin R) = surfaceOrigin R

@[simp]

theorem BGS.Markoff.semiringMarkoffSurfaceEquiv_root (R : Type u) [CommRing R] : (semiringMarkoffSurfaceEquiv R) (semiringSurfaceRoot R) = surfaceRoot R