Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_MTorsionDiff.lean

definition module

m-torsion submodule of regular differentials via q-expansions

Throughout, K is a field of characteristic p (with p prime), N \ge 1, and F_N = modularFunctionFieldC K N is the intermediate field K(\tilde\jmath,\tilde\jmath_N) of K((q)) generated by the two q-series \tilde\jmath and its N-fold q-substitute.

The first definition, qExpGens, packages a family of K-linear endomorphisms of K((q)) indexed by Option ι: at none it is the operator U_p of LaurentSeries.heckeU, which sends a Laurent series f to the series with coefficients n \mapsto a_{pn}(f); at some i it is LaurentSeries.heckeT K (ℓ i) _ 2, that is U_{\ell_i} + \ell_i \cdot V_{\ell_i} with V_\ell the coefficient-spreading operator n \mapsto a_{n/\ell} for \ell \mid n and 0 otherwise — the weight-two normalisation, the exponent k-1 being 1. Two auxiliary lemmas record the two values of this family.

For an arbitrary commuting family F of K-linear endomorphisms of K((q)) indexed by a type \sigma (a structure carrying the operators together with a proof that they pairwise commute) and a tuple \bar\theta : \sigma \to K of scalars, mTorsionDiffOf is the intersection, inside \Omega_{F_N/K}, of the submodule regularDifferentials K F_N — the differentials that at every place v of F_N/K are of the form f \cdot dv with f in the valuation ring of v — with the preimage, under the q-expansion map on differentials qExpansionDiffAlong attached to the inclusion F_N \hookrightarrow K((q)), of the submodule F.\mathrm{annPart}\,p\,\bar\theta. The membership criterion mem_mTorsionDiffOf_iff unfolds the latter: \omega lies in mTorsionDiffOf exactly when \omega is regular and, for every Q \in \mathbb{F}_p[X_\sigma] whose image in K[X_\sigma] vanishes at \bar\theta, the operator Q(F.T) kills the q-expansion of \omega.

Finally mTorsionDiff specialises this to the family qExpGens — given the commutation hypothesis hcomm as an argument — and mem_mTorsionDiff_iff restates its membership criterion.

Relation to Mathlib

Mathlib has no notion of the \mathfrak m-torsion part of the regular differentials of a modular function field; the commuting-family structure Module.End.CommFamily, its polynomial evaluation and annihilated part, the formal Hecke operators on Laurent series, the module of regular differentials and the q-expansion map on differentials are all project definitions, built on Mathlib's Module.End, MvPolynomial, LaurentSeries and KaehlerDifferential.

Where it is used

This submodule is the mod-p analogue of the space of weight-two cusp forms cut out by a maximal ideal of the Hecke algebra: all conditions are imposed on q-expansions, where U_p records both the Cartier operator and the Frobenius, and T_\ell = U_\ell + \ell V_\ell records the Hecke correspondence. It serves as the home of the mod-p eigenform attached to a Galois representation in the level-lowering step of the Frey–Serre–Ribet argument.

References

  1. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154, §1
  2. F. Diamond and J. Shurman, A First Course in Modular Forms, Graduate Texts in Mathematics 228, Springer, 2005

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_Module_CommFamilyAnnPart
import Definitions.Def_LaurentSeries_HeckeU
import Definitions.Def_LaurentSeries_HeckeV
import Definitions.Def_ModularCurve_QExpansionDiff
import Definitions.Def_ModularCurve_JqCoeff
import Definitions.Def_AlgebraicCurve_RegularDifferentials

set_option autoImplicit false
set_option synthInstance.maxHeartbeats 400000
set_option maxHeartbeats 800000

namespace ModularCurve

open AlgebraicCurve

noncomputable def qExpGens (K : Type*) [Field K] (p : ℕ) [Fact p.Prime] {ι : Type*}
    (ℓ : ι → ℕ) (hℓ : ∀ i, 0 < ℓ i) : Option ι → Module.End K (LaurentSeries K)
  | none => LaurentSeries.heckeU K p (Fact.out : p.Prime).pos
  | some i => LaurentSeries.heckeT K (ℓ i) (hℓ i) 2

