Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_ModPFormFn.lean

definition module

Mod- modular forms as Laurent series; stack order

Throughout, K is a field, \bar\jmath \in K((q)) denotes the Laurent series jqModC K (the image in K((q)) of the integral q-expansion of the modular invariant j), and \theta = q\,d/dq is realised by the K-linear map thetaL, f \mapsto q\cdot f' on K((q)). The module fixes the vocabulary in which a mod-p modular form of even weight 2m is encoded as a single Laurent series: thetaJ K is \theta\bar\jmath, and qexpOfWeight K m G, for m \in \mathbb{Z} and G \in K((q)), is the product G\cdot(\theta\bar\jmath)^m, the weight-2m expansion with coefficient G.

Holomorphy is phrased as integrality inside the ambient field K((q)). For m \in \mathbb{N}, IsModPFormFn K m G is the conjunction of two conditions: G^{6}\,\bar\jmath^{\,4m}(\bar\jmath-1728)^{3m} is integral over the K-subalgebra K[\bar\jmath] generated by \bar\jmath, and G^{2}\,\bar\jmath^{\,m}(\bar\jmath-1728)^{m} is integral over K[\bar\jmath^{-1}] (here 1728 is the image of the scalar under K \to K((q))). IsModPCuspFormFn K m G keeps the first condition and replaces the second by the existence of an M \in \mathbb{N} for which G^{2M}\,\bar\jmath^{\,mM+1}(\bar\jmath-1728)^{mM} is integral over K[\bar\jmath^{-1}]: the same exponent pattern scaled by M, with one extra factor of \bar\jmath, which amounts to a strict inequality at the cusps. Both predicates are conditions on the Laurent series G alone; the level enters only through the field in which G is required to lie by the consumers of the notion.

Finally, for a level N \ge 1, an element G of the level-N modular function field modularFunctionFieldC K N and a place x of that field over K, stackOrd N m G x is the integer u_x \cdot \operatorname{ord}_x(G) + m\bigl(\operatorname{jWidth}(\bar\jmath(x)) - 1\bigr), where \bar\jmath(x) is the value x.evalAt (jGeomGen K N) of the generator \bar\jmath at x, \operatorname{jWidth}(j) is 3, 2 or 1 according as j = 0, j = 1728 or neither, and u_x is placeWidth N x, namely \operatorname{jWidth}(\bar\jmath(x)) divided (truncated natural division) by the ramification index \operatorname{ord}_x(\bar\jmath - \bar\jmath(x)) of the map to the j-line at x, truncated to \mathbb{N}. Thus u_x is 0, and the first term degenerates, at places where that index vanishes or exceeds the width, such as the poles of \bar\jmath.

Relation to Mathlib

Mathlib's modular forms are analytic objects; it has no notion of mod-p modular form, nor of the width or stack order of a place on a modular function field. These are the project's own predicates, expressed with Mathlib's LaurentSeries, Algebra.adjoin and IsIntegral.

Where it is used

These predicates give the holomorphy and cuspidality conditions for mod-p forms of weight 2m presented as functions on the j-line, and stackOrd measures the order of vanishing of such a form at an affine place of the level-N modular function field, counted on the moduli stack. They are the vocabulary in which the Hasse invariant is handled as the function (\theta\bar\jmath)^{-(p-1)/2}, with simple zeros exactly at the supersingular places, in the characteristic-\ell study of X_0(N) preceding level lowering.

References

  1. J.-P. Serre, Formes modulaires et fonctions zêta p-adiques, in: Modular Functions of One Variable III, Lecture Notes in Mathematics 350, Springer, 1973, 191–268
  2. N. M. Katz, p-adic properties of modular schemes and modular forms, in: Modular Functions of One Variable III, Lecture Notes in Mathematics 350, Springer, 1973, 69–190
  3. G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Princeton University Press, 1971

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

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_PlaceWidth
import Definitions.Def_ModularCurve_QExpansionDiff
set_option autoImplicit false

noncomputable section
open AlgebraicCurve

namespace ModularCurve

def thetaJ (K : Type*) [Field K] : LaurentSeries K := thetaL K (jqModC K)

def qexpOfWeight (K : Type*) [Field K] (m : ℤ) (G : LaurentSeries K) : LaurentSeries K :=
  G * thetaJ K ^ m

def stackOrd {K : Type*} [Field K] [DecidableEq K] (N : ℕ) [NeZero N] (m : ℤ)
    (G : ↥(modularFunctionFieldC K N)) (x : Place K (modularFunctionFieldC K N)) : ℤ :=
  (placeWidth N x : ℤ) * x.ord G + m * ((jWidth (x.evalAt (jGeomGen K N)) : ℤ) - 1)

def IsModPFormFn (K : Type*) [Field K] (m : ℕ) (G : LaurentSeries K) : Prop :=
  IsIntegral (Algebra.adjoin K ({jqModC K} : Set (LaurentSeries K)))
      (G ^ 6 * jqModC K ^ (4 * m) * (jqModC K - algebraMap K (LaurentSeries K) 1728) ^ (3 * m)) ∧
    IsIntegral (Algebra.adjoin K ({(jqModC K)⁻¹} : Set (LaurentSeries K)))
      (G ^ 2 * jqModC K ^ m * (jqModC K - algebraMap K (LaurentSeries K) 1728) ^ m)

def IsModPCuspFormFn (K : Type*) [Field K] (m : ℕ) (G : LaurentSeries K) : Prop :=
  IsIntegral (Algebra.adjoin K ({jqModC K} : Set (LaurentSeries K)))
      (G ^ 6 * jqModC K ^ (4 * m) * (jqModC K - algebraMap K (LaurentSeries K) 1728) ^ (3 * m)) ∧
    ∃ M : ℕ, IsIntegral (Algebra.adjoin K ({(jqModC K)⁻¹} : Set (LaurentSeries K)))
      (G ^ (2 * M) * jqModC K ^ (m * M + 1) * (jqModC K - algebraMap K (LaurentSeries K) 1728) ^ (m * M))

end ModularCurve

end

Statements phrased using this module (50)