Kummer descent for the split trace power cover

The normalized split trace cover is obtained from the base curve

u * (1 - u) * v^2 + sigma * u - 1 = 0

by adjoining eta and xi with eta^e = v and xi^d = u * v. This file makes that two-stage Kummer construction explicit. Oddness is imposed because Mathlib's composite-binomial criterion currently covers odd exponents; coprimality of d and e is used in the second norm argument. Neither hypothesis is hidden in a structure field.

theorem BGS.Markoff.eval_splitTraceCoverPolynomial_of_powerRootRelations {L : Type u_1} [Field L] (sigma u v xi eta : L) (d e : ℕ) (hbase : u * (1 - u) * v ^ 2 + sigma * u - 1 = 0) (heta : eta ^ e = v) (hxi : xi ^ d = u * v) : (MvPolynomial.eval ![xi, eta]) (splitTraceCoverPolynomial 1 sigma d e) = 0

The two Kummer root relations really land on the correctly cleared trace-cover polynomial.

noncomputable def BGS.Markoff.splitTraceRadicandNumerator {K : Type u_1} [Field K] (sigma : K) : Polynomial K

Numerator of the quadratic radicand on the rational u-line.

Equations

• BGS.Markoff.splitTraceRadicandNumerator sigma = 1 - Polynomial.C sigma * Polynomial.X

noncomputable def BGS.Markoff.splitTraceRadicandDenominator {K : Type u_1} [Field K] : Polynomial K

Denominator of the quadratic radicand on the rational u-line.

Equations

• BGS.Markoff.splitTraceRadicandDenominator = Polynomial.X * (1 - Polynomial.X)

noncomputable def BGS.Markoff.splitTraceRadicand {K : Type u_1} [Field K] (sigma : K) : RatFunc K

The base trace curve has function equation v^2 = splitTraceRadicand sigma.

Equations

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

theorem BGS.Markoff.splitTraceRadicandNumerator_natDegree {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) : (splitTraceRadicandNumerator sigma).natDegree = 1

theorem BGS.Markoff.splitTraceRadicandDenominator_natDegree {K : Type u_1} [Field K] : splitTraceRadicandDenominator.natDegree = 2

theorem BGS.Markoff.splitTraceRadicandNumerator_ne_zero {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) : splitTraceRadicandNumerator sigma ≠ 0

theorem BGS.Markoff.splitTraceRadicandDenominator_ne_zero {K : Type u_1} [Field K] : splitTraceRadicandDenominator ≠ 0

theorem BGS.Markoff.splitTraceRadicand_ne_zero {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) : splitTraceRadicand sigma ≠ 0

theorem BGS.Markoff.splitTraceRadicand_intDegree {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) : (splitTraceRadicand sigma).intDegree = -1

theorem BGS.Markoff.splitTraceRadicand_equation {K : Type u_1} [Field K] (sigma : K) : RatFunc.X * (1 - RatFunc.X) * splitTraceRadicand sigma + RatFunc.C sigma * RatFunc.X - 1 = 0

The rational radicand satisfies the cleared base trace equation before adjoining its square root.

theorem BGS.Markoff.RatFunc.intDegree_pow {K : Type u_1} [Field K] (z : RatFunc K) (hz : z ≠ 0) (n : ℕ) : (z ^ n).intDegree = ↑n * z.intDegree

theorem BGS.Markoff.RatFunc.pow_ne_of_not_dvd_intDegree {K : Type u_1} [Field K] (a : RatFunc K) (ha : a ≠ 0) (q : ℕ) (hdegree : ¬↑q ∣ a.intDegree) (z : RatFunc K) : z ^ q ≠ a

An element of rational-function degree not divisible by q cannot be a q-th power.

noncomputable def BGS.Markoff.splitTraceBaseKummerPolynomial {K : Type u_1} [Field K] (sigma : K) : Polynomial (RatFunc K)

The monic quadratic defining the base function field.

Equations

• BGS.Markoff.splitTraceBaseKummerPolynomial sigma = Polynomial.X ^ 2 - Polynomial.C (BGS.Markoff.splitTraceRadicand sigma)

theorem BGS.Markoff.splitTraceBaseKummerPolynomial_irreducible {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) : Irreducible (splitTraceBaseKummerPolynomial sigma)

theorem BGS.Markoff.norm_splitTraceBaseRoot {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) : (Algebra.norm (RatFunc K)) (AdjoinRoot.root (splitTraceBaseKummerPolynomial sigma)) = -splitTraceRadicand sigma