@[simp] theorem qExpGens_none (K : Type*) [Field K] (p : ℕ) [Fact p.Prime] {ι : Type*}
    (ℓ : ι → ℕ) (hℓ : ∀ i, 0 < ℓ i) :
    qExpGens K p ℓ hℓ none = LaurentSeries.heckeU K p (Fact.out : p.Prime).pos := rfl

@[simp] theorem qExpGens_some (K : Type*) [Field K] (p : ℕ) [Fact p.Prime] {ι : Type*}
    (ℓ : ι → ℕ) (hℓ : ∀ i, 0 < ℓ i) (i : ι) :
    qExpGens K p ℓ hℓ (some i) = LaurentSeries.heckeT K (ℓ i) (hℓ i) 2 := rfl

noncomputable def mTorsionDiffOf (K : Type*) [Field K] (p : ℕ) [Fact p.Prime] [CharP K p]
    (N : ℕ) [NeZero N] {σ : Type*} (F : Module.End.CommFamily K (LaurentSeries K) σ)
    (θbar : σ → K) : Submodule K (Ω[↥(modularFunctionFieldC K N)⁄K]) :=
  regularDifferentials K (modularFunctionFieldC K N) ⊓
    (F.annPart p θbar).comap (qExpansionDiffAlong (modularFunctionFieldC K N).val)

theorem mem_mTorsionDiffOf_iff (K : Type*) [Field K] (p : ℕ) [Fact p.Prime] [CharP K p]
    (N : ℕ) [NeZero N] {σ : Type*} (F : Module.End.CommFamily K (LaurentSeries K) σ)
    (θbar : σ → K) (ω : Ω[↥(modularFunctionFieldC K N)⁄K]) :
    ω ∈ mTorsionDiffOf K p N F θbar ↔
      ω ∈ regularDifferentials K (modularFunctionFieldC K N) ∧
        ∀ Q : MvPolynomial σ (ZMod p),
          MvPolynomial.aeval θbar (MvPolynomial.map (ZMod.castHom (dvd_refl p) K) Q) = 0 →
            F.eval (MvPolynomial.map (ZMod.castHom (dvd_refl p) K) Q)
              (qExpansionDiffAlong (modularFunctionFieldC K N).val ω) = 0 := by
  rw [mTorsionDiffOf, Submodule.mem_inf, Submodule.mem_comap, Module.End.CommFamily.mem_annPart_iff]

noncomputable def mTorsionDiff (K : Type*) [Field K] (p : ℕ) [Fact p.Prime] [CharP K p]
    (N : ℕ) [NeZero N] {ι : Type*} (ℓ : ι → ℕ) (hℓ : ∀ i, 0 < ℓ i)
    (hcomm : ∀ a b : Option ι, Commute (qExpGens K p ℓ hℓ a) (qExpGens K p ℓ hℓ b))
    (θbar : Option ι → K) : Submodule K (Ω[↥(modularFunctionFieldC K N)⁄K]) :=
  mTorsionDiffOf K p N (Module.End.CommFamily.mk (qExpGens K p ℓ hℓ) hcomm) θbar

theorem mem_mTorsionDiff_iff (K : Type*) [Field K] (p : ℕ) [Fact p.Prime] [CharP K p]
    (N : ℕ) [NeZero N] {ι : Type*} (ℓ : ι → ℕ) (hℓ : ∀ i, 0 < ℓ i)
    (hcomm : ∀ a b : Option ι, Commute (qExpGens K p ℓ hℓ a) (qExpGens K p ℓ hℓ b))
    (θbar : Option ι → K) (ω : Ω[↥(modularFunctionFieldC K N)⁄K]) :
    ω ∈ mTorsionDiff K p N ℓ hℓ hcomm θbar ↔
      ω ∈ regularDifferentials K (modularFunctionFieldC K N) ∧
        ∀ Q : MvPolynomial (Option ι) (ZMod p),
          MvPolynomial.aeval θbar (MvPolynomial.map (ZMod.castHom (dvd_refl p) K) Q) = 0 →
            (Module.End.CommFamily.mk (qExpGens K p ℓ hℓ) hcomm).eval
                (MvPolynomial.map (ZMod.castHom (dvd_refl p) K) Q)
              (qExpansionDiffAlong (modularFunctionFieldC K N).val ω) = 0 := by
  rw [mTorsionDiff, mem_mTorsionDiffOf_iff]

end ModularCurve

Statements phrased using this module (2)