Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_ToricDichotomyData.lean

definition module

Guarded toric dichotomy data for Hecke modules

Throughout, G is a group, J an abelian group carrying a module structure over the project's Hecke ring HeckeAlg (a polynomial ring with generators heckeGen β„“ indexed by the primes, integer constants being written C) and a distributive G-action, J_0 a second HeckeAlg-module, S a finite set of primes, I \le G, \varphi \in G and q a prime; the two actions on J are not assumed to commute. The first definition, IsToricDichotomyQGuarded q S I 𝒯 Jβ‚€, is a predicate on a HeckeAlg-submodule \mathcal T \subseteq J: for every maximal ideal \mathfrak m \subset HeckeAlg that is not eventually Eisenstein (i.e. for which no cofinite set of primes \ell has T_\ell - (\ell+1) \in \mathfrak m) and whose residue field receives q as a unit, and for every x in the project's \mathfrak m-torsion heckeTorsion J π”ͺ fixed by all \sigma \in I, either x \in \mathcal T, or HasLowerLevelTorsion S π”ͺ Jβ‚€ holds, i.e. there is a nonzero y \in J_0 killed by every natural number lying in \mathfrak m and by every T_\ell - b (\ell \notin S, b \in \mathbb Z) that lies in \mathfrak m. Note that the second alternative is a statement about J_0 alone, independent of x and of \mathfrak m-freeness of x.

The second definition, ExistsToricDichotomyDataQGuarded J q S I Ο† Jβ‚€, asserts the existence of a HeckeAlg-submodule \mathcal T \subseteq J satisfying three conditions: ToricFrobeniusSq, that \varphi acts on \mathcal T with \varphi^2 x = q^2 x; the guarded dichotomy above towards J_0; and ToricFrobeniusHecke, that \varphi x = (q\,T_q)\,x for x \in \mathcal T. The remaining declarations are accessors: toric extracts a witness submodule via choice, and toricFrobeniusSq, toricDichotomy, toricFrobeniusHecke record its three defining properties.

Relation to Mathlib

Mathlib has no notion of Hecke-module toric part, Eisenstein maximal ideal or level-raising dichotomy; these are the project's own definitions, stated for an arbitrary module over the project's ring HeckeAlg with a compatible group action.

Where it is used

These predicates package what is needed from the Deligne–Rapoport description of the special fibre of J_0(Nq) at q in the form used by Mazur's principle: in the intended application J is the Jacobian of X_0(Nq) over \overline{\mathbb Q}, J_0 that of X_0(N), I an inertia group at a place above q and \varphi a corresponding Frobenius, and the dichotomy says that an unramified non-Eisenstein \mathfrak m-torsion point is toric unless \mathfrak m-torsion already exists at level N. They are consumed by the Mazur-principle core and by the Frey-package descent apparatus used for level lowering at a prime q.

References

  1. K. A. Ribet, On modular representations of \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}) arising from modular forms, Inventiones Mathematicae 100 (1990), 431–476, Β§3
  2. P. Deligne and M. Rapoport, Les schΓ©mas de modules de courbes elliptiques, in: Modular Functions of One Variable II, Lecture Notes in Mathematics 349, Springer, 1973, 143–316
  3. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_ToricDescentData

set_option autoImplicit false

noncomputable section

namespace ModularCurve

section Dichotomy

variable {G : Type*} [Group G]
  {J : Type*} [AddCommGroup J] [Module HeckeAlg J] [DistribMulAction G J]

def IsToricDichotomyQGuarded (q : β„•) (S : Finset Nat.Primes) (I : Subgroup G)
    (𝒯 : Submodule HeckeAlg J) (Jβ‚€ : Type*) [AddCommGroup Jβ‚€] [Module HeckeAlg Jβ‚€] : Prop :=
  βˆ€ π”ͺ : Ideal HeckeAlg, π”ͺ.IsMaximal β†’ Β¬ IsEventuallyEisenstein π”ͺ β†’
    IsUnit ((q : β„•) : HeckeAlg β§Έ π”ͺ) β†’
    βˆ€ x ∈ heckeTorsion J π”ͺ, (βˆ€ Οƒ ∈ I, Οƒ β€’ x = x) β†’ x ∈ 𝒯 ∨ HasLowerLevelTorsion S π”ͺ Jβ‚€

end Dichotomy

section Bundle

def ExistsToricDichotomyDataQGuarded {G : Type*} [Group G]
    (J : Type*) [AddCommGroup J] [Module HeckeAlg J] [DistribMulAction G J]
    (q : Nat.Primes) (S : Finset Nat.Primes) (I : Subgroup G) (Ο† : G)
    (Jβ‚€ : Type*) [AddCommGroup Jβ‚€] [Module HeckeAlg Jβ‚€] : Prop :=
  βˆƒ 𝒯 : Submodule HeckeAlg J,
    ToricFrobeniusSq (q : β„•) Ο† 𝒯 ∧ IsToricDichotomyQGuarded (q : β„•) S I 𝒯 Jβ‚€ ∧
    ToricFrobeniusHecke q Ο† 𝒯

namespace ExistsToricDichotomyDataQGuarded

variable {G : Type*} [Group G]
  {J : Type*} [AddCommGroup J] [Module HeckeAlg J] [DistribMulAction G J]
  {q : Nat.Primes} {S : Finset Nat.Primes} {I : Subgroup G} {Ο† : G}
  {Jβ‚€ : Type*} [AddCommGroup Jβ‚€] [Module HeckeAlg Jβ‚€]

def toric (h : ExistsToricDichotomyDataQGuarded J q S I Ο† Jβ‚€) : Submodule HeckeAlg J :=
  h.choose

theorem toricFrobeniusSq (h : ExistsToricDichotomyDataQGuarded J q S I Ο† Jβ‚€) :
    ToricFrobeniusSq (q : β„•) Ο† h.toric :=
  h.choose_spec.1

theorem toricDichotomy (h : ExistsToricDichotomyDataQGuarded J q S I Ο† Jβ‚€) :
    IsToricDichotomyQGuarded (q : β„•) S I h.toric Jβ‚€ :=
  h.choose_spec.2.1

theorem toricFrobeniusHecke (h : ExistsToricDichotomyDataQGuarded J q S I Ο† Jβ‚€) :
    ToricFrobeniusHecke q Ο† h.toric :=
  h.choose_spec.2.2

end ExistsToricDichotomyDataQGuarded

end Bundle

end ModularCurve

end

Statements phrased using this module (6)