Absolute irreducibility of the weighted middle-game trace curve

This module proves the absolute-irreducibility hypothesis exposed by MiddleGameCorvajaZannierGeometry. The proof uses the published torus change of variables honestly: the weighted left parameter is first scaled by alpha, and then the invertible birational coordinate u = x / y is used after passage to the coefficient fraction field. The resulting polynomial is the Eisenstein polynomial already proved irreducible in TraceCurveGeometry.

noncomputable def BGS.Markoff.polynomialVariableScaleEquiv {R : Type u_1} [CommRing R] (c : Rˣ) : Polynomial R ≃ₐ[R] Polynomial R

Scaling the variable of a polynomial by a unit is an algebra automorphism.

Equations

• BGS.Markoff.polynomialVariableScaleEquiv c = AlgEquiv.ofAlgHom (Polynomial.aeval (Polynomial.C ↑c * Polynomial.X)) (Polynomial.aeval (Polynomial.C ↑c⁻¹ * Polynomial.X)) ⋯ ⋯

@[simp]

theorem BGS.Markoff.polynomialVariableScaleEquiv_X {R : Type u_1} [CommRing R] (c : Rˣ) : (polynomialVariableScaleEquiv c) Polynomial.X = Polynomial.C ↑c * Polynomial.X

@[simp]

theorem BGS.Markoff.polynomialVariableScaleEquiv_C {R : Type u_1} [CommRing R] (c : Rˣ) (r : R) : (polynomialVariableScaleEquiv c) (Polynomial.C r) = Polynomial.C r

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

View a two-variable polynomial as a polynomial in variable 0, whose coefficients are ordinary polynomials in variable 1.

Equations

• BGS.Markoff.finTwoToIteratedPolynomial = (MvPolynomial.finSuccEquiv K 1).trans (Polynomial.mapAlgEquiv (MvPolynomial.uniqueAlgEquiv K (Fin 1)))

@[simp]

theorem BGS.Markoff.finTwoToIteratedPolynomial_X_zero {K : Type u_1} [Field K] : finTwoToIteratedPolynomial (MvPolynomial.X 0) = Polynomial.X

@[simp]

theorem BGS.Markoff.finTwoToIteratedPolynomial_X_one {K : Type u_1} [Field K] : finTwoToIteratedPolynomial (MvPolynomial.X 1) = Polynomial.C Polynomial.X

@[simp]

theorem BGS.Markoff.finTwoToIteratedPolynomial_C {K : Type u_1} [Field K] (r : K) : finTwoToIteratedPolynomial (MvPolynomial.C r) = Polynomial.C (Polynomial.C r)

noncomputable def BGS.Markoff.weightedTraceIteratedPolynomial {K : Type u_1} [Field K] (alpha beta : K) : Polynomial (Polynomial K)

The weighted trace curve in the iterated-polynomial presentation.

Equations

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

theorem BGS.Markoff.finTwoToIteratedPolynomial_weightedTraceTorusClosurePolynomial {K : Type u_1} [Field K] (alpha beta : K) (hbeta : beta ≠ 0) : finTwoToIteratedPolynomial (weightedTraceTorusClosurePolynomial alpha beta) = weightedTraceIteratedPolynomial alpha beta

noncomputable def BGS.Markoff.weightedTraceScaledBirationalPolynomial {K : Type u_1} [Field K] (alpha : Kˣ) (beta : K) : Polynomial (Polynomial K)

The swapped Eisenstein polynomial after the invertible scaling y ↦ alpha * y. It is a polynomial in the birational coordinate u, with coefficients in K[y].

Equations

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

theorem BGS.Markoff.weightedTraceScaledBirationalPolynomial_eq_map_swap {K : Type u_1} [Field K] (alpha : Kˣ) (beta : K) : weightedTraceScaledBirationalPolynomial alpha beta = (Polynomial.mapAlgEquiv (polynomialVariableScaleEquiv alpha)) (Polynomial.Bivariate.swap (normalizedSplitTraceBirationalPolynomial (↑alpha * beta)))

theorem BGS.Markoff.weightedTraceScaledBirationalPolynomial_irreducible {K : Type u_1} [Field K] (alpha : Kˣ) (beta : K) (hbeta : beta ≠ 0) (hnondegenerate : ↑alpha * beta ≠ 1) : Irreducible (weightedTraceScaledBirationalPolynomial alpha beta)

