Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_HeckeGalois_EichlerShimura.lean

definition module

Hecke polynomial algebra, mod-π”ͺ Galois action, Eichler–Shimura hypotheses

The ambient ring is HeckeAlg, defined as the polynomial ring \mathbb{Z}[X_\ell] over the type of primes (MvPolynomial Nat.Primes β„€), with heckeGen β„“ the variable indexed by \ell; it is thus a free presentation on symbols T_\ell, carrying no Hecke relations, and adjoin_range_heckeGen records that the generators generate it. For a system of eigenvalues a : \mathrm{Primes} \to k in a commutative ring k, eigenIdeal a is the kernel of the \mathbb{Z}-algebra map sending T_\ell \mapsto a_\ell; eisensteinSystem N is the system a_\ell = 1 for \ell \mid N and a_\ell = 1+\ell otherwise, and eisensteinIdeal N is its eigen-ideal. For a HeckeAlg-module J and an ideal \mathfrak m, heckeTorsion J π”ͺ is J[\mathfrak m] = \{x : t\cdot x = 0 \text{ for all } t \in \mathfrak m\} (Mathlib's torsionBySet), needing no group action; when a group G acts distributively on J commuting with HeckeAlg, smul_mem_heckeTorsion shows J[\mathfrak m] is G-stable and mTorsionGaloisRep is the resulting monoid homomorphism G \to \mathrm{End}_{\mathrm{HeckeAlg}/\mathfrak m}(J[\mathfrak m]). eisensteinKernel J I is the ideal of t for which some i \in I makes (1+i)t annihilate all of J, and EisensteinQuotientInvariantsFinite asserts that the image in J/\gamma_I J of \{x : \sigma x - x \in \gamma_I J \text{ for all } \sigma\} is finite.

The local clauses are stated for a field extension L/K, integers N,p, and J with commuting actions of \mathrm{Gal}(L/K) = L \simeq_{\mathrm{alg}[K]} L and HeckeAlg, quantified over primes \ell \nmid Np and valuation subrings A \subseteq L with \ell a non-unit of A: UnramifiedOutside says inertia at A fixes every p-power-torsion element of J; FrobeniusQuadratic says \sigma^2 x - T_\ell\cdot(\sigma x) + \ell x = 0 for each arithmetic Frobenius \sigma at A (acting as x \mapsto x^\ell on the residue field) and each p-power-torsion x; DetFrobeniusMod π”ͺ says \det(\mathrm{mTorsionGaloisRep}\,\sigma) = \ell in \mathrm{HeckeAlg}/\mathfrak m. MTorsionNeBot says J[\mathfrak m] \neq 0, EigenformSupport p J IsEig requires this for every \mathfrak m satisfying the parameter predicate IsEig with p \in \mathfrak m, and MultiplicityOneData is the three-field structure '\mathfrak m maximal, p \in \mathfrak m, \dim_{\mathrm{HeckeAlg}/\mathfrak m} J[\mathfrak m] = 2'. EichlerShimuraDataReduced bundles the first two local clauses with EigenformSupport (not the determinant clause). Finally IsSpecialization p J J' A β„“ sp F is a four-field structure on an additive map sp : J \to J' and an endomorphism F of J': sp commutes with all Hecke operators, kills the inertia action (sp(\sigma x) = sp(x) for \sigma in inertia at A), intertwines Frobenius at A with F, and is injective on p-power torsion; SpecialFibreRelation asserts F^2 - T_\ell F + \ell = 0 on J', and SpecializationExists asserts such data exist for every prime \ell \nmid Np and every A over \ell. All of these are predicates on an abstract module and acquire their intended content only upon instantiation.

Relation to Mathlib

HeckeAlg is literally Mathlib's MvPolynomial Nat.Primes β„€ and heckeTorsion an abbreviation for Submodule.torsionBySet; Mathlib has no Hecke algebra, Eichler–Shimura relation or Eisenstein ideal, so those notions are the project's own. The valuation-theoretic vocabulary used in the local clauses (LiesOverPrime, inertiaSubgroupIn, IsFrobeniusAt) is defined in the project on top of Mathlib's valuation subrings and ramification groups.

Where it is used

These are the hypothesis interfaces through which the modular-curve input enters the Frey–Serre–Ribet route: instantiated with the p-power torsion of J_0(N) and the Galois group of an algebraic closure of \mathbb{Q}, the Eichler–Shimura clauses give the mod-\mathfrak m representations attached to eigenforms together with their local behaviour at primes of good reduction, the multiplicity-one datum gives two-dimensionality, and the Eisenstein-kernel finiteness clause is the form in which Mazur's Eisenstein-ideal argument is invoked.

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. B. Mazur, Modular curves and the Eisenstein ideal, Publications MathΓ©matiques de l'IHΓ‰S 47 (1977), 33–186
  3. K. A. Ribet, On modular representations of \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}) arising from modular forms, Inventiones Mathematicae 100 (1990), 431–476

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

