Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_WeierstrassCurve_VeluBundledMap.lean

definition module

Bundled Vélu point map for a single 3-torsion kernel point

Fix a Weierstrass curve W over a field F. For a finite set S \subset F \times F the project's Vélu data attach to each Q = (x_Q,y_Q) the quantities G^x_Q = 3x_Q^2 + 2a_2x_Q + a_4 - a_1y_Q, G^y_Q = -(2y_Q + a_1x_Q + a_3), t_Q = 2G^x_Q - a_1G^y_Q, u_Q = (G^y_Q)^2, the quotient curve veluQuotient with coefficients a_1,a_2,a_3, a_4 - 5\sum_S t_Q, a_6 - b_2\sum_S t_Q - 7\sum_S(u_Q + x_Qt_Q), and the coordinate functions \mathrm{veluX}(x) = x + \sum_S\bigl(t_Q/(x-x_Q) + u_Q/(x-x_Q)^2\bigr) and \mathrm{veluY}(x,y) = y - \sum_S\bigl(u_Q(2y+a_1x+a_3)/(x-x_Q)^3 + t_Q(a_1(x-x_Q)+y-y_Q)/(x-x_Q)^2 + (a_1u_Q - G^x_QG^y_Q)/(x-x_Q)^2\bigr).

The module first records negation equivariance at the level of coordinates: for every S and all x,y \in F, \mathrm{veluY}(x, -y-a_1x-a_3) equals the value of \mathrm{negY} for the quotient curve at (\mathrm{veluX}(x), \mathrm{veluY}(x,y)), an identity of field elements valid for all x (division by zero being zero). Next, for a point (x_0,y_0) on W with \Psi_3(x_0) = 0, a point (x,y) on W with x \neq x_0, and under the hypothesis \Delta \neq 0 for W/\{(x_0,y_0)\}, the image (\mathrm{veluX}(x), \mathrm{veluY}(x,y)) is a nonsingular point of the quotient curve; this combines the cleared-denominator Vélu equation with the fact that over a field a point satisfying the Weierstrass equation of a curve with nonzero discriminant is nonsingular.

Under these hypotheses veluPointMap3 is then defined as the map W(F) \to (W/\{(x_0,y_0)\})(F) on affine point types sending the point at infinity, and every affine point with x = x_0, to the point at infinity, and any other affine point (x,y) to (\mathrm{veluX}(x), \mathrm{veluY}(x,y)). Its computation rules in the three cases are recorded, together with the statement that it commutes with negation, \mathrm{veluPointMap3}(-P) = -\mathrm{veluPointMap3}(P). No additivity statement is made here, so the map is not asserted to be a group homomorphism.

Relation to Mathlib

Mathlib supplies the ambient notions used: WeierstrassCurve, its affine model with Equation, Nonsingular, negY and the point type Affine.Point, the division polynomial \Psi_3, and the implication from the Weierstrass equation to nonsingularity when \Delta \neq 0. The Vélu quotient curve, the coordinate functions veluX, veluY and the resulting point map are the project's own; Mathlib has no construction of isogenies with prescribed kernel.

Where it is used

These definitions form part of a development of Vélu's formulas: an explicit quotient Weierstrass curve attached to a finite set of points, and the induced map on rational points, here for a kernel generated by a single point whose abscissa is a root of the third division polynomial.

References

  1. J. Vélu, Isogénies entre courbes elliptiques, C. R. Acad. Sci. Paris Sér. A 273 (1971), 238–241
  2. L. C. Washington, Elliptic Curves: Number Theory and Cryptography, 2nd ed., Chapman & Hall/CRC, 2008, §12.3
  3. J. H. Silverman, The Arithmetic of Elliptic Curves, 2nd ed., Graduate Texts in Mathematics 106, Springer, 2009

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

Source file: Definitions/Def_WeierstrassCurve_VeluBundledMap.lean

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_WeierstrassCurve_VeluPointMap

open Polynomial

namespace WeierstrassCurve

section Field

variable {F : Type*} [Field F] (W : WeierstrassCurve F)

private lemma veluY_summand_negY (x y : F) (Q : F × F) :
    W.veluU Q.1 Q.2 * (2 * W.toAffine.negY x y + W.a₁ * x + W.a₃) / (x - Q.1) ^ 3
      + W.veluT Q.1 Q.2 * (W.a₁ * (x - Q.1) + W.toAffine.negY x y - Q.2) / (x - Q.1) ^ 2
      + (W.a₁ * W.veluU Q.1 Q.2 - W.veluGx Q.1 Q.2 * W.veluGy Q.1 Q.2) / (x - Q.1) ^ 2
    = W.a₁ * (W.veluT Q.1 Q.2 / (x - Q.1) + W.veluU Q.1 Q.2 / (x - Q.1) ^ 2)
      - (W.veluU Q.1 Q.2 * (2 * y + W.a₁ * x + W.a₃) / (x - Q.1) ^ 3
        + W.veluT Q.1 Q.2 * (W.a₁ * (x - Q.1) + y - Q.2) / (x - Q.1) ^ 2
        + (W.a₁ * W.veluU Q.1 Q.2 - W.veluGx Q.1 Q.2 * W.veluGy Q.1 Q.2) / (x - Q.1) ^ 2) := by
  rcases eq_or_ne x Q.1 with h | h
  · simp [h, sub_self]
  · have hd : x - Q.1 ≠ 0 := sub_ne_zero.mpr h
    simp only [veluT, veluU, veluGx, veluGy, Affine.negY]
    field_simp
    ring

