Documentation

LeanPool.MarkoffModP.BGS.Markoff.Assembly.TransitivitySurjectivity

Punctured finite-field transitivity and reduction surjectivity #

The Markoff equation defines a functor on commutative semirings. This file identifies the finite-field transitivity statement used by the dynamical proof with the source-faithful arithmetic statement that reduction from natural-number Markoff solutions is surjective.

source
def BGS.Markoff.markoffReductionSurface (p : ℕ) :
SemiringMarkoffSurface ℕ → MarkoffSurface (ZMod p)

Reduction from natural-number solutions, viewed in the existing ring-level surface.

Equations
Instances For
    source
    @[simp]
    theorem BGS.Markoff.markoffReductionSurface_origin (p : ℕ) :
    markoffReductionSurface p (semiringSurfaceOrigin ℕ) = surfaceOrigin (ZMod p)
    source
    @[simp]
    theorem BGS.Markoff.markoffReductionSurface_root (p : ℕ) :
    markoffReductionSurface p (semiringSurfaceRoot ℕ) = surfaceRoot (ZMod p)
    source
    @[simp]
    theorem BGS.Markoff.markoffReductionSurface_natVieta1 (p : ℕ) (x : SemiringMarkoffSurface ℕ) :
    markoffReductionSurface p (natVieta1Surface x) = (vieta1SurfacePerm (ZMod p)) (markoffReductionSurface p x)
    source
    @[simp]
    theorem BGS.Markoff.markoffReductionSurface_natVieta2 (p : ℕ) (x : SemiringMarkoffSurface ℕ) :
    markoffReductionSurface p (natVieta2Surface x) = (vieta2SurfacePerm (ZMod p)) (markoffReductionSurface p x)
    source
    @[simp]
    theorem BGS.Markoff.markoffReductionSurface_natVieta3 (p : ℕ) (x : SemiringMarkoffSurface ℕ) :
    markoffReductionSurface p (natVieta3Surface x) = (vieta3SurfacePerm (ZMod p)) (markoffReductionSurface p x)
    source
    @[simp]
    theorem BGS.Markoff.markoffReductionSurface_natSwap12 (p : ℕ) (x : SemiringMarkoffSurface ℕ) :
    markoffReductionSurface p (natSwap12Surface x) = (swap12SurfacePerm (ZMod p)) (markoffReductionSurface p x)
    source
    @[simp]
    theorem BGS.Markoff.markoffReductionSurface_natSwap23 (p : ℕ) (x : SemiringMarkoffSurface ℕ) :
    markoffReductionSurface p (natSwap23Surface x) = (swap23SurfacePerm (ZMod p)) (markoffReductionSurface p x)
    source
    theorem BGS.Markoff.exists_naturalGamma_lift (p : ℕ) (g : ↥(Gamma (ZMod p))) :
    ∃ (h : ↥NaturalGamma), ∀ (x : SemiringMarkoffSurface ℕ), markoffReductionSurface p (h • x) = g • markoffReductionSurface p x

    Every word in the finite-field Markoff group has a word in the natural Markoff group whose action commutes with reduction.

    source
    theorem BGS.Markoff.exists_gamma_reduction_of_naturalGamma (p : ℕ) (h : ↥NaturalGamma) :
    ∃ (g : ↥(Gamma (ZMod p))), ∀ (x : SemiringMarkoffSurface ℕ), markoffReductionSurface p (h • x) = g • markoffReductionSurface p x

    Every word in the natural Markoff group reduces to a word in the finite-field Markoff group.

    source
    theorem BGS.Markoff.sameComponent_markoffReductionSurface_of_sameNatMarkoffComponent (p : ℕ) {x y : SemiringMarkoffSurface ℕ} (hxy : SameNatMarkoffComponent x y) :
    SameComponent (markoffReductionSurface p x) (markoffReductionSurface p y)

    Natural Markoff connectivity descends to finite-field Markoff connectivity.

    source
    @[simp]
    theorem BGS.Markoff.surfaceRoot_ne_surfaceOrigin (R : Type u_1) [CommRing R] [Nontrivial R] :
    surfaceRoot R ≠ surfaceOrigin R
    source
    theorem BGS.Markoff.markoffReduction_surjective_of_puncturedMarkoffTransitiveAt (p : ℕ) (hp : Nat.Prime p) (htransitive : PuncturedMarkoffTransitiveAt p) :
    Function.Surjective (markoffReduction p)

    Finite-field transitivity implies surjectivity of reduction from natural-number solutions.

    source
    theorem BGS.Markoff.puncturedMarkoffTransitiveAt_of_markoffReduction_surjective (p : ℕ) (hp : Nat.Prime p) (hsurjective : Function.Surjective (markoffReduction p)) :
    PuncturedMarkoffTransitiveAt p

    Surjectivity of natural-number reduction implies finite-field transitivity. The classical connectivity of nonzero natural Markoff solutions is the essential input in this direction.

    source
    theorem BGS.Markoff.puncturedMarkoffTransitiveAt_iff_markoffReduction_surjective (p : ℕ) (hp : Nat.Prime p) :
    PuncturedMarkoffTransitiveAt p ↔ Function.Surjective (markoffReduction p)

    The source-faithful reduction statement is equivalent to the finite-field transitivity statement used by the BGS dynamical proof.

    source
    theorem BGS.Markoff.puncturedMarkoffTransitiveAt_iff_strongApproximationAt (p : ℕ) (hp : Nat.Prime p) :
    PuncturedMarkoffTransitiveAt p ↔ StrongApproximationAt p

    For prime moduli, punctured finite-field transitivity is equivalent to strong approximation. Natural Markoff connectivity is the essential input from right to left.