Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_WeierstrassCurve_OddOrderSummingSet.lean

definition module

Coordinate extraction and Vélu summing sets for Weierstrass curves

Two definitions are made, both in the WeierstrassCurve namespace and both stated for an arbitrary Weierstrass curve rather than for a curve known to be elliptic.

First, for a commutative ring R and an affine Weierstrass curve W over R, WeierstrassCurve.Affine.Point.coordsOrZero is the total map W.\mathrm{Point} \to R \times R defined by cases on the inductive type of points: the point at infinity is sent to the pair (0,0), and a point Point.some x y h (an affine point with nonsingularity witness h) is sent to (x,y). Thus it extracts affine coordinates, with (0,0) as a junk value at infinity; in particular it is not injective in general, since it cannot distinguish infinity from an affine point with coordinates (0,0). The two accompanying lemmas coordsOrZero_zero and coordsOrZero_some record these two defining equations.

Second, for a field F with decidable equality and W a Weierstrass curve over F, WeierstrassCurve.oddOrderSummingSet W Q n, for a point Q of the affine curve W.\mathrm{toAffine} and n : \mathbb{N}, is the finite subset of F \times F obtained as the image of the interval Finset.Icc 1 n under k \mapsto (k \bullet Q).\mathrm{coordsOrZero}, where k \bullet Q is the \mathbb{N}-multiple of Q in the group of points. So it is the set of coordinate pairs of Q, 2Q, \dots, nQ. Nothing in the definition requires that Q have order 2n+1, or that the multiples kQ be affine: if some kQ is the point at infinity, the pair (0,0) enters the set. The name records the intended use, where Q has exact odd order 2n+1 and the set is a half-system S with \langle Q\rangle\setminus\{O\} = S \sqcup (-S). The lemma mem_oddOrderSummingSet restates membership: P lies in the set iff there is k with 1 \le k \le n and (k \bullet Q).\mathrm{coordsOrZero} = P.

Relation to Mathlib

Builds on Mathlib's WeierstrassCurve, WeierstrassCurve.Affine.Point and the group structure on points; Mathlib has no coordinate-extraction map with a junk value at infinity and no Vélu-style summing set, so both definitions here are the project's own.

Where it is used

The summing set is the format in which the data of a cyclic kernel is presented to the Vélu-type quotient constructions used in the isogeny part of the development; the module is imported very widely in the tree.

References

  1. J. Vélu, Isogénies entre courbes elliptiques, Comptes Rendus de l'Académie des Sciences de Paris, Série 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_OddOrderSummingSet.lean

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib

namespace WeierstrassCurve

namespace Affine.Point

variable {R : Type*} [CommRing R] {W : Affine R}

def coordsOrZero : W.Point → R × R
  | .zero => (0, 0)
  | .some x y _ => (x, y)

@[simp] lemma coordsOrZero_zero : ((.zero : W.Point)).coordsOrZero = (0, 0) := rfl

@[simp] lemma coordsOrZero_some {x y : R} (h : W.Nonsingular x y) :
    (Point.some x y h).coordsOrZero = (x, y) := rfl

end Affine.Point

section SummingSet

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

def oddOrderSummingSet (Q : W.toAffine.Point) (n : ℕ) : Finset (F × F) :=
  (Finset.Icc 1 n).image fun k => (k • Q).coordsOrZero

lemma mem_oddOrderSummingSet {Q : W.toAffine.Point} {n : ℕ} {P : F × F} :
    P ∈ W.oddOrderSummingSet Q n ↔ ∃ k, 1 ≤ k ∧ k ≤ n ∧ (k • Q).coordsOrZero = P := by
  simp only [oddOrderSummingSet, Finset.mem_image, Finset.mem_Icc]
  exact ⟨fun ⟨k, ⟨h1, h2⟩, h3⟩ => ⟨k, h1, h2, h3⟩, fun ⟨k, h1, h2, h3⟩ => ⟨k, ⟨h1, h2⟩, h3⟩⟩

end SummingSet

end WeierstrassCurve

Statements phrased using this module (69)