A hyperelliptic model for the order-thirteen parameter curve

This file gives a checked rational map from the reduced Tate-parameter equation in OrderThirteenReduction to the standard sextic model

y² = x⁶ + 2x⁵ + x⁴ + 2x³ + 6x² + 4x + 1.

The map is obtained by elementary completion of the square after resolving the singular plane model. Its only denominators are s-1 and r-s; both were already proved nonzero from exact order in the preceding reduction.

The two rational affine cusp abscissas on the sextic are 0 and -1. The forward image of an exact-order certificate has neither abscissa: x = 0 would discard r-1 or s-1, while x = -1 would discard the separately retained factor rs-2r+1.

def MazurTorsion.Kubert.orderThirteenHyperellipticPolynomial (x : ℚ) : ℚ

The sextic defining the hyperelliptic model of X₁(13).

Equations

• MazurTorsion.Kubert.orderThirteenHyperellipticPolynomial x = x ^ 6 + 2 * x ^ 5 + x ^ 4 + 2 * x ^ 3 + 6 * x ^ 2 + 4 * x + 1

def MazurTorsion.Kubert.orderThirteenHyperellipticX (r s : ℚ) : ℚ

The hyperelliptic abscissa attached to a reduced Tate certificate.

Equations

• MazurTorsion.Kubert.orderThirteenHyperellipticX r s = -((r - 1) * (s - 1) / (r - s))

def MazurTorsion.Kubert.orderThirteenHyperellipticY (r s : ℚ) : ℚ

The hyperelliptic ordinate attached to a reduced Tate certificate.

Writing U = (r-1)(s-1)/(r-s) and V = (r-s)/(1-s), the intermediate quadratic model is

V² + (U³-U²-1)V - U² + U = 0.

Completing its square and replacing U by -x gives the displayed formula.

Equations

• MazurTorsion.Kubert.orderThirteenHyperellipticY r s = 2 * ((r - s) / (1 - s)) + (((r - 1) * (s - 1) / (r - s)) ^ 3 - ((r - 1) * (s - 1) / (r - s)) ^ 2 - 1)

theorem MazurTorsion.Kubert.orderThirteen_hyperelliptic_cleared_identity (r s : ℚ) (hsone : s ≠ 1) (hrs : r ≠ s) : (r - s) ^ 2 * (s - 1) ^ 2 * (orderThirteenHyperellipticY r s ^ 2 - orderThirteenHyperellipticPolynomial (orderThirteenHyperellipticX r s)) = 4 * (r - 1) * orderThirteenReducedPolynomial r s

Cleared polynomial identity underlying the rational map to the sextic.

theorem MazurTorsion.Kubert.orderThirteen_reduced_to_hyperelliptic (r s : ℚ) (hsone : s ≠ 1) (hrs : r ≠ s) (hreduced : orderThirteenReducedPolynomial r s = 0) : orderThirteenHyperellipticY r s ^ 2 = orderThirteenHyperellipticPolynomial (orderThirteenHyperellipticX r s)

A noncuspidal point on the reduced Tate model maps to the hyperelliptic sextic.

theorem MazurTorsion.Kubert.orderThirteenHyperellipticX_ne_zero (r s : ℚ) (hrone : r ≠ 1) (hsone : s ≠ 1) (hrs : r ≠ s) : orderThirteenHyperellipticX r s ≠ 0

theorem MazurTorsion.Kubert.orderThirteenHyperellipticX_ne_neg_one (r s : ℚ) (hrs : r ≠ s) (hfactor : r * s - 2 * r + 1 ≠ 0) : orderThirteenHyperellipticX r s ≠ -1

theorem MazurTorsion.Kubert.exists_orderThirteen_hyperelliptic_certificate (E : WeierstrassCurve ℚ) [E.IsElliptic] (Q : (WeierstrassCurve.Affine.baseChange E ℚ).Point) (hQ : addOrderOf Q = 13) : ∃ (x : ℚ) (y : ℚ), y ^ 2 = orderThirteenHyperellipticPolynomial x ∧ x ≠ 0 ∧ x ≠ -1

An exact rational point of order 13 produces an affine rational point on the standard sextic whose abscissa is neither rational affine cusp abscissa.

theorem MazurTorsion.Kubert.rationalPoint_addOrderOf_ne_thirteen_of_noNoncuspidalPoint (E : WeierstrassCurve ℚ) [E.IsElliptic] (Q : (WeierstrassCurve.Affine.baseChange E ℚ).Point) (hNoNoncuspidal : ∀ (x y : ℚ), x ≠ 0 → x ≠ -1 → y ^ 2 = orderThirteenHyperellipticPolynomial x → False) : addOrderOf Q ≠ 13

A route-neutral exclusion of noncuspidal rational points on the hyperelliptic model rules out exact rational order thirteen.