An exact criterion for the remaining split trace-cover division theorem

For sigma != 0, 1 and odd coprime cover degrees, the source-side syntactic division theorem is equivalent to two concrete algebraic facts: irreducibility of the cleared affine cover polynomial and injectivity of the comparison map after inverting the two coordinates. The reverse direction uses primeness to prove that localization has not killed an affine class. Thus the sigma = 1 counterexample cannot be hidden by moving to the Laurent model.

theorem BGS.Markoff.splitTraceCoverPolynomial_isRelPrime_coordinateProduct {K : Type u_1} [Field K] (sigma : K) (e d : ℕ) : sigma ≠ 0 → Odd e → Odd d → IsRelPrime (splitTraceCoverPolynomial 1 sigma d e) (MvPolynomial.X 0 * MvPolynomial.X 1)

The cleared affine cover polynomial has no coordinate-axis factor. This is the exact saturation fact needed to pass faithfully from the affine quotient to the Laurent open; it uses only sigma ≠ 0 and positivity of the odd cover degrees, not irreducibility.

theorem BGS.Markoff.splitTraceAffineToLaurent_injective {K : Type u_1} [Field K] (sigma : K) (e d : ℕ) : sigma ≠ 0 → Odd e → Odd d → Function.Injective ⇑(algebraMap (SplitTraceAffineCoordinateRing K sigma d e) (SplitTraceLaurentCoordinateRing K sigma d e))

Inverting the coordinate product does not kill any affine trace-cover class. This affine saturation theorem is independent of the unresolved irreducibility statement.

theorem BGS.Markoff.splitTraceAffineToKummerTop_injective_of_laurentInjective {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (hde : d.Coprime e) (hLaurent : Function.Injective ⇑(splitTraceLaurentToKummerTop sigma hsigma e d heOdd hdOdd hde)) : Function.Injective ⇑(splitTraceAffineToKummerTop sigma hsigma e d heOdd hdOdd hde)

Injectivity of the Laurent comparison already forces injectivity of the affine comparison: the coordinate-product localization is faithful by the explicit saturation theorem above.

theorem BGS.Markoff.splitTracePolynomialSyntacticNormalForm_division_of_laurentInjective {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (hde : d.Coprime e) (hLaurent : Function.Injective ⇑(splitTraceLaurentToKummerTop sigma hsigma e d heOdd hdOdd hde)) (p : MvPolynomial (Fin 2) K) (hnormal : splitTracePolynomialSyntacticNormalForm sigma hsigma e d heOdd hdOdd p = 0) : p ∈ Ideal.span {splitTraceCoverPolynomial 1 sigma d e}

Injectivity on the Laurent open implies the exact source-side syntactic division theorem.

theorem BGS.Markoff.splitTraceCoverPolynomial_irreducible_of_laurentInjective {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (hde : d.Coprime e) (hLaurent : Function.Injective ⇑(splitTraceLaurentToKummerTop sigma hsigma e d heOdd hdOdd hde)) : Irreducible (splitTraceCoverPolynomial 1 sigma d e)

Laurent-to-Kummer injectivity also forces irreducibility of the cleared affine cover. Indeed the affine quotient injects into the Kummer function field, hence is a domain.

theorem BGS.Markoff.splitTracePolynomialSyntacticNormalForm_division_iff_laurentInjective {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (hde : d.Coprime e) (hnondegenerate : sigma ≠ 1) : (∀ (p : MvPolynomial (Fin 2) K), splitTracePolynomialSyntacticNormalForm sigma hsigma e d heOdd hdOdd p = 0 → p ∈ Ideal.span {splitTraceCoverPolynomial 1 sigma d e}) ↔ Function.Injective ⇑(splitTraceLaurentToKummerTop sigma hsigma e d heOdd hdOdd hde)

Exact characterization of the remaining source-division wall. In the nondegenerate case, division by the cleared cover polynomial is equivalent to injectivity of the explicit Laurent-to-Kummer comparison; the affine-to-Laurent map has already been proved faithful.