The scaled-and-swapped birational polynomial remains irreducible.

theorem BGS.Markoff.weightedTraceScaledBirationalPolynomial_irreducible_fractionMap {K : Type u_1} [Field K] (alpha : Kˣ) (beta : K) (hbeta : beta ≠ 0) (hnondegenerate : ↑alpha * beta ≠ 1) : Irreducible (Polynomial.map (algebraMap (Polynomial K) (FractionRing (Polynomial K))) (weightedTraceScaledBirationalPolynomial alpha beta))

The scaled birational polynomial stays irreducible over the coefficient fraction field.

noncomputable def BGS.Markoff.weightedTraceFractionScaleUnit {K : Type u_1} [Field K] (alpha : Kˣ) : (FractionRing (Polynomial K))ˣ

The unit alpha * y in the rational function field K(y).

Equations

• BGS.Markoff.weightedTraceFractionScaleUnit alpha = Units.mk0 ((algebraMap (Polynomial K) (FractionRing (Polynomial K))) (Polynomial.C ↑alpha * Polynomial.X)) ⋯

@[simp]

theorem BGS.Markoff.weightedTraceFractionScaleUnit_val {K : Type u_1} [Field K] (alpha : Kˣ) : ↑(weightedTraceFractionScaleUnit alpha) = (algebraMap (Polynomial K) (FractionRing (Polynomial K))) (Polynomial.C ↑alpha * Polynomial.X)

theorem BGS.Markoff.polynomialVariableScaleEquiv_map_weightedTraceIteratedPolynomial {K : Type u_1} [Field K] (alpha : Kˣ) (beta : K) : (polynomialVariableScaleEquiv (weightedTraceFractionScaleUnit alpha)) (Polynomial.map (algebraMap (Polynomial K) (FractionRing (Polynomial K))) (weightedTraceIteratedPolynomial (↑alpha) beta)) = Polynomial.C ((algebraMap (Polynomial K) (FractionRing (Polynomial K))) Polynomial.X) * Polynomial.map (algebraMap (Polynomial K) (FractionRing (Polynomial K))) (weightedTraceScaledBirationalPolynomial alpha beta)

After passing to K(y) and scaling x by the invertible element alpha * y, the weighted trace polynomial is y times the scaled Eisenstein polynomial.

theorem BGS.Markoff.weightedTraceIteratedPolynomial_irreducible {K : Type u_1} [Field K] (alpha beta : K) (halpha : alpha ≠ 0) (hbeta : beta ≠ 0) (hnondegenerate : alpha * beta ≠ 1) : Irreducible (weightedTraceIteratedPolynomial alpha beta)

The actual weighted trace polynomial is irreducible in the iterated presentation.

theorem BGS.Markoff.map_weightedTraceTorusClosurePolynomial_of_beta_ne_zero {K : Type u_1} [Field K] {L : Type u_2} [Field L] (phi : K →+* L) (alpha beta : K) (hbeta : beta ≠ 0) : (MvPolynomial.map phi) (weightedTraceTorusClosurePolynomial alpha beta) = weightedTraceTorusClosurePolynomial (phi alpha) (phi beta)

The reduced torus closure commutes with injective scalar extension in the nonzero beta branch used by the (2,2) middle-game curve.

theorem BGS.Markoff.weightedTraceTorusClosurePolynomial_irreducible {K : Type u_1} [Field K] (alpha beta : K) (halpha : alpha ≠ 0) (hbeta : beta ≠ 0) (hnondegenerate : alpha * beta ≠ 1) : Irreducible (weightedTraceTorusClosurePolynomial alpha beta)

Irreducibility over the ground field, obtained from the iterated-polynomial proof by the explicit two-variable polynomial equivalence.

theorem BGS.Markoff.weightedTraceCurve_absolutelyIrreducible {K : Type u_1} [Field K] (alpha beta : K) (halpha : alpha ≠ 0) (hbeta : beta ≠ 0) (hnondegenerate : alpha * beta ≠ 1) : WeightedTraceCurveAbsolutelyIrreducible alpha beta

The actual weighted trace curve is absolutely irreducible when both weights are nonzero and their product is not one. Every coordinate change used in the proof is an explicit algebra equivalence or a Gauss-lemma passage to a fraction field.