Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_SSCarrier.lean

definition module

Supersingular place index, carrier, pole orders, leading coefficients

Throughout, p is a prime, N \ge 1, and K is an algebraically closed field of characteristic p; F = \mathrm{modularFunctionFieldC}\,K\,N is the subfield of \mathrm{LaurentSeries}\,K generated over K by the q-expansions j(q) and j(q^N), with distinguished generators jGeomGen and jNGeomGen, and places of F over K are the objects of the project's structure AlgebraicCurve.Place (a proper valuation subring of F containing K whose ideals are principal), with normalised valuation ord and evaluation map evalAt into K.

SSIndex p N K hp5 k is the subtype of places x satisfying: x \in ssPlaces p N K, i.e. x is rational, both j(q) and j(q^N) lie in its valuation subring, and the value j(x) = x.\mathrm{evalAt}(j(q)) lies in ssJSet p K (those j \in K such that every elliptic Weierstrass curve over K with that j-invariant has no non-zero p-torsion point); together with the x-independent conditions 2 \le k, 2 \mid k, 5 \le p, and the divisibility \mathrm{placeWidth}_N(x) \mid k/2, where \mathrm{placeWidth}_N(x) = W(j(x))/e_j(x) is the natural-number quotient of the j-width W(j) \in \{3,2,1\} (according as j = 0, j = 1728, or otherwise) by e_j(x) = \mathrm{ord}_x\bigl(j(q) - j(x)\bigr). Thus the type is empty unless k is even and at least 2 and p \ge 5. SSCarrier is the function type \mathrm{SSIndex} \to K.

poleOrder attaches to such an x the integer (k/2)\,(W(j(x)) - 1)/\mathrm{placeWidth}_N(x) (integer division, exact here by the divisibility condition in the index type). unif x is a choice, via Classical.epsilon, of an element \pi_x \in F with \mathrm{ord}_x(\pi_x) = 1; lead x a f = x.\mathrm{evalAt}(\pi_x^{\,a} f), the value at x of \pi_x^{a} f, which for a equal to the pole order of f is a leading coefficient. Finally resFnFun p N K hp5 m G, for m \in \mathbb{N} and any G \in F, is the element of \mathrm{SSCarrier} in weight k = 2m sending x to \mathrm{lead}\,x\,(\mathrm{poleOrder}\ldots)\,G. Because \pi_x is chosen, lead and resFnFun are determined only up to a non-zero factor at each place.

Relation to Mathlib

Mathlib has no notion of the places of the modular function field K(j(q), j(q^N)), of supersingular j-invariants, or of widths of places; these rest on the project's own AlgebraicCurve.Place and the project's q-expansion model of the function field of X_0(N).

Where it is used

These types and functions form the carrier for the supersingular data attached to X_0(N) in characteristic p: functions on the supersingular places (one coordinate per place, without multiplicities), the admissible pole orders of weight-k functions at the elliptic supersingular places j = 0, 1728, and the passage from a function on X_0(N) to its leading coefficients there. They support the study of the supersingular locus of the special fibre used in the level-lowering step of the Frey–Serre–Ribet–Wiles route.

References

  1. J. H. Silverman, The Arithmetic of Elliptic Curves, Graduate Texts in Mathematics 106, Springer, 1986, Ch. III §10 and Ch. V §3
  2. M. Deuring, Die Typen der Multiplikatorenringe elliptischer Funktionenkörper, Abhandlungen aus dem Mathematischen Seminar der Universität Hamburg 14 (1941), 197–272
  3. B. Edixhoven, The weight in Serre's conjectures on modular forms, Inventiones Mathematicae 109 (1992), 563–594

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

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_PlaceWidth

set_option autoImplicit false

noncomputable section
open AlgebraicCurve ModularCurve

namespace ModularCurve

variable (p : ℕ) [Fact p.Prime] (N : ℕ) [NeZero N] (K : Type) [Field K] [CharP K p] [IsAlgClosed K] [DecidableEq K]

def SSIndex (hp5 : 5 ≤ p) (k : ℤ) : Type :=
  { x : Place K (modularFunctionFieldC K N) // x ∈ ssPlaces p N K ∧ 2 ≤ k ∧ 2 ∣ k ∧ ((placeWidth N x : ℤ) ∣ k / 2) ∧ 5 ≤ p }

abbrev SSCarrier (hp5 : 5 ≤ p) (k : ℤ) : Type := SSIndex p N K hp5 k → K

def poleOrder (hp5 : 5 ≤ p) (k : ℤ) (x : SSIndex p N K hp5 k) : ℤ :=
  (k / 2) * ((jWidth (x.1.evalAt (jGeomGen K N)) : ℤ) - 1) / (placeWidth N x.1 : ℤ)

omit [Fact p.Prime] [CharP K p] [IsAlgClosed K] [DecidableEq K] in

def unif (x : Place K (modularFunctionFieldC K N)) : modularFunctionFieldC K N :=
  Classical.epsilon (fun π : modularFunctionFieldC K N => x.ord π = 1)

omit [Fact p.Prime] [CharP K p] [IsAlgClosed K] [DecidableEq K] in

def lead (x : Place K (modularFunctionFieldC K N)) (a : ℤ) (f : modularFunctionFieldC K N) : K :=
  x.evalAt (unif N K x ^ a * f)

def resFnFun (hp5 : 5 ≤ p) (m : ℕ) (G : modularFunctionFieldC K N) : SSCarrier p N K hp5 (2 * (m : ℤ)) :=
  fun x => lead N K x.1 (poleOrder p N K hp5 (2 * (m : ℤ)) x) G

end ModularCurve

end

Statements phrased using this module (32)