Injectivity of the Laurent comparison from cover irreducibility

This file identifies the remaining Laurent-to-Kummer comparison wall with the actual irreducibility assertion in the paper. The canonical eta coordinate in the Kummer tower is proved transcendental over the constant field. Consequently it may be used as the coefficient parameter in a rational-function field. An irreducible cleared cover polynomial then becomes the minimal polynomial of the xi coordinate, so evaluation has exactly the expected principal kernel.

theorem BGS.Markoff.splitTraceRadicand_not_constant {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) : ¬∃ (c : K), splitTraceRadicand sigma = RatFunc.C c

The rational radicand is not a constant rational function.

theorem BGS.Markoff.splitTraceBaseV_transcendental {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) : Transcendental K (splitTraceBaseV sigma)

The quadratic base coordinate is transcendental over the constant field.

theorem BGS.Markoff.splitTraceEtaRootInXiField_transcendental {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (hde : d.Coprime e) : Transcendental K (splitTraceEtaRootInXiField sigma e d)

The eta coordinate of the explicit odd-coprime Kummer tower is transcendental over K. This is the coefficient-field input needed to turn bivariate evaluation into honest univariate minimal-polynomial evaluation.

noncomputable def BGS.Markoff.splitTraceCoverIteratedPolynomial {K : Type u_1} [Field K] (sigma : K) (d e : ℕ) : Polynomial (Polynomial K)

The cleared cover, viewed as a polynomial in x with coefficients in K[y].

Equations

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

theorem BGS.Markoff.finTwoToIteratedPolynomial_splitTraceCoverPolynomial {K : Type u_1} [Field K] (sigma : K) (d e : ℕ) : finTwoToIteratedPolynomial (splitTraceCoverPolynomial 1 sigma d e) = splitTraceCoverIteratedPolynomial sigma d e

theorem BGS.Markoff.splitTraceCoverIteratedPolynomial_coeff_two_mul {K : Type u_1} [Field K] (sigma : K) (d e : ℕ) (hd : d ≠ 0) : (splitTraceCoverIteratedPolynomial sigma d e).coeff (2 * d) = -Polynomial.X ^ e

theorem BGS.Markoff.splitTraceCoverIteratedPolynomial_natDegree_ne_zero {K : Type u_1} [Field K] (sigma : K) (d e : ℕ) (hd : d ≠ 0) : (splitTraceCoverIteratedPolynomial sigma d e).natDegree ≠ 0

theorem BGS.Markoff.finTwoToIteratedPolynomial_aeval {K : Type u_1} [Field K] {A : Type u_2} [CommRing A] [Algebra K A] (p : MvPolynomial (Fin 2) K) (x y : A) : (Polynomial.aevalTower (Polynomial.aeval y) x) (finTwoToIteratedPolynomial p) = (MvPolynomial.aeval ![x, y]) p

Evaluation through the iterated-polynomial presentation is ordinary bivariate evaluation. The outer polynomial variable is coordinate 0, while the coefficient-polynomial variable is coordinate 1.

noncomputable def BGS.Markoff.splitTraceEtaPolynomialEvaluation {K : Type u_1} [Field K] (sigma : K) (e d : ℕ) : Polynomial K →ₐ[K] SplitTraceXiFunctionField K sigma e d

Evaluate a coefficient polynomial at the transcendental Kummer eta coordinate.

Equations

• BGS.Markoff.splitTraceEtaPolynomialEvaluation sigma e d = Polynomial.aeval (BGS.Markoff.splitTraceEtaRootInXiField sigma e d)

noncomputable def BGS.Markoff.splitTraceEtaRatFuncEvaluation {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (hde : d.Coprime e) : RatFunc K →ₐ[K] SplitTraceXiFunctionField K sigma e d

Specialize rational functions at the transcendental Kummer eta coordinate.

Equations

• BGS.Markoff.splitTraceEtaRatFuncEvaluation sigma hsigma e d heOdd hdOdd hde = RatFunc.liftAlgHom (BGS.Markoff.splitTraceEtaPolynomialEvaluation sigma e d) ⋯

theorem BGS.Markoff.splitTraceIteratedFractionEvaluation {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) : Polynomial.eval₂ (splitTraceEtaRatFuncEvaluation sigma hsigma e d heOdd hdOdd hde).toRingHom (splitTraceXiRoot sigma e d) (Polynomial.map (algebraMap (Polynomial K) (RatFunc K)) (finTwoToIteratedPolynomial p)) = (MvPolynomial.aeval ![splitTraceXiRoot sigma e d, splitTraceEtaRootInXiField sigma e d]) p

Mapping an iterated polynomial to K(y)[x] and then specializing the transcendental coefficient parameter y to the Kummer eta coordinate recovers direct bivariate evaluation.

theorem BGS.Markoff.splitTracePolynomial_mem_span_of_cover_irreducible_and_maps_to_zero {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (hde : d.Coprime e) (hcover : Irreducible (splitTraceCoverPolynomial 1 sigma d e)) (p : MvPolynomial (Fin 2) K) (hp : (splitTracePolynomialToKummerTop sigma hsigma e d heOdd hdOdd hde) p = 0) : p ∈ Ideal.span {splitTraceCoverPolynomial 1 sigma d e}

Once the actual cleared cover polynomial is irreducible, its principal ideal is the full kernel of evaluation at the Kummer coordinates. The proof uses eta as a transcendental coefficient parameter and the irreducible iterated polynomial as the minimal polynomial of xi.

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

The paper's irreducibility assertion is sufficient for injectivity of the explicit Laurent-to-Kummer comparison map. There is no additional hidden localization hypothesis: the coordinate-product localization was already proved faithful.

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

Exact endgame wall: in the nondegenerate odd-coprime case, injectivity of the constructed Laurent comparison is equivalent to irreducibility of the paper's cleared trace-cover polynomial. Thus proving the published irreducibility lemma closes the comparison; no extra quotient-division axiom is required.