The order-eleven Tate curve and X₁(11)

This file gives a denominator-safe bridge from the compact Tate parameter equation in OrderElevenReduction to the standard model

v² + v = u³ - u²

of X₁(11).

Put

r = b/c, q = c²/(b-c).

The compact polynomial is a nonzero scalar multiple of the raw equation

r² - rq³ + 3rq² - 4rq + q = 0.

Writing

N = rq - 2r + 1, K = q² - q - r + 1,

the checked rational map is

u = K/N,

v = (q-r)K/N² - 1.

For context, this is the composition of the standard raw-to-plane map

x = (q-r)/N, y = N/K

to x²y - xy² + y - 1 = 0 with the projective linear change

u = 1/y, v = x/y - 1.

The raw equation proves N, K, and q-r nonzero on the honest Tate locus. Thus an exact order-eleven point maps to an affine point whose abscissa is neither 0 nor 1, the abscissae of the four rational finite cusp points on this model. No rational-point classification is asserted.

def MazurTorsion.XOneEleven.curve : WeierstrassCurve ℚ

The standard elliptic model v²+v=u³-u² of X₁(11).

Equations

• MazurTorsion.XOneEleven.curve = { a₁ := 0, a₂ := -1, a₃ := 1, a₄ := 0, a₆ := 0 }

def MazurTorsion.Kubert.orderElevenRawPolynomial (r q : ℚ) : ℚ

The raw affine equation for X₁(11).

Equations

• MazurTorsion.Kubert.orderElevenRawPolynomial r q = r ^ 2 - r * q ^ 3 + 3 * r * q ^ 2 - 4 * r * q + q

def MazurTorsion.Kubert.orderElevenRawR (b c : ℚ) : ℚ

The raw parameter r=b/c.

Equations

• MazurTorsion.Kubert.orderElevenRawR b c = b / c

def MazurTorsion.Kubert.orderElevenRawQ (b c : ℚ) : ℚ

The raw parameter q=c²/(b-c).

Equations

• MazurTorsion.Kubert.orderElevenRawQ b c = c ^ 2 / (b - c)

def MazurTorsion.Kubert.orderElevenModelUOfRaw (r q : ℚ) : ℚ

The Weierstrass abscissa obtained from raw parameters.

Equations

• MazurTorsion.Kubert.orderElevenModelUOfRaw r q = (q ^ 2 - q - r + 1) / (r * q - 2 * r + 1)

def MazurTorsion.Kubert.orderElevenModelVOfRaw (r q : ℚ) : ℚ

The Weierstrass ordinate obtained from raw parameters.

Equations

• MazurTorsion.Kubert.orderElevenModelVOfRaw r q = (q - r) * (q ^ 2 - q - r + 1) / (r * q - 2 * r + 1) ^ 2 - 1

def MazurTorsion.Kubert.orderElevenModelU (b c : ℚ) : ℚ

The u-coordinate attached directly to Tate parameters.

Equations

• MazurTorsion.Kubert.orderElevenModelU b c = MazurTorsion.Kubert.orderElevenModelUOfRaw (MazurTorsion.Kubert.orderElevenRawR b c) (MazurTorsion.Kubert.orderElevenRawQ b c)

def MazurTorsion.Kubert.orderElevenModelV (b c : ℚ) : ℚ

The v-coordinate attached directly to Tate parameters.

Equations

• MazurTorsion.Kubert.orderElevenModelV b c = MazurTorsion.Kubert.orderElevenModelVOfRaw (MazurTorsion.Kubert.orderElevenRawR b c) (MazurTorsion.Kubert.orderElevenRawQ b c)

theorem MazurTorsion.Kubert.orderElevenRawPolynomial_eq_zero {b c : ℚ} (hc : c ≠ 0) (hbc : b ≠ c) (hpoly : orderElevenPolynomial b c = 0) : orderElevenRawPolynomial (orderElevenRawR b c) (orderElevenRawQ b c) = 0

The compact Tate equation is the raw X₁(11) equation after the displayed denominator-safe substitution.