The quadratic base root has norm -splitTraceRadicand sigma.

theorem BGS.Markoff.splitTraceBaseRoot_not_primePower {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (q : ℕ) (hq : Nat.Prime q) (z : AdjoinRoot (splitTraceBaseKummerPolynomial sigma)) : z ^ q ≠ AdjoinRoot.root (splitTraceBaseKummerPolynomial sigma)

A prime-power root of the base coordinate v cannot already lie in the quadratic base function field. The obstruction is the rational-function degree -1 of its norm.

theorem BGS.Markoff.splitTraceEtaKummerPolynomial_irreducible {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e : ℕ) (heOdd : Odd e) : Irreducible (Polynomial.X ^ e - Polynomial.C (AdjoinRoot.root (splitTraceBaseKummerPolynomial sigma)))

For every positive odd e, adjoining an e-th root of the base coordinate v is a genuine degree-e Kummer extension.

noncomputable def BGS.Markoff.splitTraceBaseU {K : Type u_1} [Field K] (sigma : K) : AdjoinRoot (splitTraceBaseKummerPolynomial sigma)

The rational parameter u, embedded in the quadratic base function field.

Equations

• BGS.Markoff.splitTraceBaseU sigma = (algebraMap (RatFunc K) (AdjoinRoot (BGS.Markoff.splitTraceBaseKummerPolynomial sigma))) RatFunc.X

noncomputable def BGS.Markoff.splitTraceBaseV {K : Type u_1} [Field K] (sigma : K) : AdjoinRoot (splitTraceBaseKummerPolynomial sigma)

The quadratic coordinate v in the base function field.

Equations

• BGS.Markoff.splitTraceBaseV sigma = AdjoinRoot.root (BGS.Markoff.splitTraceBaseKummerPolynomial sigma)

theorem BGS.Markoff.splitTraceBaseU_V_equation {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) : splitTraceBaseU sigma * (1 - splitTraceBaseU sigma) * splitTraceBaseV sigma ^ 2 + (algebraMap (RatFunc K) (AdjoinRoot (splitTraceBaseKummerPolynomial sigma))) (RatFunc.C sigma) * splitTraceBaseU sigma - 1 = 0

The two base coordinates satisfy the birational trace equation inside the quadratic function field.

theorem BGS.Markoff.splitTraceBaseFunctionField_finrank {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) : Module.finrank (RatFunc K) (AdjoinRoot (splitTraceBaseKummerPolynomial sigma)) = 2

theorem BGS.Markoff.norm_splitTraceBaseU_mul_V_intDegree {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) : ((Algebra.norm (RatFunc K)) (splitTraceBaseU sigma * splitTraceBaseV sigma)).intDegree = 1

The norm of u * v has rational-function degree one. This is the second independent divisor obstruction used after adjoining the e-th root of v.

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

The first Kummer polynomial, adjoining eta with eta^e = v.

Equations

• BGS.Markoff.splitTraceEtaKummerPolynomial sigma e = Polynomial.X ^ e - Polynomial.C (BGS.Markoff.splitTraceBaseV sigma)

theorem BGS.Markoff.splitTraceEtaKummerPolynomial_irreducible' {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e : ℕ) (heOdd : Odd e) : Irreducible (splitTraceEtaKummerPolynomial sigma e)

theorem BGS.Markoff.splitTraceEtaFunctionField_finrank {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e : ℕ) (heOdd : Odd e) : Module.finrank (AdjoinRoot (splitTraceBaseKummerPolynomial sigma)) (AdjoinRoot (splitTraceEtaKummerPolynomial sigma e)) = e

noncomputable def BGS.Markoff.splitTraceXiRadicand {K : Type u_1} [Field K] (sigma : K) (e : ℕ) : AdjoinRoot (splitTraceEtaKummerPolynomial sigma e)

The second Kummer radicand, corresponding to xi^d = u * v.

Equations

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

theorem BGS.Markoff.splitTraceXiRadicand_not_primePower {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e : ℕ) (heOdd : Odd e) (q : ℕ) (hq : Nat.Prime q) (hqe : ¬q ∣ e) (z : AdjoinRoot (splitTraceEtaKummerPolynomial sigma e)) : z ^ q ≠ splitTraceXiRadicand sigma e

After adjoining the e-th root of v, the element u*v is not a q-th power whenever q is prime and coprime to e. The proof takes two successive norms; their rational-function degree forces q to divide e, a contradiction.

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

The second Kummer polynomial, adjoining xi with xi^d = u*v.

Equations

• BGS.Markoff.splitTraceXiKummerPolynomial sigma e d = Polynomial.X ^ d - Polynomial.C (BGS.Markoff.splitTraceXiRadicand sigma e)

@[reducible, inline]

abbrev BGS.Markoff.SplitTraceBaseFunctionField (K : Type u_2) [Field K] (sigma : K) : Type u_2

The three fields in the explicit Kummer tower.

Equations

• BGS.Markoff.SplitTraceBaseFunctionField K sigma = AdjoinRoot (BGS.Markoff.splitTraceBaseKummerPolynomial sigma)

@[reducible, inline]

abbrev BGS.Markoff.SplitTraceEtaFunctionField (K : Type u_2) [Field K] (sigma : K) (e : ℕ) : Type u_2

The function field of the split trace curve expressed using the eta coordinate.

Equations

• BGS.Markoff.SplitTraceEtaFunctionField K sigma e = AdjoinRoot (BGS.Markoff.splitTraceEtaKummerPolynomial sigma e)

@[reducible, inline]

abbrev BGS.Markoff.SplitTraceXiFunctionField (K : Type u_2) [Field K] (sigma : K) (e d : ℕ) : Type u_2

The function field of the split trace curve expressed using the xi coordinate.

Equations

• BGS.Markoff.SplitTraceXiFunctionField K sigma e d = AdjoinRoot (BGS.Markoff.splitTraceXiKummerPolynomial sigma e d)

noncomputable def BGS.Markoff.splitTraceBaseElementInXiField {K : Type u_1} [Field K] (sigma : K) (e d : ℕ) (a : SplitTraceBaseFunctionField K sigma) : SplitTraceXiFunctionField K sigma e d

Embed a base-function-field element through both Kummer stages.

Equations

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

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

The canonical eta root, embedded into the top Kummer field.

Equations

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

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

The canonical xi root in the top Kummer field.

Equations

• BGS.Markoff.splitTraceXiRoot sigma e d = AdjoinRoot.root (BGS.Markoff.splitTraceXiKummerPolynomial sigma e d)

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

For positive odd coprime exponents, the second Kummer polynomial is irreducible. This is the connectedness step that the printed translate argument does not supply.

theorem BGS.Markoff.splitTraceKummerTower_roots_on_cover {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (hde : d.Coprime e) : (MvPolynomial.eval ![splitTraceXiRoot sigma e d, splitTraceEtaRootInXiField sigma e d]) (splitTraceCoverPolynomial 1 (splitTraceBaseElementInXiField sigma e d ((algebraMap (RatFunc K) (SplitTraceBaseFunctionField K sigma)) (RatFunc.C sigma))) d e) = 0

The canonical roots of the proved Kummer tower lie on the exact cleared trace-cover polynomial. This connects the function-field construction back to splitTraceCoverPolynomial.

theorem BGS.Markoff.splitTraceXiFunctionField_finrank {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (hde : d.Coprime e) : Module.finrank (AdjoinRoot (splitTraceEtaKummerPolynomial sigma e)) (AdjoinRoot (splitTraceXiKummerPolynomial sigma e d)) = d

theorem BGS.Markoff.splitTraceOddCoprimeKummerTower_isDomain {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (hde : d.Coprime e) : IsDomain (AdjoinRoot (splitTraceXiKummerPolynomial sigma e d))

The iterated Kummer function-field tower for the odd, coprime split trace power cover is a domain. All three irreducibility facts are constructed from the explicit norm-degree arguments above; none is assumed as a field or typeclass parameter. This theorem does not yet identify the tower with a localization or tensor base change of the affine coordinate ring.

theorem BGS.Markoff.splitTraceOddCoprimeKummerTower_isDomain_afterConstantExtension {K : Type u_1} [Field K] {L : Type u_2} [Field L] (phi : K →+* L) (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (hde : d.Coprime e) : IsDomain (AdjoinRoot (splitTraceXiKummerPolynomial (phi sigma) e d))

Reconstructing the same explicit Kummer tower after an arbitrary extension of the constant field again gives a domain. The remaining scheme-level wall is to identify this reconstructed tower with the localization of the tensor-product base change of the original coordinate ring.