Imports

Imported by

Declarations

Source

import Definitions.Def_FLTPrelim_Ramification
import Definitions.Def_EllipticCurve_FrobeniusTrace
import Mathlib.Algebra.MvPolynomial.CommRing β†—
import Mathlib.Algebra.Module.Torsion.Basic β†—
import Mathlib.LinearAlgebra.Determinant β†—
import Mathlib.LinearAlgebra.Dimension.Finrank β†—

set_option autoImplicit false

noncomputable section

namespace ModularCurve

abbrev HeckeAlg : Type := MvPolynomial Nat.Primes β„€

def heckeGen (β„“ : Nat.Primes) : HeckeAlg := MvPolynomial.X β„“

@[simp] lemma aeval_heckeGen {A : Type*} [CommSemiring A] [Algebra β„€ A]
    (a : Nat.Primes β†’ A) (β„“ : Nat.Primes) :
    MvPolynomial.aeval a (heckeGen β„“) = a β„“ :=
  MvPolynomial.aeval_X a β„“

lemma adjoin_range_heckeGen : Algebra.adjoin β„€ (Set.range heckeGen) = ⊀ :=
  MvPolynomial.adjoin_range_X

section EigenIdeal

variable {k : Type*} [CommRing k]

def eigenIdeal (a : Nat.Primes β†’ k) : Ideal HeckeAlg :=
  RingHom.ker (MvPolynomial.aeval (R := β„€) a)

lemma mem_eigenIdeal_iff (a : Nat.Primes β†’ k) (t : HeckeAlg) :
    t ∈ eigenIdeal a ↔ MvPolynomial.aeval a t = 0 :=
  RingHom.mem_ker

lemma heckeGen_sub_mem_eigenIdeal (a : Nat.Primes β†’ k) (β„“ : Nat.Primes) (b : β„€)
    (hb : algebraMap β„€ k b = a β„“) :
    heckeGen β„“ - MvPolynomial.C b ∈ eigenIdeal a := by
  rw [mem_eigenIdeal_iff, map_sub, aeval_heckeGen, MvPolynomial.aeval_C, hb, sub_self]

end EigenIdeal

section Divisorial

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

abbrev heckeTorsion (π”ͺ : Ideal HeckeAlg) : Submodule HeckeAlg J :=
  Submodule.torsionBySet HeckeAlg J (π”ͺ : Set HeckeAlg)

lemma mem_heckeTorsion_iff (π”ͺ : Ideal HeckeAlg) (x : J) :
    x ∈ heckeTorsion J π”ͺ ↔ βˆ€ t ∈ π”ͺ, t β€’ x = 0 := by
  rw [Submodule.mem_torsionBySet_iff]
  exact ⟨fun h t ht => h ⟨t, ht⟩, fun h t => h t.1 t.2⟩

theorem smul_mem_heckeTorsion {π”ͺ : Ideal HeckeAlg} (g : G) {x : J}
    (hx : x ∈ heckeTorsion J π”ͺ) : g β€’ x ∈ heckeTorsion J π”ͺ := by
  rw [Submodule.mem_torsionBySet_iff] at hx ⊒
  intro t
  rw [← smul_comm g (t : HeckeAlg) x, hx t, smul_zero]

def mTorsionGaloisRep (π”ͺ : Ideal HeckeAlg) :
    G β†’* Module.End (HeckeAlg β§Έ π”ͺ) (heckeTorsion J π”ͺ) where
  toFun g :=
    { toFun := fun x => ⟨g β€’ (x : J), smul_mem_heckeTorsion J g x.2⟩
      map_add' := fun x y => by
        ext
        simp [smul_add]
      map_smul' := fun r x => by
        obtain ⟨a, rfl⟩ := Ideal.Quotient.mk_surjective r
        ext
        simp only [Submodule.torsionBySet.mk_smul, RingHom.id_apply, Submodule.coe_smul]
        exact smul_comm g a (x : J) }
  map_one' := by
    ext x
    simp
  map_mul' g h := by
    ext x
    simp [mul_smul]

@[simp] theorem coe_mTorsionGaloisRep_apply (π”ͺ : Ideal HeckeAlg) (g : G)
    (x : heckeTorsion J π”ͺ) :
    ((mTorsionGaloisRep J π”ͺ g x : heckeTorsion J π”ͺ) : J) = g β€’ (x : J) := rfl

