Absolute irreducibility of weighted odd-coprime split trace covers

The residue-block proof gives irreducibility first for the normalized coefficients (1, sigma). This file connects that result to the paper's actual weights (alpha, beta). Over the algebraic closure choose c with c ^ e = alpha; the reversible coordinate scaling y ↦ c * y carries the normalized cover with sigma = alpha * beta to alpha times the weighted cover. Thus no new irreducibility assumption is introduced at the normalization step.

noncomputable def BGS.Markoff.finTwoSecondVariableScaleEquiv {K : Type u_1} [Field K] (c : Kˣ) : MvPolynomial (Fin 2) K ≃ₐ[K] MvPolynomial (Fin 2) K

Scaling the second variable of a two-variable polynomial by a unit.

Equations

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

@[simp]

theorem BGS.Markoff.finTwoSecondVariableScaleEquiv_X_zero {K : Type u_1} [Field K] (c : Kˣ) : (finTwoSecondVariableScaleEquiv c) (MvPolynomial.X 0) = MvPolynomial.X 0

@[simp]

theorem BGS.Markoff.finTwoSecondVariableScaleEquiv_X_one {K : Type u_1} [Field K] (c : Kˣ) : (finTwoSecondVariableScaleEquiv c) (MvPolynomial.X 1) = MvPolynomial.C ↑c * MvPolynomial.X 1

@[simp]

theorem BGS.Markoff.finTwoSecondVariableScaleEquiv_C {K : Type u_1} [Field K] (c : Kˣ) (a : K) : (finTwoSecondVariableScaleEquiv c) (MvPolynomial.C a) = MvPolynomial.C a

theorem BGS.Markoff.finTwoSecondVariableScaleEquiv_normalizedCover {K : Type u_1} [Field K] (alpha beta : K) (e d : ℕ) (c : Kˣ) (hc : ↑c ^ e = alpha) : (finTwoSecondVariableScaleEquiv c) (splitTraceCoverPolynomial 1 (alpha * beta) d e) = MvPolynomial.C alpha * splitTraceCoverPolynomial alpha beta d e

Exact scaling identity between the normalized and weighted covers.

theorem BGS.Markoff.map_splitTraceCoverPolynomial {K : Type u_1} [Field K] {L : Type u_2} [Field L] (phi : K →+* L) (alpha beta : K) (d e : ℕ) : (MvPolynomial.map phi) (splitTraceCoverPolynomial alpha beta d e) = splitTraceCoverPolynomial (phi alpha) (phi beta) d e

The cleared split trace-cover polynomial commutes with scalar extension.

theorem BGS.Markoff.splitTraceCoverPolynomial_absolutelyIrreducible_of_positiveExponents {K : Type u_1} [Field K] (alpha beta : K) (halpha : alpha ≠ 0) (hbeta : beta ≠ 0) (hnondegenerate : alpha * beta ≠ 1) (e d : ℕ) (he : 0 < e) (hd : 0 < d) (heChar : ↑e ≠ 0) : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) (splitTraceCoverPolynomial alpha beta d e))

The paper's weighted split trace cover is absolutely irreducible for arbitrary positive covering exponents when the first-stage exponent is nonzero in the ground field. This is the characteristic condition satisfied by the endgame exponents dividing p - 1 or p + 1.

theorem BGS.Markoff.splitTraceCoverPolynomial_absolutelyIrreducible_of_coprime {K : Type u_1} [Field K] (alpha beta : K) (halpha : alpha ≠ 0) (hbeta : beta ≠ 0) (hnondegenerate : alpha * beta ≠ 1) (e d : ℕ) (he : 0 < e) (hd : 0 < d) (hde : d.Coprime e) : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) (splitTraceCoverPolynomial alpha beta d e))

The paper's weighted split trace cover is absolutely irreducible for nonzero weights with nondegenerate product and arbitrary positive coprime covering exponents. Passing to the algebraic closure supplies both the required square root of -1 and the root used to normalize the first weight.

theorem BGS.Markoff.splitTraceCoverPolynomial_absolutelyIrreducible_of_oddCoprime {K : Type u_1} [Field K] (alpha beta : K) (halpha : alpha ≠ 0) (hbeta : beta ≠ 0) (hnondegenerate : alpha * beta ≠ 1) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (hde : d.Coprime e) : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) (splitTraceCoverPolynomial alpha beta d e))

Backwards-compatible odd-coprime specialization of the positive-coprime theorem.