Syntactic monomial reduction for the split trace cover

This file starts the source-side quotient reduction. A monomial xi^i * eta^j is reduced by Euclidean division of i by d and j by e. Its rectangular basis index is (j % e, i % d), and its coefficient in the quadratic base function field is u^(i / d) * v^(i / d + j / e).

theorem BGS.Markoff.pow_eq_pow_div_mul_pow_mod {M : Type u_1} [Monoid M] (x : M) (n q : ℕ) : x ^ n = (x ^ q) ^ (n / q) * x ^ (n % q)

theorem BGS.Markoff.splitTraceEtaKummerPolynomial_natDegree {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e : ℕ) : (splitTraceEtaKummerPolynomial sigma e).natDegree = e

theorem BGS.Markoff.splitTraceXiKummerPolynomial_natDegree {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) : (splitTraceXiKummerPolynomial sigma e d).natDegree = d

def BGS.Markoff.splitTraceMonomialNormalIndex {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (i j : ℕ) : Fin (splitTraceEtaKummerPolynomial sigma e).natDegree × Fin (splitTraceXiKummerPolynomial sigma e d).natDegree

Residual rectangular index of the monomial xi^i * eta^j.

Equations

• BGS.Markoff.splitTraceMonomialNormalIndex sigma hsigma e d heOdd hdOdd i j = (⟨j % e, ⋯⟩, ⟨i % d, ⋯⟩)

@[simp]

theorem BGS.Markoff.splitTraceMonomialNormalIndex_fst_val {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (i j : ℕ) : ↑(splitTraceMonomialNormalIndex sigma hsigma e d heOdd hdOdd i j).1 = j % e

@[simp]

theorem BGS.Markoff.splitTraceMonomialNormalIndex_snd_val {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (i j : ℕ) : ↑(splitTraceMonomialNormalIndex sigma hsigma e d heOdd hdOdd i j).2 = i % d

noncomputable def BGS.Markoff.splitTraceMonomialNormalCoefficient {K : Type u_1} [Field K] (sigma : K) (e d i j : ℕ) : SplitTraceBaseFunctionField K sigma

Base-function-field coefficient extracted from xi^i * eta^j.

Equations

• BGS.Markoff.splitTraceMonomialNormalCoefficient sigma e d i j = BGS.Markoff.splitTraceBaseU sigma ^ (i / d) * BGS.Markoff.splitTraceBaseV sigma ^ (i / d + j / e)

noncomputable def BGS.Markoff.splitTraceExplicitNormalFormEvaluation {K : Type u_1} [Field K] (sigma : K) (e d : ℕ) (c : Fin (splitTraceEtaKummerPolynomial sigma e).natDegree × Fin (splitTraceXiKummerPolynomial sigma e d).natDegree →₀ AdjoinRoot (splitTraceBaseKummerPolynomial sigma)) : SplitTraceXiFunctionField K sigma e d

Evaluate a rectangular coefficient vector by the explicit normal monomial family.

Equations

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

noncomputable def BGS.Markoff.splitTracePolynomialSyntacticNormalForm {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (p : MvPolynomial (Fin 2) K) : Fin (splitTraceEtaKummerPolynomial sigma e).natDegree × Fin (splitTraceXiKummerPolynomial sigma e d).natDegree →₀ AdjoinRoot (splitTraceBaseKummerPolynomial sigma)

Explicit source-side rectangular coefficients of a polynomial in the two affine coordinates. Each source monomial is reduced independently by quotient and remainder of its two exponents.

Equations

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

@[simp]

theorem BGS.Markoff.splitTracePolynomialSyntacticNormalForm_zero {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) : splitTracePolynomialSyntacticNormalForm sigma hsigma e d heOdd hdOdd 0 = 0

theorem BGS.Markoff.splitTracePolynomialSyntacticNormalForm_add {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (p q : MvPolynomial (Fin 2) K) : splitTracePolynomialSyntacticNormalForm sigma hsigma e d heOdd hdOdd (p + q) = splitTracePolynomialSyntacticNormalForm sigma hsigma e d heOdd hdOdd p + splitTracePolynomialSyntacticNormalForm sigma hsigma e d heOdd hdOdd q

@[simp]

theorem BGS.Markoff.splitTracePolynomialSyntacticNormalForm_monomial {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (ex : Fin 2 →₀ ℕ) (c : K) : splitTracePolynomialSyntacticNormalForm sigma hsigma e d heOdd hdOdd ((MvPolynomial.monomial ex) c) = Finsupp.single (splitTraceMonomialNormalIndex sigma hsigma e d heOdd hdOdd (ex 0) (ex 1)) ((algebraMap K (AdjoinRoot (splitTraceBaseKummerPolynomial sigma))) c * splitTraceMonomialNormalCoefficient sigma e d (ex 0) (ex 1))

theorem BGS.Markoff.splitTraceEtaRootInXiField_pow {K : Type u_1} [Field K] (sigma : K) (e d : ℕ) : splitTraceEtaRootInXiField sigma e d ^ e = splitTraceBaseElementInXiField sigma e d (splitTraceBaseV sigma)

theorem BGS.Markoff.splitTraceKummer_monomial_reduction {K : Type u_1} [Field K] (sigma : K) (e d i j : ℕ) : splitTraceXiRoot sigma e d ^ i * splitTraceEtaRootInXiField sigma e d ^ j = splitTraceBaseElementInXiField sigma e d (splitTraceMonomialNormalCoefficient sigma e d i j) * (splitTraceEtaRootInXiField sigma e d ^ (j % e) * splitTraceXiRoot sigma e d ^ (i % d))

Explicit source-side monomial reduction in the Kummer top algebra.

theorem BGS.Markoff.splitTraceExplicitNormalFormEvaluation_single_monomial {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (i j : ℕ) : splitTraceExplicitNormalFormEvaluation sigma e d (Finsupp.single (splitTraceMonomialNormalIndex sigma hsigma e d heOdd hdOdd i j) (splitTraceMonomialNormalCoefficient sigma e d i j)) = splitTraceXiRoot sigma e d ^ i * splitTraceEtaRootInXiField sigma e d ^ j

The explicit normal-form evaluation of the singleton produced from a source monomial is the original monomial in the Kummer top algebra.

theorem BGS.Markoff.splitTraceExplicitNormalFormEvaluation_single_scaled_monomial {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (c : K) (i j : ℕ) : splitTraceExplicitNormalFormEvaluation sigma e d (Finsupp.single (splitTraceMonomialNormalIndex sigma hsigma e d heOdd hdOdd i j) ((algebraMap K (AdjoinRoot (splitTraceBaseKummerPolynomial sigma))) c * splitTraceMonomialNormalCoefficient sigma e d i j)) = (algebraMap K (SplitTraceXiFunctionField K sigma e d)) c * (splitTraceXiRoot sigma e d ^ i * splitTraceEtaRootInXiField sigma e d ^ j)

Including the source coefficient, explicit evaluation of the syntactic singleton agrees with evaluation of the original source monomial.

theorem BGS.Markoff.splitTracePolynomialToKummerTop_monomial {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (hde : d.Coprime e) (ex : Fin 2 →₀ ℕ) (c : K) : (splitTracePolynomialToKummerTop sigma hsigma e d heOdd hdOdd hde) ((MvPolynomial.monomial ex) c) = (algebraMap K (SplitTraceXiFunctionField K sigma e d)) c * (splitTraceXiRoot sigma e d ^ ex 0 * splitTraceEtaRootInXiField sigma e d ^ ex 1)

theorem BGS.Markoff.splitTracePolynomialSyntacticNormalForm_evaluation {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (hde : d.Coprime e) (p : MvPolynomial (Fin 2) K) : splitTraceExplicitNormalFormEvaluation sigma e d (splitTracePolynomialSyntacticNormalForm sigma hsigma e d heOdd hdOdd p) = (splitTracePolynomialToKummerTop sigma hsigma e d heOdd hdOdd hde) p

Evaluation of the explicit syntactic coefficient vector agrees with direct polynomial evaluation at the two Kummer roots.

theorem BGS.Markoff.splitTraceExplicitNormalFormEvaluation_eq_zero_iff {K : Type u_1} [Field K] (sigma : K) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (hde : d.Coprime e) (c : Fin (splitTraceEtaKummerPolynomial sigma e).natDegree × Fin (splitTraceXiKummerPolynomial sigma e d).natDegree →₀ AdjoinRoot (splitTraceBaseKummerPolynomial sigma)) : splitTraceExplicitNormalFormEvaluation sigma e d c = 0 ↔ c = 0

The committed normal-monomial independence theorem makes explicit normal-form evaluation injective.

theorem BGS.Markoff.splitTracePolynomialSyntacticNormalForm_eq_zero_iff {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (hde : d.Coprime e) (p : MvPolynomial (Fin 2) K) : splitTracePolynomialSyntacticNormalForm sigma hsigma e d heOdd hdOdd p = 0 ↔ (splitTracePolynomialToKummerTop sigma hsigma e d heOdd hdOdd hde) p = 0

A source polynomial has zero syntactic normal form exactly when its evaluation at the Kummer roots vanishes. The remaining injectivity wall is to identify this explicit zero condition with membership in the principal ideal generated by the trace-cover polynomial.

theorem BGS.Markoff.splitTraceAffineToKummerTop_injective_of_syntacticNormalForm_division {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) (hdivision : ∀ (p : MvPolynomial (Fin 2) K), splitTracePolynomialSyntacticNormalForm sigma hsigma e d heOdd hdOdd p = 0 → p ∈ Ideal.span {splitTraceCoverPolynomial 1 sigma d e}) : Function.Injective ⇑(splitTraceAffineToKummerTop sigma hsigma e d heOdd hdOdd hde)

For a nondegenerate trace parameter, the remaining source-side division theorem is sufficient for injectivity of the affine comparison map. The division hypothesis is deliberately an ordinary explicit proposition: it is not an assumed declaration, typeclass, or structure field. The condition sigma ≠ 1 is essential: at sigma = 1 the cleared cover factors and the Kummer tower selects only one component; see TraceCurveSyntacticDivisionObstruction.