Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_SupersingularModuli.lean

definition module

Supersingular -invariants and the supersingular locus

For a natural number p and a field K, ssJSet p K is defined to be the set of those j \in K with the property that for every Weierstrass curve W over K which is elliptic and satisfies W.j = j, every point P of the group W.toAffine.Point of K-rational points of the affine model with p \cdot P = 0 is the point at infinity. Thus membership is a statement about all elliptic Weierstrass models over K with the given j-invariant simultaneously, and it asserts only the vanishing of the p-torsion among K-rational points; in particular j lies in the set vacuously if no elliptic Weierstrass curve over K has that j-invariant, and over a field that is not algebraically closed the set is in general only an upper bound for the classical set of supersingular j-invariants (over an algebraically closed field of characteristic p the condition is Deuring's criterion E[p] = 0). Since the defining condition depends on j alone and quantifies over all models, it transfers to moduli points: for x a point of ModuliPoint N K — the quotient of the type of \Gamma_0(N)-pairs (an elliptic Weierstrass curve over K together with a rational point of exact additive order N) by the relation generated by a Weierstrass variable change followed by replacement of the marked point by a multiple k with k coprime to N — the predicate ModuliPoint.IsSupersingular p x is defined as x.j \in ssJSet p K, where x.j is the j-invariant of any representative, and ssLocus p N K is the set of moduli points satisfying it. The remaining three results record these definitions as equivalences: membership in ssJSet p K, membership in ssLocus p N K in terms of x.j, and, for a point presented by a pair P, supersingularity as membership of P.toCurve.j in ssJSet p K.

Relation to Mathlib

Mathlib has no predicate of supersingularity for elliptic curves and no moduli points for \Gamma_0(N); both are the project's own, formulated on top of Mathlib's WeierstrassCurve, its IsElliptic class, its j-invariant and its group of affine rational points.

Where it is used

The supersingular locus of a \Gamma_0(N)-moduli space is the object whose finiteness and cardinality are needed in the analysis of modular curves at a prime p of bad reduction, which underlies the level-lowering step of the route to Fermat's Last Theorem. Statements about its members are to be made over an algebraically closed field, or with the member pinned by an explicit condition such as j^{p^2} = j.

References

  1. J. H. Silverman, The Arithmetic of Elliptic Curves, 2nd edition, Graduate Texts in Mathematics 106, Springer, 2009, Chapter V
  2. N. M. Katz and B. Mazur, Arithmetic Moduli of Elliptic Curves, Annals of Mathematics Studies 108, Princeton University Press, 1985

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

Imports

Imported by

Declarations

Source

import Definitions.Def_ModularCurve_ModuliPoint

set_option autoImplicit false

namespace ModularCurve

def ssJSet (p : ℕ) (K : Type*) [Field K] [DecidableEq K] : Set K :=
  {j | ∀ (W : WeierstrassCurve K) [W.IsElliptic], W.j = j →
    ∀ P : W.toAffine.Point, p • P = 0 → P = 0}

theorem mem_ssJSet_iff {p : ℕ} {K : Type*} [Field K] [DecidableEq K] {j : K} :
    j ∈ ssJSet p K ↔ ∀ (W : WeierstrassCurve K) [W.IsElliptic], W.j = j →
      ∀ P : W.toAffine.Point, p • P = 0 → P = 0 :=
  Iff.rfl

def ModuliPoint.IsSupersingular (p : ℕ) {N : ℕ} {K : Type*} [Field K] [DecidableEq K]
    (x : ModuliPoint N K) : Prop :=
  x.j ∈ ssJSet p K

def ssLocus (p N : ℕ) (K : Type*) [Field K] [DecidableEq K] : Set (ModuliPoint N K) :=
  {x | x.IsSupersingular p}

theorem mem_ssLocus_iff {p N : ℕ} {K : Type*} [Field K] [DecidableEq K]
    {x : ModuliPoint N K} :
    x ∈ ssLocus p N K ↔ x.j ∈ ssJSet p K :=
  Iff.rfl

theorem isSupersingular_mk_iff {p N : ℕ} {K : Type*} [Field K] [DecidableEq K]
    {P : Gamma0Pair N K} :
    ModuliPoint.IsSupersingular p (Quot.mk _ P : ModuliPoint N K) ↔
      P.toCurve.j ∈ ssJSet p K :=
  Iff.rfl

end ModularCurve

Statements phrased using this module (1,020)

… and 870 more statements (search for the module name to find them).