lemma veluY_negY (S : Finset (F × F)) (x y : F) :
    W.veluY S x (W.toAffine.negY x y)
      = (W.veluQuotient S).toAffine.negY (W.veluX S x) (W.veluY S x y) := by
  simp only [veluY, veluX]
  rw [Finset.sum_congr rfl fun Q _ => W.veluY_summand_negY x y Q,
    Finset.sum_sub_distrib, ← Finset.mul_sum]
  simp only [Affine.negY, veluQuotient_a₁, veluQuotient_a₃]
  ring

variable {W} in

theorem velu_singleton_map_nonsingular {x₀ y₀ x y : F}
    (hP : W.toAffine.Equation x y) (hQ : W.toAffine.Equation x₀ y₀)
    (hΨ : (W.Ψ₃).eval x₀ = 0) (hx : x ≠ x₀)
    (hΔ : (W.veluQuotient {(x₀, y₀)}).Δ ≠ 0) :
    (W.veluQuotient {(x₀, y₀)}).toAffine.Nonsingular
      (W.veluX {(x₀, y₀)} x) (W.veluY {(x₀, y₀)} x y) :=
  ((W.veluQuotient {(x₀, y₀)}).toAffine.equation_iff_nonsingular_of_Δ_ne_zero hΔ).mp
    (W.velu_singleton_map_equation hP hQ hΨ hx)

private lemma some_congr {W' : Affine F} {x y₁ y₂ : F} {h₁ : W'.Nonsingular x y₁}
    {h₂ : W'.Nonsingular x y₂} (hy : y₁ = y₂) :
    Affine.Point.some x y₁ h₁ = Affine.Point.some x y₂ h₂ := by
  subst hy; rfl

variable {W} in
open scoped Classical in

noncomputable def veluPointMap3 {x₀ y₀ : F} (hQ : W.toAffine.Equation x₀ y₀)
    (hΨ : (W.Ψ₃).eval x₀ = 0) (hΔ : (W.veluQuotient {(x₀, y₀)}).Δ ≠ 0) :
    W.toAffine.Point → (W.veluQuotient {(x₀, y₀)}).toAffine.Point
  | .zero => .zero
  | .some x y h =>
    if hx : x = x₀ then .zero
    else .some _ _ (velu_singleton_map_nonsingular h.1 hQ hΨ hx hΔ)

variable {W}
variable {x₀ y₀ : F} (hQ : W.toAffine.Equation x₀ y₀) (hΨ : (W.Ψ₃).eval x₀ = 0)
  (hΔ : (W.veluQuotient {(x₀, y₀)}).Δ ≠ 0)

@[simp] lemma veluPointMap3_zero : veluPointMap3 hQ hΨ hΔ .zero = .zero := rfl

lemma veluPointMap3_some_of_eq {x y : F} (h : W.toAffine.Nonsingular x y) (hx : x = x₀) :
    veluPointMap3 hQ hΨ hΔ (.some x y h) = .zero := by
  simp only [veluPointMap3]
  exact dif_pos hx

lemma veluPointMap3_some_of_ne {x y : F} (h : W.toAffine.Nonsingular x y) (hx : x ≠ x₀) :
    veluPointMap3 hQ hΨ hΔ (.some x y h)
      = .some _ _ (velu_singleton_map_nonsingular h.1 hQ hΨ hx hΔ) := by
  simp only [veluPointMap3]
  exact dif_neg hx

lemma veluPointMap3_neg (P : W.toAffine.Point) :
    veluPointMap3 hQ hΨ hΔ (-P) = -(veluPointMap3 hQ hΨ hΔ P) := by
  cases P with
  | zero => rfl
  | some x y h =>
    rw [Affine.Point.neg_some]
    by_cases hx : x = x₀
    · rw [veluPointMap3_some_of_eq hQ hΨ hΔ _ hx, veluPointMap3_some_of_eq hQ hΨ hΔ h hx]
      rfl
    · rw [veluPointMap3_some_of_ne hQ hΨ hΔ _ hx, veluPointMap3_some_of_ne hQ hΨ hΔ h hx,
        Affine.Point.neg_some]
      exact some_congr (W.veluY_negY {(x₀, y₀)} x y)

end Field

end WeierstrassCurve

Statements phrased using this module (0)

No statement module imports it directly (it is used through other definition modules or by proofs).