The Laurent split trace cover inside its Kummer function field

This file constructs the comparison map that was missing between the denominator-cleared affine trace-cover coordinate ring, localized away from the two coordinate axes, and the explicit odd-coprime Kummer tower. Injectivity is kept as the visible remaining wall; it is not encoded as an axiom or typeclass field.

@[reducible, inline]

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

The affine coordinate ring of the normalized split trace cover.

Equations

• BGS.Markoff.SplitTraceAffineCoordinateRing K sigma d e = (MvPolynomial (Fin 2) K ⧸ Ideal.span {BGS.Markoff.splitTraceCoverPolynomial 1 sigma d e})

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

The product of the two coordinate functions in the affine trace-cover ring.

Equations

• BGS.Markoff.splitTraceAffineCoordinateProduct sigma d e = (Ideal.Quotient.mk (Ideal.span {BGS.Markoff.splitTraceCoverPolynomial 1 sigma d e})) (MvPolynomial.X 0 * MvPolynomial.X 1)

@[reducible, inline]

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

The coordinate ring of the open trace cover in the two-dimensional torus.

Equations

• BGS.Markoff.SplitTraceLaurentCoordinateRing K sigma d e = Localization.Away (BGS.Markoff.splitTraceAffineCoordinateProduct sigma d e)

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

Evaluation of the two affine coordinates at the canonical roots of the Kummer tower.

Equations

• BGS.Markoff.splitTracePolynomialToKummerTop sigma hsigma e d heOdd hdOdd hde = MvPolynomial.aeval ![BGS.Markoff.splitTraceXiRoot sigma e d, BGS.Markoff.splitTraceEtaRootInXiField sigma e d]

theorem BGS.Markoff.splitTracePolynomialToKummerTop_relation {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (hde : d.Coprime e) : (splitTracePolynomialToKummerTop sigma hsigma e d heOdd hdOdd hde) (splitTraceCoverPolynomial 1 sigma d e) = 0

The defining affine trace-cover relation vanishes under evaluation in the Kummer tower.

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

The affine trace-cover coordinate ring maps canonically to the Kummer top field.

Equations

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

@[simp]

theorem BGS.Markoff.splitTraceAffineToKummerTop_coordinate {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (hde : d.Coprime e) (i : Fin 2) : (splitTraceAffineToKummerTop sigma hsigma e d heOdd hdOdd hde) ((Ideal.Quotient.mk (Ideal.span {splitTraceCoverPolynomial 1 sigma d e})) (MvPolynomial.X i)) = ![splitTraceXiRoot sigma e d, splitTraceEtaRootInXiField sigma e d] i

theorem BGS.Markoff.splitTraceBaseV_sq {K : Type u_1} [Field K] (sigma : K) : splitTraceBaseV sigma ^ 2 = (algebraMap (RatFunc K) (SplitTraceBaseFunctionField K sigma)) (splitTraceRadicand sigma)

theorem BGS.Markoff.splitTraceEtaRoot_pow {K : Type u_1} [Field K] (sigma : K) (e : ℕ) : AdjoinRoot.root (splitTraceEtaKummerPolynomial sigma e) ^ e = (algebraMap (SplitTraceBaseFunctionField K sigma) (SplitTraceEtaFunctionField K sigma e)) (splitTraceBaseV sigma)

theorem BGS.Markoff.splitTraceXiRoot_pow {K : Type u_1} [Field K] (sigma : K) (e d : ℕ) : splitTraceXiRoot sigma e d ^ d = (algebraMap (SplitTraceEtaFunctionField K sigma e) (SplitTraceXiFunctionField K sigma e d)) (splitTraceXiRadicand sigma e)

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

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

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

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

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

theorem BGS.Markoff.splitTraceAffineCoordinateProduct_maps_to_isUnit {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (hde : d.Coprime e) : IsUnit ((splitTraceAffineToKummerTop sigma hsigma e d heOdd hdOdd hde) (splitTraceAffineCoordinateProduct sigma d e))

The image of the coordinate product is a unit for algebraic reasons internal to the Kummer tower. This proof uses the three root-power equations, rather than treating the top quotient as a field through a late typeclass instance.

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

The affine comparison map extends uniquely across the localization inverting both trace-cover coordinates.

Equations

• BGS.Markoff.splitTraceLaurentToKummerTop sigma hsigma e d heOdd hdOdd hde = IsLocalization.Away.liftAlgHom (BGS.Markoff.splitTraceAffineCoordinateProduct sigma d e) ⋯

theorem BGS.Markoff.splitTraceLaurentToKummerTop_algebraMap_apply {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (hde : d.Coprime e) (a : SplitTraceAffineCoordinateRing K sigma d e) : (splitTraceLaurentToKummerTop sigma hsigma e d heOdd hdOdd hde) ((algebraMap (SplitTraceAffineCoordinateRing K sigma d e) (SplitTraceLaurentCoordinateRing K sigma d e)) a) = (splitTraceAffineToKummerTop sigma hsigma e d heOdd hdOdd hde) a

theorem BGS.Markoff.splitTraceLaurentToKummerTop_injective_of_affine_injective {K : Type u_1} [Field K] (sigma : K) (hsigma : sigma ≠ 0) (e d : ℕ) (heOdd : Odd e) (hdOdd : Odd d) (hde : d.Coprime e) (hAffine : Function.Injective ⇑(splitTraceAffineToKummerTop sigma hsigma e d heOdd hdOdd hde)) : Function.Injective ⇑(splitTraceLaurentToKummerTop sigma hsigma e d heOdd hdOdd hde)

Injectivity of the Laurent comparison map is reduced exactly to injectivity of the affine quotient map. No domain hypothesis is manufactured here: proving the affine map injective is the remaining kernel-equality/irreducibility wall.