The two-isogeny descent for the X₀(49) model

The modular curve X₀(49) is the conductor-49 elliptic curve y² + xy = x³ - x² - 2x - 1; completing the square and shifting gives the model

y² = x(x² + 21x + 112)

used here. The two-isogenous curve is Y² = X(X² - 42X - 7). The original descent images are {1, 7}: negative classes die by positivity, and the classes 2 and 14 die modulo eight. The dual images are {1, -7}: the classes -1 and 7 die by a two-step seven-adic descent. Consequently every rational point lies in one of the two cosets of doubling represented by 0 and (0,0), the group is finitely generated of rank zero, and, since the curve has no rational point of order four and reduction modulo three bounds the cardinality by four, the rational point group is exactly {0, (0,0)}.

def MazurTorsion.XZeroFortyNine.curve : WeierstrassCurve ℚ

The split model of X₀(49) used for the descent.

Equations

• MazurTorsion.XZeroFortyNine.curve = { a₁ := 0, a₂ := 21, a₃ := 0, a₄ := 112, a₆ := 0 }

instance MazurTorsion.XZeroFortyNine.instIsEllipticRatCurve : curve.IsElliptic

The dual squareclasses -1 and 7 are impossible

Dual abscissas have squareclass 1 or -7

theorem MazurTorsion.XZeroFortyNine.dual_abscissa_isSquare_or_negSeven {X Y : ℚ} (hX0 : X ≠ 0) (hdual : Y ^ 2 = X * (X ^ 2 - 42 * X - 7)) : IsSquare X ∨ ∃ (z : ℚ), X = -(7 * z ^ 2)

On the dual curve Y² = X(X² - 42X - 7), every nonzero rational abscissa is a square or -7 times a square.

Curve abscissas have squareclass 1, 2, 7, or 14

theorem MazurTorsion.XZeroFortyNine.curve_abscissa_isSquare_or_seven {U V : ℚ} (hU0 : U ≠ 0) (hcurve : V ^ 2 = U * (U ^ 2 + 21 * U + 112)) : IsSquare U ∨ ∃ (z : ℚ), U = 7 * z ^ 2

Every nonzero abscissa on the X₀(49) model is a square or seven times a square.

Reverse doubling from a square abscissa

theorem MazurTorsion.XZeroFortyNine.double_of_square_abscissa {U V : ℚ} (hU0 : U ≠ 0) (hP : curve.toAffine.Nonsingular U V) (hUSquare : IsSquare U) : ∃ (Q : curve.toAffine.Point), 2 • Q = WeierstrassCurve.Affine.Point.some U V hP

A nonzero rational point whose abscissa is a square is divisible by two. If the first auxiliary dual abscissa has squareclass -7, its conjugate (their product is -7) is a square and gives the same doubling abscissa.

The two doubling cosets and rank zero

theorem MazurTorsion.XZeroFortyNine.nonsingular_zero_zero : curve.toAffine.Nonsingular 0 0

def MazurTorsion.XZeroFortyNine.T : curve.toAffine.Point

The unique nonzero rational point killed by two.

Equations

• MazurTorsion.XZeroFortyNine.T = WeierstrassCurve.Affine.Point.some 0 0 MazurTorsion.XZeroFortyNine.nonsingular_zero_zero

theorem MazurTorsion.XZeroFortyNine.two_doubling_cosets (P : curve.toAffine.Point) : (∃ (Q : curve.toAffine.Point), P = 2 • Q) ∨ ∃ (Q : curve.toAffine.Point), P = T + 2 • Q

Every rational point lies in one of two explicit cosets of twice the rational point group.

@[reducible, inline]

abbrev MazurTorsion.XZeroFortyNine.doublingRange : AddSubgroup curve.toAffine.Point

The image of multiplication by two on the rational point group.

Equations

• MazurTorsion.XZeroFortyNine.doublingRange = (nsmulAddMonoidHom 2).range

theorem MazurTorsion.XZeroFortyNine.doubling_finiteIndex : doublingRange.FiniteIndex

The image of multiplication by two has finite index.

theorem MazurTorsion.XZeroFortyNine.point_fg : AddGroup.FG curve.toAffine.Point

The rational point group is finitely generated.

theorem MazurTorsion.XZeroFortyNine.doubling_index_le_two : doublingRange.index ≤ 2

The multiplication-by-two index is at most two.

theorem MazurTorsion.XZeroFortyNine.eq_zero_or_T_of_two_nsmul_eq_zero (P : curve.toAffine.Point) (h2 : 2 • P = 0) : P = 0 ∨ P = T

A rational point killed by two is 0 or (0,0).

theorem MazurTorsion.XZeroFortyNine.two_torsion_card_eq_two : Nat.card { P : curve.toAffine.Point // 2 • P = 0 } = 2

The X₀(49) model has exactly two rational points killed by two.

theorem MazurTorsion.XZeroFortyNine.point_rank_zero : Module.finrank ℤ curve.toAffine.Point = 0

The rational point group has Mordell--Weil rank zero.

theorem MazurTorsion.XZeroFortyNine.point_finite : Finite curve.toAffine.Point

All rational points are torsion; the rational point group is finite.

No rational point of order four

theorem MazurTorsion.XZeroFortyNine.no_order_four (Q : curve.toAffine.Point) (hQ : 2 • Q = T) : False

The X₀(49) model has no rational point of order four.