theorem MazurTorsion.Kubert.orderElevenModel_factors_ne_zero {b c : ℚ} (hb : b ≠ 0) (hc : c ≠ 0) (hbc : b ≠ c) (hA : c ^ 2 + c - b ≠ 0) (hpoly : orderElevenPolynomial b c = 0) : have r := orderElevenRawR b c; have q := orderElevenRawQ b c; r * q - 2 * r + 1 ≠ 0 ∧ q ^ 2 - q - r + 1 ≠ 0 ∧ q - r ≠ 0 ∧ q ≠ 1

Every denominator and both rational finite-cusp factors of the model map are nonzero on the admissible Tate locus.

theorem MazurTorsion.Kubert.orderElevenModel_curve_equation_of_raw {r q : ℚ} (hmiddle : r * q - 2 * r + 1 ≠ 0) (hraw : orderElevenRawPolynomial r q = 0) : orderElevenModelVOfRaw r q ^ 2 + orderElevenModelVOfRaw r q = orderElevenModelUOfRaw r q ^ 3 - orderElevenModelUOfRaw r q ^ 2

The raw rational formulas satisfy the standard Weierstrass equation whenever their sole denominator is nonzero.

theorem MazurTorsion.Kubert.orderElevenModel_curve_equation {b c : ℚ} (hb : b ≠ 0) (hc : c ≠ 0) (hbc : b ≠ c) (hA : c ^ 2 + c - b ≠ 0) (hpoly : orderElevenPolynomial b c = 0) : orderElevenModelV b c ^ 2 + orderElevenModelV b c = orderElevenModelU b c ^ 3 - orderElevenModelU b c ^ 2

The Tate-parameter image lies on v²+v=u³-u².

theorem MazurTorsion.Kubert.orderElevenModel_nonsingular {b c : ℚ} (hb : b ≠ 0) (hc : c ≠ 0) (hbc : b ≠ c) (hA : c ^ 2 + c - b ≠ 0) (hpoly : orderElevenPolynomial b c = 0) : XOneEleven.curve.toAffine.Nonsingular (orderElevenModelU b c) (orderElevenModelV b c)

The image coordinates define an affine point on the standard X₁(11) model.

theorem MazurTorsion.Kubert.orderElevenModelU_ne_zero {b c : ℚ} (hb : b ≠ 0) (hc : c ≠ 0) (hbc : b ≠ c) (hA : c ^ 2 + c - b ≠ 0) (hpoly : orderElevenPolynomial b c = 0) : orderElevenModelU b c ≠ 0

The image avoids the rational finite-cusp abscissa u=0.

theorem MazurTorsion.Kubert.orderElevenModelU_ne_one {b c : ℚ} (hb : b ≠ 0) (hc : c ≠ 0) (hbc : b ≠ c) (hA : c ^ 2 + c - b ≠ 0) (hpoly : orderElevenPolynomial b c = 0) : orderElevenModelU b c ≠ 1

The image avoids the rational finite-cusp abscissa u=1.

theorem MazurTorsion.Kubert.orderElevenModel_of_admissible {b c : ℚ} (hb : b ≠ 0) (hc : c ≠ 0) (hbc : b ≠ c) (hA : c ^ 2 + c - b ≠ 0) (hpoly : orderElevenPolynomial b c = 0) : XOneEleven.curve.toAffine.Nonsingular (orderElevenModelU b c) (orderElevenModelV b c) ∧ orderElevenModelU b c ≠ 0 ∧ orderElevenModelU b c ≠ 1

The complete bridge: admissible Tate parameters give a nonsingular point outside both rational finite-cusp abscissae on X₁(11).

theorem MazurTorsion.Kubert.exists_orderElevenModel_of_exact_order (E : WeierstrassCurve ℚ) [E.IsElliptic] (Q : (WeierstrassCurve.Affine.baseChange E ℚ).Point) (hQ : addOrderOf Q = 11) : ∃ (b : ℚ) (c : ℚ), XOneEleven.curve.toAffine.Nonsingular (orderElevenModelU b c) (orderElevenModelV b c) ∧ orderElevenModelU b c ≠ 0 ∧ orderElevenModelU b c ≠ 1

An exact rational point of order eleven produces an affine point on the standard X₁(11) model outside all rational cusp points: the point at infinity is avoided by affineness, and the four finite ones have abscissa 0 or 1.