Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_WeierstrassCurve_FullKernelQuotient.lean

definition module

Vélu quotient by the full kernel of a point

Let W be a Weierstrass curve over a field F and Q a point of the associated affine curve. For N : \mathbb{N}, WeierstrassCurve.fullKernelQuotient W Q N is the Weierstrass curve obtained from W by veluQuotientOfSums applied to the two sums taken over the finite set oddOrderSummingSet W Q (N - 1) — the set of coordinate pairs (x,y) of the multiples Q, 2Q, \dots, (N-1)Q, each pair occurring once, with the point at infinity recorded as (0,0): the first sum is \sum_P g_x(x_P,y_P) and the second is \sum_P\bigl(x_P g_x(x_P,y_P) - y_P g_y(x_P,y_P)\bigr), where g_x(x,y) = 3x^2 + 2a_2x + a_4 - a_1y and g_y(x,y) = -(2y + a_1x + a_3). Thus a_1,a_2,a_3 are unchanged while a_4 and a_6 are decreased by 5t and by b_2 t + 7w for those two sums t,w; the construction is a curve in a fixed Weierstrass presentation, not an isogeny.

The arithmetic content is the identification of this one-sided sum with Vélu's symmetric one. Two polynomial identities show that g_x(x,y) + g_x(x, -y-a_1x-a_3) equals t_P = 2g_x - a_1g_y and that the corresponding pair of asymmetric weights sums to w_P = g_y^2 + x\,t_P. When Q has exact additive order 2n+1, the set of pairs for Q,\dots,2nQ is the disjoint union of the pairs for Q,\dots,nQ and their images under (x,y) \mapsto (x, -y-a_1x-a_3), whence the two sums equal veluTSum and veluWSum of the half-system, and \mathrm{fullKernelQuotient}(W,Q,2n+1) = \mathrm{veluQuotient}(W, S_n(Q)). Supplementary cases: for N = 1 the sums are empty and the value is W; for N = 2 at a nonsingular point (x,y) with g_y(x,y) = 0 the value is the order-two quotient veluQuotient2 W x y.

Relation to Mathlib

Mathlib supplies WeierstrassCurve and its affine points; the Vélu data (veluGx, veluGy, veluT, veluW, veluTSum, veluWSum, veluQuotient, veluQuotient2), the coordinate map coordsOrZero and the summing sets are the project's own definitions.

Where it is used

These constructions give an explicit Weierstrass model for the quotient of a curve by the cyclic subgroup generated by a torsion point, indexed either by a half-system of multiples or by the whole punctured kernel, and so provide the explicit isogenous curves used in the elliptic-curve part of the argument.

References

  1. J. Vélu, Isogénies entre courbes elliptiques, C. R. Acad. Sci. Paris Sér. A-B 273 (1971), 238–241
  2. J. H. Silverman, The Arithmetic of Elliptic Curves, 2nd edition, 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_FullKernelQuotient.lean

Imports

Imported by

Declarations

Source

import Definitions.Def_WeierstrassCurve_OddOrderSummingSet
import Definitions.Def_WeierstrassCurve_VeluQuotientOfSums
import Definitions.Def_WeierstrassCurve_VeluOrderTwo

set_option autoImplicit false

namespace WeierstrassCurve

def fullKernelQuotient {F : Type*} [Field F] [DecidableEq F] (W : WeierstrassCurve F)
    (Q : W.toAffine.Point) (N : ℕ) : WeierstrassCurve F :=
  W.veluQuotientOfSums
    (∑ P ∈ W.oddOrderSummingSet Q (N - 1), W.veluGx P.1 P.2)
    (∑ P ∈ W.oddOrderSummingSet Q (N - 1),
      (P.1 * W.veluGx P.1 P.2 - P.2 * W.veluGy P.1 P.2))

theorem veluGx_add_veluGx_negY {R : Type*} [CommRing R] (W : WeierstrassCurve R) (x y : R) :
    W.veluGx x y + W.veluGx x (W.toAffine.negY x y) = W.veluT x y := by
  simp only [veluGx, veluGy, veluT, Affine.negY]
  ring

theorem asymWeight_add_asymWeight_negY {R : Type*} [CommRing R] (W : WeierstrassCurve R) (x y : R) :
    (x * W.veluGx x y - y * W.veluGy x y) +
        (x * W.veluGx x (W.toAffine.negY x y) -
          W.toAffine.negY x y * W.veluGy x (W.toAffine.negY x y)) =
      W.veluW x y := by
  simp only [veluGx, veluGy, veluT, veluW, veluU, Affine.negY]
  ring

