Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_WeierstrassCurve_VeluQuotientMap.lean

definition module

Odd Vélu summing sets, Vélu's -map, quotient discriminant

The standing setting is a Weierstrass curve W over a commutative ring R, with the auxiliary quantities g_x(x,y)=3x^2+2a_2x+a_4-a_1y, g_y(x,y)=-(2y+a_1x+a_3), t(x,y)=2g_x-a_1g_y (equivalently 6x^2+b_2x+b_4), u(x,y)=g_y^2 and w(x,y)=u+xt, and with T(S)=\sum_{P\in S}t(P), W(S)=\sum_{P\in S}w(P) for a finite set S of pairs; the Vélu quotient curve veluQuotient has the same a_1,a_2,a_3 and a_4-5T(S), a_6-b_2T(S)-7W(S).

The structure IsOddVeluSet is a predicate on a finite set S\subseteq R\times R with three fields: every P\in S satisfies the affine Weierstrass equation of W; g_y(P)\neq 0 for every P\in S (so no point of S is fixed by y\mapsto -y-a_1x-a_3); and the first-coordinate map is injective on S, in the form that P,P'\in S with equal x-coordinates are equal. It implies the weaker predicate IsVeluSet, which asks only for the equation; the empty set and, given a point satisfying the equation with g_y\neq0, the singleton containing it are examples. A further lemma records that replacing y by \mathrm{negY}(x,y) in a singleton leaves the quotient curve unchanged, since t and w are invariant under that involution.

Over a field F, veluX is the rational function x\mapsto x+\sum_{Q\in S}\bigl(t(Q)/(x-x_Q)+u(Q)/(x-x_Q)^2\bigr), taken with Lean's convention that division by zero vanishes; it reduces to the identity for S=\varnothing, and for x distinct from all x_Q it equals x+\sum_Q\bigl(t(Q)(x-x_Q)+u(Q)\bigr)/(x-x_Q)^2. Finally, veluQuotient_Δ expresses the discriminant of the quotient curve as \Delta(W) plus an explicit twelve-term polynomial in b_2,b_4,b_6, T(S) and W(S).

Relation to Mathlib

Mathlib supplies the WeierstrassCurve structure, its b- and \Delta-invariants, the affine equation, Affine.negY and the division polynomial \Psi_2^2; the Vélu data (g_x, g_y, t, u, w, their sums, the quotient curve, and the summing-set predicates) are the project's own, Mathlib having no Vélu construction.

Where it is used

These definitions belong to the project's treatment of isogenies by Vélu's formulas: IsOddVeluSet isolates the summing sets arising from kernels with no 2-torsion, veluX is the x-coordinate of the induced map to the quotient curve, and the discriminant formula controls how \Delta changes under the quotient. They are imported throughout the isogeny development built on top of this module.

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, Chapter III

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_VeluQuotientMap.lean

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_WeierstrassCurve_Velu

open Polynomial

namespace WeierstrassCurve

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

structure IsOddVeluSet (S : Finset (R × R)) : Prop where

  equation : ∀ P ∈ S, W.toAffine.Equation P.1 P.2

  gy_ne_zero : ∀ P ∈ S, W.veluGy P.1 P.2 ≠ 0

  x_injOn : ∀ P ∈ S, ∀ P' ∈ S, P.1 = P'.1 → P = P'

lemma IsOddVeluSet.isVeluSet {S : Finset (R × R)} (h : W.IsOddVeluSet S) : W.IsVeluSet S :=
  ⟨h.equation⟩

lemma isOddVeluSet_empty : W.IsOddVeluSet ∅ where
  equation := by simp
  gy_ne_zero := by simp
  x_injOn := by simp

lemma isOddVeluSet_singleton {x y : R} (h : W.toAffine.Equation x y)
    (h2 : W.veluGy x y ≠ 0) : W.IsOddVeluSet {(x, y)} where
  equation := by simpa using h
  gy_ne_zero := by simpa using h2
  x_injOn := by simp

lemma veluQuotient_singleton_negY (x y : R) :
    W.veluQuotient {(x, W.toAffine.negY x y)} = W.veluQuotient {(x, y)} := by
  have ht : W.veluTSum {(x, W.toAffine.negY x y)} = W.veluTSum {(x, y)} := by
    simp only [veluTSum, Finset.sum_singleton]
    exact W.veluT_negY x y
  have hw : W.veluWSum {(x, W.toAffine.negY x y)} = W.veluWSum {(x, y)} := by
    simp only [veluWSum, Finset.sum_singleton]
    exact W.veluW_negY x y
  ext <;> simp only [veluQuotient_a₁, veluQuotient_a₂, veluQuotient_a₃, veluQuotient_a₄,
    veluQuotient_a₆, ht, hw]

section QuotientMap

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

noncomputable def veluX (S : Finset (F × F)) (x : F) : F :=
  x + ∑ Q ∈ S, (W.veluT Q.1 Q.2 / (x - Q.1) + W.veluU Q.1 Q.2 / (x - Q.1) ^ 2)

@[simp] lemma veluX_empty (x : F) : W.veluX ∅ x = x := by simp [veluX]

lemma veluX_def_of_ne (S : Finset (F × F)) {x : F} (hx : ∀ Q ∈ S, x ≠ Q.1) :
    W.veluX S x = x + ∑ Q ∈ S, (W.veluT Q.1 Q.2 * (x - Q.1) + W.veluU Q.1 Q.2)
      / (x - Q.1) ^ 2 := by
  unfold veluX
  congr 1
  refine Finset.sum_congr rfl fun Q hQ => ?_
  have h0 : x - Q.1 ≠ 0 := sub_ne_zero.mpr (hx Q hQ)
  field_simp

end QuotientMap

lemma veluQuotient_Δ (S : Finset (R × R)) :
    (W.veluQuotient S).Δ = W.Δ +
      (W.b₂ ^ 4 * W.veluTSum S + 7 * W.b₂ ^ 3 * W.veluWSum S
        - 41 * W.b₂ ^ 2 * W.b₄ * W.veluTSum S - 47 * W.b₂ ^ 2 * W.veluTSum S ^ 2
        - 252 * W.b₂ * W.b₄ * W.veluWSum S + 126 * W.b₂ * W.b₆ * W.veluTSum S
        - 3528 * W.b₂ * W.veluTSum S * W.veluWSum S + 240 * W.b₄ ^ 2 * W.veluTSum S
        - 2400 * W.b₄ * W.veluTSum S ^ 2 + 1512 * W.b₆ * W.veluWSum S
        + 8000 * W.veluTSum S ^ 3 - 21168 * W.veluWSum S ^ 2) := by
  simp only [Δ, veluQuotient_b₂, veluQuotient_b₄, veluQuotient_b₆, veluQuotient_b₈]
  ring

end WeierstrassCurve

Statements phrased using this module (21)