Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_WeierstrassCurve_VeluOrderTwo.lean

definition module

Vélu quotient by an order-two point; quadratic cofactor discriminant

Throughout, R is a commutative ring and W a Weierstrass curve over R with coefficients a_1,a_2,a_3,a_4,a_6.

The first definition, WeierstrassCurve.veluQuotient2, attaches to a pair (x_0,y_0) of elements of R a new Weierstrass curve over R. Writing t = W.veluGx x₀ y₀ = 3x_0^2 + 2a_2x_0 + a_4 - a_1y_0 (the X-partial of the Weierstrass polynomial at (x_0,y_0), up to sign), the new curve has the same a_1,a_2,a_3 as W, and a_4' = a_4 - 5t, \qquad a_6' = a_6 - b_2 t - 7x_0 t . This is the shape of WeierstrassCurve.veluQuotient for a Vélu set, with the sums \sum \mathrm{t}_P and \sum \mathrm{w}_P replaced by the single values t and x_0 t; at a point of order two, where veluGy vanishes, this halves the uniform odd-kernel contributions \mathrm{t} = 2t and \mathrm{w} = 2x_0t, which is the convention appropriate to a self-paired kernel point. The accompanying component lemmas record the five coefficients, and veluQuotient2_b₂ records that b_2 = a_1^2 + 4a_2 is unchanged by the construction. No hypothesis relating (x_0,y_0) to W is imposed: the curve is defined for an arbitrary pair.

The second definition, WeierstrassCurve.velu2QuadDisc, is the element d(x_0) = b_2^2 - 8b_2x_0 - 48x_0^2 - 32b_4 of R, again for arbitrary x_0. The lemma velu2QuadDisc_eq_disc_cofactor rewrites it as (b_2+4x_0)^2 - 16\,(4x_0^2 + b_2x_0 + 2b_4), i.e. as the discriminant of the quadratic 4X^2 + (b_2+4x_0)X + (4x_0^2+b_2x_0+2b_4), which is the cofactor of X - x_0 in the 2-division polynomial 4X^3 + b_2X^2 + 2b_4X + b_6 when x_0 is a root of the latter. Finally, map_velu2QuadDisc states compatibility with base change: for a ring homomorphism f \colon R \to S, the invariant of W.\mathrm{map}\,f at f(x_0) is f(d(x_0)).

Relation to Mathlib

Mathlib supplies WeierstrassCurve, the invariants b_2,b_4, the 2-division polynomial and base change along a ring homomorphism; the Vélu quotient curves and the quantity velu2QuadDisc are the project's own, built on the Vélu data (veluGx, veluT, veluW, veluQuotient) of the project's Vélu module.

Where it is used

These definitions support the order-two branch of Vélu's isogeny construction, where the kernel is generated by a single affine 2-torsion point and the odd-kernel convention would count it twice. The quantity velu2QuadDisc is the invariant through which the discriminants of W and of its quotient by an order-two point are compared, as needed for the 2-isogeny arguments about Frey curves.

References

  1. J. Vélu, Isogénies entre courbes elliptiques, C. R. Acad. Sci. Paris Sér. A 273 (1971), 238–241
  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_VeluOrderTwo.lean

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_WeierstrassCurve_Velu

set_option autoImplicit false

namespace WeierstrassCurve

section CommRing

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

def veluQuotient2 (x₀ y₀ : R) : WeierstrassCurve R where
  a₁ := W.a₁
  a₂ := W.a₂
  a₃ := W.a₃
  a₄ := W.a₄ - 5 * W.veluGx x₀ y₀
  a₆ := W.a₆ - W.b₂ * W.veluGx x₀ y₀ - 7 * (x₀ * W.veluGx x₀ y₀)

variable (x₀ y₀ : R)

@[simp] lemma veluQuotient2_a₁ : (W.veluQuotient2 x₀ y₀).a₁ = W.a₁ := rfl
@[simp] lemma veluQuotient2_a₂ : (W.veluQuotient2 x₀ y₀).a₂ = W.a₂ := rfl
@[simp] lemma veluQuotient2_a₃ : (W.veluQuotient2 x₀ y₀).a₃ = W.a₃ := rfl
lemma veluQuotient2_a₄ : (W.veluQuotient2 x₀ y₀).a₄ = W.a₄ - 5 * W.veluGx x₀ y₀ := rfl
lemma veluQuotient2_a₆ :
    (W.veluQuotient2 x₀ y₀).a₆ = W.a₆ - W.b₂ * W.veluGx x₀ y₀ - 7 * (x₀ * W.veluGx x₀ y₀) :=
  rfl

lemma veluQuotient2_b₂ : (W.veluQuotient2 x₀ y₀).b₂ = W.b₂ := by
  simp [b₂]

def velu2QuadDisc (x₀ : R) : R :=
  W.b₂ ^ 2 - 8 * W.b₂ * x₀ - 48 * x₀ ^ 2 - 32 * W.b₄

lemma velu2QuadDisc_def (x₀ : R) :
    W.velu2QuadDisc x₀ = W.b₂ ^ 2 - 8 * W.b₂ * x₀ - 48 * x₀ ^ 2 - 32 * W.b₄ := rfl

lemma velu2QuadDisc_eq_disc_cofactor (x₀ : R) :
    W.velu2QuadDisc x₀
      = (W.b₂ + 4 * x₀) ^ 2 - 16 * (4 * x₀ ^ 2 + W.b₂ * x₀ + 2 * W.b₄) := by
  simp only [velu2QuadDisc]; ring

lemma map_velu2QuadDisc {S : Type*} [CommRing S] (f : R →+* S) (x₀ : R) :
    (W.map f).velu2QuadDisc (f x₀) = f (W.velu2QuadDisc x₀) := by
  simp only [velu2QuadDisc, map_b₂, map_b₄, map_sub, map_mul, map_pow, map_ofNat]

end CommRing

end WeierstrassCurve

Statements phrased using this module (18)