Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_IgusaFunctionFieldX1.lean

definition module

Igusa function field over from a weight-one form

Fix a field \kappa and a level M : \mathbb{N}. The structure ModularCurve.IntegralWeightOneForm packages, as data, a weight-one modular form together with an integral q-expansion whose reduction is nonzero: its fields are a form of weight 1 for the image of \Gamma_1(M) in \mathrm{GL}_2(\mathbb{R}), a power series series over \mathbb{Z}, a proof field isIntegralQExp asserting that pushing series forward along \mathbb{Z} \to \mathbb{C} gives the q-expansion (of width 1) of the form, and a proof field intSeriesC_ne_zero asserting that the Laurent series \bar p \in \kappa((q)) obtained by reducing series modulo the characteristic of \kappa (via intSeriesC) is nonzero. For such a datum w, IntegralWeightOneForm.hasseRootFn is the Laurent series \bar p^{-1} \in \kappa((q)) — the q-expansion of the ratio of a (p-1)-st root of the Hasse invariant to the given weight-one form — and hasseRootFn_ne_zero records that it is nonzero.

The Igusa function field igusaFunctionFieldX1C κ M w is then defined as the intermediate field \kappa \subseteq K_0(\bar p^{-1}) \subseteq \kappa((q)) generated over \kappa by K_0 \cup \{\bar p^{-1}\}, where K_0 = x1FunctionFieldC κ M is the field generated over \kappa by all quotients \bar p_f / \bar p_g of reductions of integral q-expansions of two modular forms of one and the same weight on \Gamma_1(M), the denominator having nonzero reduction. The two accompanying lemmas state the inclusion K_0 \le K_0(\bar p^{-1}) and the membership \bar p^{-1} \in K_0(\bar p^{-1}). Finally, for a prime p with \kappa of characteristic p, IgusaDiamondDataX1C abbreviates the general Igusa diamond datum at exponent k = -1 for this pair (K_0, \bar p^{-1}): an action of (\mathbb{Z}/p)^\times by \kappa-algebra automorphisms of K_0(\bar p^{-1}) fixing every element of K_0 and sending the generator \bar p^{-1} to b^{-1} \cdot \bar p^{-1}, the scalar being the image of b^{-1} \in (\mathbb{Z}/p)^\times in \kappa. The Kummer-generator property, the bounds on p and M, and the existence of a weight-one datum are not asserted here; they are carried as data or hypotheses elsewhere.

Relation to Mathlib

Mathlib supplies the ingredients — ModularForm for a subgroup of \mathrm{GL}_2(\mathbb{R}), qExpansion, LaurentSeries and IntermediateField.adjoin — while the notion of an integral weight-one datum, the associated generator \bar p^{-1}, and the Igusa function field and its diamond datum are the project's own.

Where it is used

This is the fine-moduli (\Gamma_1(M)) instantiation of the general construction of the function field of an Igusa curve over X_1(M)_\kappa, obtained by adjoining a (p-1)-st root of the Hasse invariant divided by a weight-one form. It underlies the study of the Igusa tower and of the diamond operators \langle b \rangle acting on it, used in the mod p analysis of modular curves in characteristic p.

References

  1. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154
  2. J. Igusa, Kroneckerian model of fields of elliptic modular functions, American Journal of Mathematics 81 (1959), 561–577
  3. B. H. Gross, A tameness criterion for Galois representations associated to modular forms (mod p), Duke Mathematical Journal 61 (1990), 445–517

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_IgusaFunctionField
import Definitions.Def_ModularCurve_X1

set_option autoImplicit false

noncomputable section

open CongruenceSubgroup
open scoped MatrixGroups

namespace ModularCurve

variable (κ : Type*) [Field κ] (M : ℕ)

structure IntegralWeightOneForm where

  form : ModularForm (Gamma1 M : Subgroup (GL (Fin 2) ℝ)) 1

  series : PowerSeries ℤ
  isIntegralQExp : IsIntegralQExp form series

  intSeriesC_ne_zero : intSeriesC κ series ≠ 0

variable {κ M}

def IntegralWeightOneForm.hasseRootFn (w : IntegralWeightOneForm κ M) : LaurentSeries κ :=
  (intSeriesC κ w.series)⁻¹

theorem IntegralWeightOneForm.hasseRootFn_ne_zero (w : IntegralWeightOneForm κ M) : w.hasseRootFn ≠ 0 :=
  inv_ne_zero w.intSeriesC_ne_zero

variable (κ M)

def igusaFunctionFieldX1C (w : IntegralWeightOneForm κ M) : IntermediateField κ (LaurentSeries κ) :=
  IgusaCover.igusaFunctionField (x1FunctionFieldC κ M) w.hasseRootFn

theorem x1FunctionFieldC_le_igusaFunctionFieldX1C (w : IntegralWeightOneForm κ M) :
    x1FunctionFieldC κ M ≤ igusaFunctionFieldX1C κ M w :=
  IgusaCover.le_igusaFunctionField _ _

theorem hasseRootFn_mem_igusaFunctionFieldX1C (w : IntegralWeightOneForm κ M) :
    w.hasseRootFn ∈ igusaFunctionFieldX1C κ M w :=
  IgusaCover.mem_igusaFunctionField _ _

abbrev IgusaDiamondDataX1C (w : IntegralWeightOneForm κ M) (p : ℕ) [Fact p.Prime] [CharP κ p] :=
  IgusaCover.IgusaDiamondData p (-1) (x1FunctionFieldC κ M) w.hasseRootFn

end ModularCurve

end

Statements phrased using this module (198)

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