Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_WeierstrassCurve_VeluQuotientOfSums.lean

definition module

Vélu quotient curve with free total parameters

Over a commutative ring R and for a Weierstrass curve W with coefficients a_1,\dots,a_6, this module introduces WeierstrassCurve.veluQuotientOfSums: given two ring elements t,w, it is the Weierstrass curve with the same a_1,a_2,a_3 as W and with a_4' = a_4 - 5t, \qquad a_6' = a_6 - b_2 t - 7w, where b_2 = a_1^2 + 4a_2 is Mathlib's invariant of W. This is the Vélu recipe for the coefficients of a quotient curve, but with the two totals t and w entering as free parameters instead of being computed from a kernel set. The five projection lemmas veluQuotientOfSums_a₁ through veluQuotientOfSums_a₆ record the five coefficients as just displayed.

The remaining two statements link this with the Finset-indexed construction WeierstrassCurve.veluQuotient of the imported module, where for a finite set S \subseteq R \times R of candidate points the totals are the sums t = \sum_{(x,y) \in S} (6x^2 + b_2 x + b_4) (the function veluT, evaluated there as 2g_x - a_1 g_y with g_x = 3x^2 + 2a_2x + a_4 - a_1y, g_y = -(2y + a_1x + a_3)) and w = \sum_{(x,y) \in S} (g_y^2 + x \cdot \text{veluT}(x,y)), these being veluTSum S and veluWSum S. The theorem veluQuotient_eq_veluQuotientOfSums states that W.veluQuotient S is W.veluQuotientOfSums (W.veluTSum S) (W.veluWSum S), and veluQuotient_eq_veluQuotientOfSums_of_sums is its variant in which hypotheses \text{veluTSum}(S) = t and \text{veluWSum}(S) = w are supplied, concluding W.veluQuotient S = W.veluQuotientOfSums t w.

Relation to Mathlib

Mathlib supplies the structure WeierstrassCurve and the invariants b_2, b_4, b_6, b_8 used here; the Vélu quotient construction, in both its Finset-indexed and its two-parameter form, is the project's own.

Where it is used

The two-parameter form is what is needed when the totals fed into the Vélu coefficient formulae are not the uniform sums over a single finite set of points, as happens for kernels containing a point of order two, and it is the form on which the variable-change behaviour of the Vélu quotient is stated. These constructions serve the explicit isogeny computations on the curves occurring in the Frey curve analysis.

References

  1. J. Vélu, Isogénies entre courbes elliptiques, C. R. Acad. Sci. Paris Sér. A–B 273 (1971), A238–A241
  2. J. H. Silverman, The Arithmetic of Elliptic Curves, Graduate Texts in Mathematics 106, Springer, 2nd ed., 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_VeluQuotientOfSums.lean

Imports

Imported by

Declarations

Source

import Definitions.Def_WeierstrassCurve_Velu

set_option autoImplicit false

namespace WeierstrassCurve

variable {R : Type*} [CommRing R] (W : WeierstrassCurve R)

def veluQuotientOfSums (t w : R) : WeierstrassCurve R where
  a₁ := W.a₁
  a₂ := W.a₂
  a₃ := W.a₃
  a₄ := W.a₄ - 5 * t
  a₆ := W.a₆ - W.b₂ * t - 7 * w

@[simp] lemma veluQuotientOfSums_a₁ (t w : R) : (W.veluQuotientOfSums t w).a₁ = W.a₁ := rfl
@[simp] lemma veluQuotientOfSums_a₂ (t w : R) : (W.veluQuotientOfSums t w).a₂ = W.a₂ := rfl
@[simp] lemma veluQuotientOfSums_a₃ (t w : R) : (W.veluQuotientOfSums t w).a₃ = W.a₃ := rfl
lemma veluQuotientOfSums_a₄ (t w : R) : (W.veluQuotientOfSums t w).a₄ = W.a₄ - 5 * t := rfl
lemma veluQuotientOfSums_a₆ (t w : R) :
    (W.veluQuotientOfSums t w).a₆ = W.a₆ - W.b₂ * t - 7 * w := rfl

theorem veluQuotient_eq_veluQuotientOfSums (S : Finset (R × R)) :
    W.veluQuotient S = W.veluQuotientOfSums (W.veluTSum S) (W.veluWSum S) := rfl

theorem veluQuotient_eq_veluQuotientOfSums_of_sums {S : Finset (R × R)} {t w : R}
    (ht : W.veluTSum S = t) (hw : W.veluWSum S = w) :
    W.veluQuotient S = W.veluQuotientOfSums t w := by
  subst ht hw; rfl

end WeierstrassCurve

Statements phrased using this module (2)