theorem coordsOrZero_neg {R : Type*} [CommRing R] {W : WeierstrassCurve R} (P : W.toAffine.Point)
    (hP : P ≠ 0) :
    (-P).coordsOrZero = (P.coordsOrZero.1, W.toAffine.negY P.coordsOrZero.1 P.coordsOrZero.2) := by
  rcases P with _ | ⟨x, y, h⟩
  · exact absurd rfl hP
  · rfl

theorem eq_of_coordsOrZero_eq {R : Type*} [CommRing R] {W : WeierstrassCurve R} {P P' : W.toAffine.Point}
    (hP : P ≠ 0) (hP' : P' ≠ 0) (h : P.coordsOrZero = P'.coordsOrZero) : P = P' := by
  rcases P with _ | ⟨x, y, hx⟩
  · exact absurd rfl hP
  rcases P' with _ | ⟨x', y', hx'⟩
  · exact absurd rfl hP'
  simp only [Affine.Point.coordsOrZero_some, Prod.mk.injEq] at h
  obtain ⟨rfl, rfl⟩ := h
  rfl

theorem negPair_injective {R : Type*} [CommRing R] (W : WeierstrassCurve R) :
    Function.Injective (fun P : R × R => (P.1, W.toAffine.negY P.1 P.2)) := by
  intro P P' h
  simp only [Prod.mk.injEq] at h
  obtain ⟨h1, h2⟩ := h
  have h3 := congrArg (W.toAffine.negY P.1) h2
  rw [Affine.negY_negY, h1, Affine.negY_negY] at h3
  exact Prod.ext h1 h3

theorem oddOrderSummingSet_two_mul {F : Type*} [Field F] [DecidableEq F] (W : WeierstrassCurve F)
    (Q : W.toAffine.Point) (n : ℕ) (hQ : addOrderOf Q = 2 * n + 1) :
    W.oddOrderSummingSet Q (2 * n) =
      W.oddOrderSummingSet Q n ∪
        (W.oddOrderSummingSet Q n).image (fun P => (P.1, W.toAffine.negY P.1 P.2)) := by
  have hrefl : ∀ k, 1 ≤ k → k ≤ 2 * n → (2 * n + 1 - k) • Q = -(k • Q) := fun k hk1 hk2 => by
    refine eq_neg_of_add_eq_zero_left ?_
    rw [← add_nsmul, Nat.sub_add_cancel (by omega), ← hQ, addOrderOf_nsmul_eq_zero]
  have hne : ∀ k, 1 ≤ k → k ≤ 2 * n → k • Q ≠ 0 := fun k hk1 hk2 =>
    nsmul_ne_zero_of_lt_addOrderOf (by omega) (by rw [hQ]; omega)
  ext P
  simp only [Finset.mem_union, Finset.mem_image, mem_oddOrderSummingSet]
  constructor
  · rintro ⟨k, hk1, hk2, rfl⟩
    by_cases hkn : k ≤ n
    · exact Or.inl ⟨k, hk1, hkn, rfl⟩
    · refine Or.inr ⟨((2 * n + 1 - k) • Q).coordsOrZero, ⟨2 * n + 1 - k, by omega, by omega, rfl⟩, ?_⟩
      rw [hrefl k hk1 hk2, coordsOrZero_neg _ (hne k hk1 hk2), Affine.negY_negY]
  · rintro (⟨k, hk1, hk2, rfl⟩ | ⟨P', ⟨k, hk1, hk2, rfl⟩, rfl⟩)
    · exact ⟨k, hk1, by omega, rfl⟩
    · refine ⟨2 * n + 1 - k, by omega, by omega, ?_⟩
      rw [hrefl k hk1 (by omega), coordsOrZero_neg _ (hne k hk1 (by omega))]

theorem disjoint_oddOrderSummingSet_image_neg {F : Type*} [Field F] [DecidableEq F] (W : WeierstrassCurve F)
    (Q : W.toAffine.Point) (n : ℕ) (hQ : addOrderOf Q = 2 * n + 1) :
    Disjoint (W.oddOrderSummingSet Q n)
      ((W.oddOrderSummingSet Q n).image (fun P => (P.1, W.toAffine.negY P.1 P.2))) := by
  have hne : ∀ k, 1 ≤ k → k ≤ n → k • Q ≠ 0 := fun k hk1 hk2 =>
    nsmul_ne_zero_of_lt_addOrderOf (by omega) (by rw [hQ]; omega)
  rw [Finset.disjoint_left]
  rintro P hP hP'
  rw [mem_oddOrderSummingSet] at hP
  simp only [Finset.mem_image, mem_oddOrderSummingSet] at hP'
  obtain ⟨k, hk1, hk2, rfl⟩ := hP
  obtain ⟨P', ⟨l, hl1, hl2, rfl⟩, h⟩ := hP'
  rw [← coordsOrZero_neg _ (hne l hl1 hl2)] at h
  have hkl : -(l • Q) = k • Q := eq_of_coordsOrZero_eq (neg_ne_zero.mpr (hne l hl1 hl2)) (hne k hk1 hk2) h
  have h0 : (k + l) • Q = 0 := by rw [add_nsmul, ← hkl, neg_add_cancel]
  have hdvd : addOrderOf Q ∣ k + l := addOrderOf_dvd_iff_nsmul_eq_zero.mpr h0
  rw [hQ] at hdvd
  exact absurd (Nat.le_of_dvd (by omega) hdvd) (by omega)

theorem sum_oddOrderSummingSet_two_mul {F : Type*} [Field F] [DecidableEq F] (W : WeierstrassCurve F)
    (Q : W.toAffine.Point) (n : ℕ) (hQ : addOrderOf Q = 2 * n + 1) (f : F × F → F) :
    ∑ P ∈ W.oddOrderSummingSet Q (2 * n), f P =
      ∑ P ∈ W.oddOrderSummingSet Q n, (f P + f (P.1, W.toAffine.negY P.1 P.2)) := by
  rw [oddOrderSummingSet_two_mul W Q n hQ, Finset.sum_union (disjoint_oddOrderSummingSet_image_neg W Q n hQ),
    Finset.sum_image (fun P _ P' _ h => negPair_injective W h), Finset.sum_add_distrib]

theorem sum_veluGx_oddOrderSummingSet_two_mul {F : Type*} [Field F] [DecidableEq F] (W : WeierstrassCurve F)
    (Q : W.toAffine.Point) (n : ℕ) (hQ : addOrderOf Q = 2 * n + 1) :
    ∑ P ∈ W.oddOrderSummingSet Q (2 * n), W.veluGx P.1 P.2 = W.veluTSum (W.oddOrderSummingSet Q n) := by
  rw [sum_oddOrderSummingSet_two_mul W Q n hQ (fun P => W.veluGx P.1 P.2), veluTSum]
  exact Finset.sum_congr rfl fun P _ => veluGx_add_veluGx_negY W P.1 P.2

theorem sum_asymWeight_oddOrderSummingSet_two_mul {F : Type*} [Field F] [DecidableEq F]
    (W : WeierstrassCurve F) (Q : W.toAffine.Point) (n : ℕ) (hQ : addOrderOf Q = 2 * n + 1) :
    ∑ P ∈ W.oddOrderSummingSet Q (2 * n), (P.1 * W.veluGx P.1 P.2 - P.2 * W.veluGy P.1 P.2) =
      W.veluWSum (W.oddOrderSummingSet Q n) := by
  rw [sum_oddOrderSummingSet_two_mul W Q n hQ (fun P => P.1 * W.veluGx P.1 P.2 - P.2 * W.veluGy P.1 P.2),
    veluWSum]
  exact Finset.sum_congr rfl fun P _ => asymWeight_add_asymWeight_negY W P.1 P.2

theorem fullKernelQuotient_eq_veluQuotient_oddOrderSummingSet {F : Type*} [Field F] [DecidableEq F]
    (W : WeierstrassCurve F) (Q : W.toAffine.Point) (n : ℕ) (hQ : addOrderOf Q = 2 * n + 1) :
    W.fullKernelQuotient Q (2 * n + 1) = W.veluQuotient (W.oddOrderSummingSet Q n) := by
  rw [fullKernelQuotient, Nat.add_sub_cancel, sum_veluGx_oddOrderSummingSet_two_mul W Q n hQ,
    sum_asymWeight_oddOrderSummingSet_two_mul W Q n hQ]
  exact (W.veluQuotient_eq_veluQuotientOfSums _).symm

theorem fullKernelQuotient_one {F : Type*} [Field F] [DecidableEq F] (W : WeierstrassCurve F)
    (Q : W.toAffine.Point) : W.fullKernelQuotient Q 1 = W := by
  have h : W.oddOrderSummingSet Q (1 - 1) = ∅ := by
    simp [oddOrderSummingSet]
  rw [fullKernelQuotient, h, Finset.sum_empty, Finset.sum_empty]
  ext <;> simp [veluQuotientOfSums]

theorem fullKernelQuotient_two {F : Type*} [Field F] [DecidableEq F] (W : WeierstrassCurve F) {x y : F}
    (h : W.toAffine.Nonsingular x y) (hgy : W.veluGy x y = 0) :
    W.fullKernelQuotient (.some x y h) 2 = W.veluQuotient2 x y := by
  have hS : W.oddOrderSummingSet (.some x y h) (2 - 1) = {(x, y)} := by
    simp [oddOrderSummingSet]
  rw [fullKernelQuotient, hS]
  simp only [Finset.sum_singleton]
  rw [hgy, mul_zero, sub_zero]
  rfl

end WeierstrassCurve

Statements phrased using this module (31)