def eisensteinKernel (I : Ideal HeckeAlg) : Ideal HeckeAlg where
  carrier := {t | βˆƒ i ∈ I, βˆ€ x : J, ((1 + i) * t) β€’ x = 0}
  zero_mem' := ⟨0, I.zero_mem, fun x => by simp⟩
  add_mem' := by
    rintro t t' ⟨i, hi, ht⟩ ⟨i', hi', ht'⟩
    refine ⟨i + i' + i * i', I.add_mem (I.add_mem hi hi') (I.mul_mem_left i hi'), fun x => ?_⟩
    have h1 : ((1 + i') * ((1 + i) * t)) β€’ x = 0 := by rw [mul_smul, ht x, smul_zero]
    have h2 : ((1 + i) * ((1 + i') * t')) β€’ x = 0 := by rw [mul_smul, ht' x, smul_zero]
    have : (1 + (i + i' + i * i')) * (t + t')
        = (1 + i') * ((1 + i) * t) + (1 + i) * ((1 + i') * t') := by
      ring
    rw [this, add_smul, h1, h2, add_zero]
  smul_mem' := by
    rintro c t ⟨i, hi, ht⟩
    refine ⟨i, hi, fun x => ?_⟩
    have : (1 + i) * (c β€’ t) = c * ((1 + i) * t) := by rw [smul_eq_mul]; ring
    rw [this, mul_smul, ht x, smul_zero]

def EisensteinQuotientInvariantsFinite (I : Ideal HeckeAlg) : Prop :=
  Set.Finite ((eisensteinKernel J I β€’ (⊀ : Submodule HeckeAlg J)).mkQ ''
    {x : J | βˆ€ Οƒ : G, Οƒ β€’ x - x ∈ eisensteinKernel J I β€’ (⊀ : Submodule HeckeAlg J)})

end Divisorial

section Forms

variable (𝕋 : Type*) [CommRing 𝕋] (J : Type*) [AddCommGroup J] [Module 𝕋 J] (π”ͺ : Ideal 𝕋)

def MTorsionNeBot : Prop :=
  Submodule.torsionBySet 𝕋 J π”ͺ β‰  βŠ₯

end Forms

section LocalClauses

variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable (N p : β„•) (J : Type*) [AddCommGroup J] [Module HeckeAlg J]
  [DistribMulAction (L ≃ₐ[K] L) J] [SMulCommClass (L ≃ₐ[K] L) HeckeAlg J]

def UnramifiedOutside : Prop :=
  βˆ€ β„“ : β„•, β„“.Prime β†’ Β¬ β„“ ∣ N * p β†’
    βˆ€ A : ValuationSubring L, A.LiesOverPrime β„“ β†’
      βˆ€ Οƒ ∈ A.inertiaSubgroupIn K, βˆ€ x : J, (βˆƒ n : β„•, p ^ n β€’ x = 0) β†’ Οƒ β€’ x = x

def FrobeniusQuadratic : Prop :=
  βˆ€ β„“ : β„•, (hβ„“ : β„“.Prime) β†’ Β¬ β„“ ∣ N * p β†’
    βˆ€ A : ValuationSubring L, A.LiesOverPrime β„“ β†’
      βˆ€ Οƒ : L ≃ₐ[K] L, A.IsFrobeniusAt Οƒ β„“ β†’
        βˆ€ x : J, (βˆƒ n : β„•, p ^ n β€’ x = 0) β†’
          Οƒ β€’ Οƒ β€’ x - heckeGen βŸ¨β„“, hβ„“βŸ© β€’ (Οƒ β€’ x) + β„“ β€’ x = 0

def DetFrobeniusMod (π”ͺ : Ideal HeckeAlg) : Prop :=
  βˆ€ β„“ : β„•, β„“.Prime β†’ Β¬ β„“ ∣ N * p β†’
    βˆ€ A : ValuationSubring L, A.LiesOverPrime β„“ β†’
      βˆ€ Οƒ : L ≃ₐ[K] L, A.IsFrobeniusAt Οƒ β„“ β†’
        LinearMap.det (mTorsionGaloisRep J π”ͺ Οƒ) = ((β„“ : HeckeAlg β§Έ π”ͺ))

end LocalClauses

section MultiplicityOne

variable (p : β„•) (J : Type*) [AddCommGroup J] [Module HeckeAlg J]

structure MultiplicityOneData (π”ͺ : Ideal HeckeAlg) : Prop where
  isMaximal : π”ͺ.IsMaximal
  resChar : (p : HeckeAlg) ∈ π”ͺ
  finrank_two : Module.finrank (HeckeAlg β§Έ π”ͺ) (heckeTorsion J π”ͺ) = 2

end MultiplicityOne

def eisensteinSystem (N : β„•) : Nat.Primes β†’ β„€ :=
  fun β„“ => if (β„“ : β„•) ∣ N then 1 else 1 + (β„“ : β„•)

@[simp] lemma eisensteinSystem_of_not_dvd {N : β„•} {β„“ : Nat.Primes} (h : Β¬ (β„“ : β„•) ∣ N) :
    eisensteinSystem N β„“ = 1 + (β„“ : β„•) := if_neg h

@[simp] lemma eisensteinSystem_of_dvd {N : β„•} {β„“ : Nat.Primes} (h : (β„“ : β„•) ∣ N) :
    eisensteinSystem N β„“ = 1 := if_pos h

def eisensteinIdeal (N : β„•) : Ideal HeckeAlg :=
  eigenIdeal (eisensteinSystem N)

section Support

variable (p : β„•) (J : Type*) [AddCommGroup J] [Module HeckeAlg J]

def EigenformSupport (IsEig : Ideal HeckeAlg β†’ Prop) : Prop :=
  βˆ€ π”ͺ : Ideal HeckeAlg, IsEig π”ͺ β†’ ((p : HeckeAlg)) ∈ π”ͺ β†’ MTorsionNeBot HeckeAlg J π”ͺ

end Support

section Bundle

variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable (N p : β„•) (J : Type*) [AddCommGroup J] [Module HeckeAlg J]
  [DistribMulAction (L ≃ₐ[K] L) J] [SMulCommClass (L ≃ₐ[K] L) HeckeAlg J]

structure EichlerShimuraDataReduced (IsEig : Ideal HeckeAlg β†’ Prop) : Prop where
  unramifiedOutside : UnramifiedOutside (K := K) (L := L) N p J
  frobeniusQuadratic : FrobeniusQuadratic (K := K) (L := L) N p J
  eigenformSupport : EigenformSupport p J IsEig

end Bundle

section Datum

variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable (p : β„•) (J : Type*) [AddCommGroup J] [Module HeckeAlg J]
  [DistribMulAction (L ≃ₐ[K] L) J] [SMulCommClass (L ≃ₐ[K] L) HeckeAlg J]
variable (J' : Type*) [AddCommGroup J'] [Module HeckeAlg J']

structure IsSpecialization (A : ValuationSubring L) (β„“ : β„•) (sp : J β†’+ J') (F : J' β†’+ J') :
    Prop where

  hecke_comm : βˆ€ (T : HeckeAlg) (x : J), sp (T β€’ x) = T β€’ sp x

  inertia_comm : βˆ€ Οƒ ∈ A.inertiaSubgroupIn K, βˆ€ x : J, sp (Οƒ β€’ x) = sp x

  frobenius_comm : βˆ€ Οƒ : L ≃ₐ[K] L, A.IsFrobeniusAt Οƒ β„“ β†’ βˆ€ x : J, sp (Οƒ β€’ x) = F (sp x)

  injective_torsion : βˆ€ x : J, (βˆƒ n : β„•, p ^ n β€’ x = 0) β†’ sp x = 0 β†’ x = 0

def SpecialFibreRelation (β„“ : β„•) (hβ„“ : β„“.Prime) (F : J' β†’+ J') : Prop :=
  βˆ€ y : J', F (F y) - heckeGen βŸ¨β„“, hβ„“βŸ© β€’ F y + β„“ β€’ y = 0

end Datum

section Citation

variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable (N p : β„•) (J : Type*) [AddCommGroup J] [Module HeckeAlg J]
  [DistribMulAction (L ≃ₐ[K] L) J] [SMulCommClass (L ≃ₐ[K] L) HeckeAlg J]

def SpecializationExists : Prop :=
  βˆ€ β„“ : β„•, (hβ„“ : β„“.Prime) β†’ Β¬ β„“ ∣ N * p β†’
    βˆ€ A : ValuationSubring L, A.LiesOverPrime β„“ β†’
      βˆƒ (J' : Type) (_ : AddCommGroup J') (_ : Module HeckeAlg J') (sp : J β†’+ J')
        (F : J' β†’+ J'),
        IsSpecialization (K := K) p J J' A β„“ sp F ∧ SpecialFibreRelation J' β„“ hβ„“ F

end Citation

end ModularCurve

Statements phrased using this module (83)