Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_EllipticCurve_PointReduction.lean

definition module

Reduction of coordinates and points on a minimal Weierstrass curve

Throughout, R is a discrete valuation ring that is a domain, K is a field equipped with an R-algebra structure making it the fraction field of R, and \mathrm{ResidueField}\,R denotes the residue field of R.

WeierstrassCurve.reduceCoord R x, for x \in K, is defined by cases: if some r \in R has r \mapsto x under the structure map R \to K, the value is the residue class of such an r in the residue field; otherwise the value is 0. Since R \to K is injective, the residue class does not depend on the element chosen, so on R-integral elements this is the composite R \to \mathrm{ResidueField}\,R transported along R \cong (integral elements of K), while non-integral x receive the junk value 0.

WeierstrassCurve.reducePoint_alt takes a Weierstrass curve W over K together with an instance of Mathlib's minimality predicate W.IsMinimal R, and produces a function from the points of the associated affine curve W to the points of the affine curve attached to the reduced curve W.reduction R over the residue field. It is defined by cases on the point: the point at infinity goes to the point at infinity; an affine point (x,y) (carrying its nonsingularity witness on W) goes to (\bar x, \bar y) = (reduceCoord R x, reduceCoord R y) provided two conditions hold, namely that both valuations v(x), v(y) \le 1 for the valuation of K attached to the maximal ideal of R (that is, both coordinates are integral) and that the pair (\bar x, \bar y) is a nonsingular point of the reduced curve; in every remaining case, the value is the point at infinity. Thus points with a non-integral coordinate, and pairs whose reduction is singular, are sent to the point at infinity by fiat. This is a bare function on points: no additivity, kernel or injectivity statement is part of the definition.

Relation to Mathlib

Mathlib supplies the minimality predicate WeierstrassCurve.IsMinimal, the reduced curve WeierstrassCurve.reduction, and the group of affine points WeierstrassCurve.Affine.Point; the reduction map on points, and the partial section reduceCoord of the residue map used to define it, are the project's own.

Where it is used

These definitions provide the reduction map E(K) \to \tilde E(k) at a discrete valuation, in the form used in the modules of the tree that study torsion and its reduction for elliptic curves over local and global fields.

References

  1. J. H. Silverman, The Arithmetic of Elliptic Curves, Graduate Texts in Mathematics 106, Springer, 2nd ed., 2009, Ch. VII §2

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

Declarations

Source

import Mathlib.AlgebraicGeometry.EllipticCurve.Reduction ↗
import Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point ↗

set_option autoImplicit false

noncomputable section

namespace WeierstrassCurve

open IsDiscreteValuationRing IsLocalRing IsDedekindDomain.HeightOneSpectrum

variable (R : Type*) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
  {K : Type*} [Field K] [Algebra R K] [IsFractionRing R K]

open Classical in

def reduceCoord (x : K) : ResidueField R :=
  if h : ∃ r : R, algebraMap R K r = x then residue R h.choose else 0

open Classical in

def reducePoint_alt (W : WeierstrassCurve K) [W.IsMinimal R] :
    W.toAffine.Point → (W.reduction R).toAffine.Point
  | .zero => .zero
  | .some x y _ =>
    if _ : valuation K (maximalIdeal R) x ≤ 1 ∧ valuation K (maximalIdeal R) y ≤ 1 then
      if h' : (W.reduction R).toAffine.Nonsingular (reduceCoord R x) (reduceCoord R y)
        then .some _ _ h'
      else .zero
    else .zero

end WeierstrassCurve

end

Statements phrased using this module (6)