The full rational three-torsion obstruction

This file proves that the rational points of a Weierstrass curve over ℚ cannot contain a subgroup isomorphic to ZMod 3 × ZMod 3. The proof derives the three-division polynomial from the tangent formulas and uses its four hypothetical rational roots to contradict the Weierstrass coefficient relation.

theorem MazurTorsion.ThreeTorsion.tangent_forces_three_division {a₁ a₂ a₃ a₄ a₆ x y slope : ℚ} (hcurve : y ^ 2 + a₁ * x * y + a₃ * y = x ^ 3 + a₂ * x ^ 2 + a₄ * x + a₆) (hslope : slope * (2 * y + a₁ * x + a₃) = 3 * x ^ 2 + 2 * a₂ * x + a₄ - a₁ * y) (hx : slope ^ 2 + a₁ * slope - a₂ - 3 * x = 0) : 3 * x ^ 4 + (a₁ ^ 2 + 4 * a₂) * x ^ 3 + 3 * (a₁ * a₃ + 2 * a₄) * x ^ 2 + 3 * (a₃ ^ 2 + 4 * a₆) * x + (a₁ ^ 2 * a₆ + 4 * a₂ * a₆ - a₁ * a₃ * a₄ + a₂ * a₃ ^ 2 - a₄ ^ 2) = 0

theorem MazurTorsion.ThreeTorsion.three_division_tangent_identity {a₁ a₂ a₃ a₄ a₆ x y slope : ℚ} (hcurve : y ^ 2 + a₁ * x * y + a₃ * y = x ^ 3 + a₂ * x ^ 2 + a₄ * x + a₆) (hslope : slope * (2 * y + a₁ * x + a₃) = 3 * x ^ 2 + 2 * a₂ * x + a₄ - a₁ * y) : 3 * x ^ 4 + (a₁ ^ 2 + 4 * a₂) * x ^ 3 + 3 * (a₁ * a₃ + 2 * a₄) * x ^ 2 + 3 * (a₃ ^ 2 + 4 * a₆) * x + (a₁ ^ 2 * a₆ + 4 * a₂ * a₆ - a₁ * a₃ * a₄ + a₂ * a₃ ^ 2 - a₄ ^ 2) = -(2 * y + a₁ * x + a₃) ^ 2 * (slope ^ 2 + a₁ * slope - a₂ - 3 * x)

The exact algebraic identity behind the three-division polynomial: on the curve, the value of Ψ₃ is the negative square of the tangent denominator times the difference between the doubled and original x-coordinates.

theorem MazurTorsion.ThreeTorsion.nonzero_three_torsion_abscissa (W : WeierstrassCurve.Affine ℚ) (P : W.Point) (hthree : 3 • P = 0) (hne : P ≠ 0) : ∃ (x : ℚ) (y : ℚ) (hP : W.Nonsingular x y), P = WeierstrassCurve.Affine.Point.some x y hP ∧ Polynomial.eval x (WeierstrassCurve.Ψ₃ W) = 0

theorem MazurTorsion.ThreeTorsion.three_nsmul_some_eq_zero_iff (W : WeierstrassCurve.Affine ℚ) {x y : ℚ} (hP : W.Nonsingular x y) : 3 • WeierstrassCurve.Affine.Point.some x y hP = 0 ↔ Polynomial.eval x (WeierstrassCurve.Ψ₃ W) = 0

For a nonsingular affine point over ℚ, vanishing of the three-division polynomial is equivalent to the point being killed by 3.

theorem MazurTorsion.ThreeTorsion.ncard_three_torsion_le_nine (W : WeierstrassCurve.Affine ℚ) : {P : W.Point | 3 • P = 0}.ncard ≤ 9

The rational three-torsion of a Weierstrass curve has at most nine points.

theorem MazurTorsion.ThreeTorsion.quartic_coefficients_of_four_distinct_roots {b₂ b₄ b₆ b₈ r₁ r₂ r₃ r₄ : ℚ} (hne₁₂ : r₁ ≠ r₂) (hne₁₃ : r₁ ≠ r₃) (hne₁₄ : r₁ ≠ r₄) (hne₂₃ : r₂ ≠ r₃) (hne₂₄ : r₂ ≠ r₄) (hne₃₄ : r₃ ≠ r₄) (h₁ : 3 * r₁ ^ 4 + b₂ * r₁ ^ 3 + 3 * b₄ * r₁ ^ 2 + 3 * b₆ * r₁ + b₈ = 0) (h₂ : 3 * r₂ ^ 4 + b₂ * r₂ ^ 3 + 3 * b₄ * r₂ ^ 2 + 3 * b₆ * r₂ + b₈ = 0) (h₃ : 3 * r₃ ^ 4 + b₂ * r₃ ^ 3 + 3 * b₄ * r₃ ^ 2 + 3 * b₆ * r₃ + b₈ = 0) (h₄ : 3 * r₄ ^ 4 + b₂ * r₄ ^ 3 + 3 * b₄ * r₄ ^ 2 + 3 * b₆ * r₄ + b₈ = 0) : b₂ = -3 * (r₁ + r₂ + r₃ + r₄) ∧ b₄ = r₁ * r₂ + r₁ * r₃ + r₁ * r₄ + r₂ * r₃ + r₂ * r₄ + r₃ * r₄ ∧ b₆ = -(r₁ * r₂ * r₃ + r₁ * r₂ * r₄ + r₁ * r₃ * r₄ + r₂ * r₃ * r₄) ∧ b₈ = 3 * (r₁ * r₂ * r₃ * r₄)

theorem MazurTorsion.ThreeTorsion.four_distinct_roots_invariant_impossible {b₂ b₄ b₆ b₈ r₁ r₂ r₃ r₄ : ℚ} (hne₁₂ : r₁ ≠ r₂) (hne₃₄ : r₃ ≠ r₄) (hb₂ : b₂ = -3 * (r₁ + r₂ + r₃ + r₄)) (hb₄ : b₄ = r₁ * r₂ + r₁ * r₃ + r₁ * r₄ + r₂ * r₃ + r₂ * r₄ + r₃ * r₄) (hb₆ : b₆ = -(r₁ * r₂ * r₃ + r₁ * r₂ * r₄ + r₁ * r₃ * r₄ + r₂ * r₃ * r₄)) (hb₈ : b₈ = 3 * (r₁ * r₂ * r₃ * r₄)) (hrel : 4 * b₈ = b₂ * b₆ - b₄ ^ 2) : False

theorem MazurTorsion.ThreeTorsion.not_injective_zmod_three_square (E : WeierstrassCurve ℚ) (φ : ZMod 3 × ZMod 3 →+ (WeierstrassCurve.Affine.baseChange E ℚ).Point) : ¬Function.Injective ⇑φ

There is no full rational three-torsion subgroup on a Weierstrass curve over ℚ.