Irreducibility of positive coprime split trace covers

This module removes the oddness restriction from the split-cover proof. A Capelli-style binomial criterion constructs the Kummer tower for arbitrary positive coprime exponents over a field containing a square root of -1. A parity-free residue decomposition then reconnects the tower to the actual affine cover polynomial and proves its principal ideal prime.

The coprimality restriction is still real in this proof: common prime divisors require a separate Kummer-class independence argument and are not hidden here.

theorem BGS.Markoff.exists_primePowerRootOfNegOne {K : Type u_1} [Field K] (i : K) (hi : i ^ 2 = -1) (q : ℕ) (hq : Nat.Prime q) : ∃ (c : K), c ^ q = -1

theorem BGS.Markoff.X_pow_sub_C_irreducible_of_sqrt_neg_one {K : Type u_1} [Field K] (i : K) (hi : i ^ 2 = -1) {n : ℕ} (hn : n ≠ 0) {a : K} (ha : ∀ (q : ℕ), Nat.Prime q → q ∣ n → ∀ (b : K), b ^ q ≠ a) : Irreducible (Polynomial.X ^ n - Polynomial.C a)

Over a field in which -1 is a square, the usual prime-radicand criterion for X^n-a is valid also for even n.

theorem BGS.Markoff.splitTraceEtaKummerPolynomial_irreducible_of_sqrt_neg_one {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (i : K) (hi : i ^ 2 = -1) (e : ℕ) (he : 0 < e) : Irreducible (splitTraceEtaKummerPolynomial sigma e)

The first trace-curve Kummer polynomial is irreducible for every positive exponent once the constant field contains a square root of -1.

theorem BGS.Markoff.splitTraceEtaFunctionField_finrank_of_sqrt_neg_one {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (i : K) (hi : i ^ 2 = -1) (e : ℕ) (he : 0 < e) : Module.finrank (SplitTraceBaseFunctionField K sigma) (SplitTraceEtaFunctionField K sigma e) = e

theorem BGS.Markoff.splitTraceXiRadicand_not_primePower_of_sqrt_neg_one {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (i : K) (hi : i ^ 2 = -1) (e : ℕ) (he : 0 < e) (q : ℕ) (hq : Nat.Prime q) (hqe : ¬q ∣ e) (z : SplitTraceEtaFunctionField K sigma e) : z ^ q ≠ splitTraceXiRadicand sigma e

The norm-degree obstruction for the second radicand does not depend on parity. It applies to every prime not dividing the first exponent.

theorem BGS.Markoff.splitTraceXiKummerPolynomial_irreducible_of_sqrt_neg_one_coprime {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (i : K) (hi : i ^ 2 = -1) (e d : ℕ) (he : 0 < e) (hd : 0 < d) (hde : d.Coprime e) : Irreducible (splitTraceXiKummerPolynomial sigma e d)

For arbitrary positive coprime exponents, including even exponents, the second Kummer polynomial is irreducible once the constant field contains a square root of -1.

def BGS.Markoff.generalSplitTraceMonomialNormalIndex {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (i : K) (hi : i ^ 2 = -1) (e d : ℕ) (he : 0 < e) (hd : 0 < d) (a b : ℕ) : Fin (splitTraceEtaKummerPolynomial sigma e).natDegree × Fin (splitTraceXiKummerPolynomial sigma e d).natDegree

Rectangular residue index for arbitrary positive coprime exponents.

Equations

• BGS.Markoff.generalSplitTraceMonomialNormalIndex sigma hsigma i hi e d he hd a b = (⟨b % e, ⋯⟩, ⟨a % d, ⋯⟩)

@[simp]

theorem BGS.Markoff.generalSplitTraceMonomialNormalIndex_fst_val {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (i : K) (hi : i ^ 2 = -1) (e d : ℕ) (he : 0 < e) (hd : 0 < d) (a b : ℕ) : ↑(generalSplitTraceMonomialNormalIndex sigma hsigma i hi e d he hd a b).1 = b % e

@[simp]

theorem BGS.Markoff.generalSplitTraceMonomialNormalIndex_snd_val {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (i : K) (hi : i ^ 2 = -1) (e d : ℕ) (he : 0 < e) (hd : 0 < d) (a b : ℕ) : ↑(generalSplitTraceMonomialNormalIndex sigma hsigma i hi e d he hd a b).2 = a % d

noncomputable def BGS.Markoff.generalSplitTracePolynomialSyntacticNormalForm {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (i : K) (hi : i ^ 2 = -1) (e d : ℕ) (he : 0 < e) (hd : 0 < d) (p : MvPolynomial (Fin 2) K) : Fin (splitTraceEtaKummerPolynomial sigma e).natDegree × Fin (splitTraceXiKummerPolynomial sigma e d).natDegree →₀ SplitTraceBaseFunctionField K sigma

Syntactic rectangular coefficients without parity assumptions.

Equations

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

@[simp]

theorem BGS.Markoff.generalSplitTracePolynomialSyntacticNormalForm_zero {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (i : K) (hi : i ^ 2 = -1) (e d : ℕ) (he : 0 < e) (hd : 0 < d) : generalSplitTracePolynomialSyntacticNormalForm sigma hsigma i hi e d he hd 0 = 0

theorem BGS.Markoff.generalSplitTracePolynomialSyntacticNormalForm_add {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (i : K) (hi : i ^ 2 = -1) (e d : ℕ) (he : 0 < e) (hd : 0 < d) (p q : MvPolynomial (Fin 2) K) : generalSplitTracePolynomialSyntacticNormalForm sigma hsigma i hi e d he hd (p + q) = generalSplitTracePolynomialSyntacticNormalForm sigma hsigma i hi e d he hd p + generalSplitTracePolynomialSyntacticNormalForm sigma hsigma i hi e d he hd q

@[simp]

theorem BGS.Markoff.generalSplitTracePolynomialSyntacticNormalForm_monomial {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (i : K) (hi : i ^ 2 = -1) (e d : ℕ) (he : 0 < e) (hd : 0 < d) (ex : Fin 2 →₀ ℕ) (c : K) : generalSplitTracePolynomialSyntacticNormalForm sigma hsigma i hi e d he hd ((MvPolynomial.monomial ex) c) = Finsupp.single (generalSplitTraceMonomialNormalIndex sigma hsigma i hi e d he hd (ex 0) (ex 1)) ((algebraMap K (SplitTraceBaseFunctionField K sigma)) c * splitTraceMonomialNormalCoefficient sigma e d (ex 0) (ex 1))

noncomputable def BGS.Markoff.generalSplitTracePolynomialToKummerTop {K : Type u_1} [Field K] (sigma : K) (e d : ℕ) : MvPolynomial (Fin 2) K →ₐ[K] SplitTraceXiFunctionField K sigma e d

Evaluation at the two roots in the general positive-coprime Kummer tower.

Equations

• BGS.Markoff.generalSplitTracePolynomialToKummerTop sigma e d = MvPolynomial.aeval ![BGS.Markoff.splitTraceXiRoot sigma e d, BGS.Markoff.splitTraceEtaRootInXiField sigma e d]

@[simp]

theorem BGS.Markoff.generalSplitTracePolynomialToKummerTop_monomial {K : Type u_1} [Field K] (sigma : K) (e d : ℕ) (ex : Fin 2 →₀ ℕ) (c : K) : (generalSplitTracePolynomialToKummerTop sigma e d) ((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.generalSplitTracePolynomialSyntacticNormalForm_evaluation {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (i : K) (hi : i ^ 2 = -1) (e d : ℕ) (he : 0 < e) (hd : 0 < d) (p : MvPolynomial (Fin 2) K) : splitTraceExplicitNormalFormEvaluation sigma e d (generalSplitTracePolynomialSyntacticNormalForm sigma hsigma i hi e d he hd p) = (generalSplitTracePolynomialToKummerTop sigma e d) p

theorem BGS.Markoff.generalSplitTracePolynomialSyntacticNormalForm_eq_zero_iff {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (i : K) (hi : i ^ 2 = -1) (e d : ℕ) (he : 0 < e) (hd : 0 < d) (p : MvPolynomial (Fin 2) K) : generalSplitTracePolynomialSyntacticNormalForm sigma hsigma i hi e d he hd p = 0 ↔ (generalSplitTracePolynomialToKummerTop sigma e d) p = 0

noncomputable def BGS.Markoff.generalSplitTracePolynomialResidueBlocks {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (i : K) (hi : i ^ 2 = -1) (e d : ℕ) (he : 0 < e) (hd : 0 < d) (p : MvPolynomial (Fin 2) K) : Fin (splitTraceEtaKummerPolynomial sigma e).natDegree × Fin (splitTraceXiKummerPolynomial sigma e d).natDegree →₀ MvPolynomial (Fin 2) K

Residue-block coefficient polynomials for arbitrary positive exponents.

Equations

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

@[simp]

theorem BGS.Markoff.generalSplitTracePolynomialResidueBlocks_zero {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (i : K) (hi : i ^ 2 = -1) (e d : ℕ) (he : 0 < e) (hd : 0 < d) : generalSplitTracePolynomialResidueBlocks sigma hsigma i hi e d he hd 0 = 0

theorem BGS.Markoff.generalSplitTracePolynomialResidueBlocks_add {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (i : K) (hi : i ^ 2 = -1) (e d : ℕ) (he : 0 < e) (hd : 0 < d) (p q : MvPolynomial (Fin 2) K) : generalSplitTracePolynomialResidueBlocks sigma hsigma i hi e d he hd (p + q) = generalSplitTracePolynomialResidueBlocks sigma hsigma i hi e d he hd p + generalSplitTracePolynomialResidueBlocks sigma hsigma i hi e d he hd q

@[simp]

theorem BGS.Markoff.generalSplitTracePolynomialResidueBlocks_monomial {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (i : K) (hi : i ^ 2 = -1) (e d : ℕ) (he : 0 < e) (hd : 0 < d) (ex : Fin 2 →₀ ℕ) (c : K) : generalSplitTracePolynomialResidueBlocks sigma hsigma i hi e d he hd ((MvPolynomial.monomial ex) c) = Finsupp.single (generalSplitTraceMonomialNormalIndex sigma hsigma i hi e d he hd (ex 0) (ex 1)) ((MvPolynomial.monomial (finTwoExponent (ex 0 / d) (ex 1 / e))) c)

theorem BGS.Markoff.splitTraceRecomposeGeneralResidueBlocks_single_monomial {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (i : K) (hi : i ^ 2 = -1) (e d : ℕ) (he : 0 < e) (hd : 0 < d) (a b : ℕ) (c : K) : splitTraceRecomposeResidueBlocks sigma e d (Finsupp.single (generalSplitTraceMonomialNormalIndex sigma hsigma i hi e d he hd a b) ((MvPolynomial.monomial (finTwoExponent (a / d) (b / e))) c)) = (MvPolynomial.monomial (finTwoExponent a b)) c

theorem BGS.Markoff.splitTraceRecomposeGeneralResidueBlocks_polynomial {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (i : K) (hi : i ^ 2 = -1) (e d : ℕ) (he : 0 < e) (hd : 0 < d) (p : MvPolynomial (Fin 2) K) : splitTraceRecomposeResidueBlocks sigma e d (generalSplitTracePolynomialResidueBlocks sigma hsigma i hi e d he hd p) = p

Exact reconstruction from the general residue blocks.

theorem BGS.Markoff.splitTraceBaseResidueEvaluation_generalResidueBlock {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (i : K) (hi : i ^ 2 = -1) (e d : ℕ) (he : 0 < e) (hd : 0 < d) (p : MvPolynomial (Fin 2) K) (ji : Fin (splitTraceEtaKummerPolynomial sigma e).natDegree × Fin (splitTraceXiKummerPolynomial sigma e d).natDegree) : (splitTraceBaseResidueEvaluation sigma) ((generalSplitTracePolynomialResidueBlocks sigma hsigma i hi e d he hd p) ji) = (generalSplitTracePolynomialSyntacticNormalForm sigma hsigma i hi e d he hd p) ji

Each general syntactic coefficient is the base-curve evaluation of its residue block.

theorem BGS.Markoff.generalSplitTracePolynomialSyntacticNormalForm_division {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (i : K) (hi : i ^ 2 = -1) (e d : ℕ) (he : 0 < e) (hd : 0 < d) (hnondegenerate : sigma ≠ 1) (p : MvPolynomial (Fin 2) K) (hnormal : generalSplitTracePolynomialSyntacticNormalForm sigma hsigma i hi e d he hd p = 0) : p ∈ Ideal.span {splitTraceCoverPolynomial 1 sigma d e}

Source division for every positive coprime cover once the even Kummer criterion applies.

theorem BGS.Markoff.generalSplitTraceKummerTower_cover_maps_to_zero {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (i : K) (hi : i ^ 2 = -1) (e d : ℕ) (he : 0 < e) (hd : 0 < d) (hde : d.Coprime e) : (generalSplitTracePolynomialToKummerTop sigma e d) (splitTraceCoverPolynomial 1 sigma d e) = 0

The roots of the positive-coprime tower satisfy the cleared affine cover equation.

theorem BGS.Markoff.splitTraceCoverPolynomial_irreducible_of_sqrt_neg_one_coprime {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (i : K) (hi : i ^ 2 = -1) (e d : ℕ) (he : 0 < e) (hd : 0 < d) (hde : d.Coprime e) (hnondegenerate : sigma ≠ 1) : Irreducible (splitTraceCoverPolynomial 1 sigma d e)

The normalized split trace-cover polynomial is irreducible for all positive coprime exponents, including even exponents, over a field containing a square root of -1.