Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_HeckeSeam.lean

definition module

Hecke action on differentials and its comparison with

Fix N\ge 1 and write F_N^L for the base-changed modular function field laurentBaseChange L (modularFunctionFieldFull N), a subfield of the Laurent series over L, with L a field of characteristic zero containing \mathbb{Q}. For a prime \ell, heckeOmegaAlong is the L-linear endomorphism of \Omega_{F_N^L/L} obtained by pulling differentials back along the L-algebra map heckeAlphaBar from level N to level N\ell and then applying the trace map traceDiff for the F_N^L-algebra structure on F_{N\ell}^L supplied by heckeBetaBar; heckeOmegaAlongT is the same construction with the two legs interchanged. Specialising L to \overline{\mathbb{Q}} gives heckeOmegaBar and heckeOmegaBarT. The predicates HeckeOmegaPreservesBar and HeckeOmegaPreservesBarT say that these operators carry the submodule regularDiffs (the span of the differentials with non-negative order at every place) into itself; granted this, heckeOmegaRegBar (as a \mathbb{Z}-linear map) and heckeOmegaRegBarQ, heckeOmegaRegBarQT (as \overline{\mathbb{Q}}-linear maps) are the restrictions, and are set to 0 otherwise. Under the corresponding pairwise-commutation predicates the \mathbb{Z}-subalgebra generated by the family is commutative, so the abstract Hecke algebra HeckeAlg =\mathbb{Z}[X_\ell] evaluates into it; this yields the ring maps heckeEvalOmegaBar, heckeEvalOmegaBarQ, heckeEvalOmegaBarQT (the latter two totalised with a zero fallback) and a HeckeAlg-module structure heckeOmegaModuleBar on the regular differentials, again with a constant-coefficient fallback.

Two annihilator ideals of HeckeAlg are then compared: heckeKerJ, the annihilator of J_0(N)=\mathrm{Pic}^0 of the level-N function field over \overline{\mathbb{Q}} for the divisorial Hecke module, and heckeKerOmega, the annihilator of the regular differentials. A theorem identifies heckeKerJ with the kernel of heckeEvalBar when the divisorial operators commute. The Prop-valued structure HeckeSeam carries three fields as data: the two inclusions between these ideals, and, for every prime p, every n and every t:\mathrm{Fin}\,n\to HeckeAlg, the passage from \mathbb{Z}-linear independence of the classes of t modulo heckeKerJ to \mathbb{Q}_p-linear independence of their images under rationalHeckeRep on the rational p-adic Tate module of J_0(N).

The HeckeWord section provides the letter calculus used to compare the two actions. HeckeInputsAlongT asserts the existence of integrality witnesses for both legs, the principal-divisor property at level N\ell, finiteness along heckeBetaBar, the fundamental identity along heckeAlphaBar and the norm formula along heckeBetaBar. letterKey conjoins HeckeInputsAlong and HeckeInputsAlongT over \overline{\mathbb{Q}} with the two preservation predicates. Indexed by \mathrm{Primes}\sqcup\mathrm{Primes} (an operator and its transpose), letterJ gives endomorphisms of J_0(N) built from heckePic0Bar and heckePic0BarTranspose, and letterO the corresponding restrictions of heckeOmegaBar and heckeOmegaBarT, each replaced by 0 when letterKey fails. wordJ multiplies the J-letters along a word, wordO multiplies the \Omega-letters along the reversed word, wordTr reverses a word and swaps each letter's orientation, and vpEnd sends an endomorphism of J_0(N) to the induced \mathbb{Q}_p-linear endomorphism of the rational Tate module.

Relation to Mathlib

Kähler differentials \Omega_{F/K}, Laurent series, Module.annihilator and Module.End are Mathlib's; the Hecke algebra here is the project's free commutative ring MvPolynomial Nat.Primes ℤ, and the regular differentials, the trace map on differentials, the modular function field as an intermediate field of Laurent series and the Hecke action on either side are project notions with no Mathlib counterpart.

Where it is used

The two annihilator ideals and the independence clause of HeckeSeam form the interface through which the Eichler–Shimura comparison between the cotangent space of J_0(N) (regular differentials, i.e. weight-two cusp forms) and the p-adic Tate module of J_0(N) is stated, feeding the construction of the Galois representations attached to Hecke eigensystems that the level-lowering and modularity-lifting steps consume.

References

  1. G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Iwanami Shoten and Princeton University Press, 1971
  2. F. Diamond and J. Shurman, A First Course in Modular Forms, Graduate Texts in Mathematics 228, Springer, 2005
  3. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154, §1

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

Imports

Imported by

Declarations

Source

import Definitions.Def_ModularCurve_HeckeModule
import Definitions.Def_AlgebraicCurve_Differentials
import Definitions.Def_ModularCurve_QExpansionDiff
import Definitions.Def_ModularCurve_JZeroTateModule

set_option autoImplicit false

noncomputable section

namespace ModularCurve

open AlgebraicCurve

section OmegaAlong

variable (L : Type*) [Field L] [Algebra ℚ L] (N ℓ : ℕ) [NeZero N] [NeZero ℓ]

def heckeOmegaAlong :
    Ω[↥(laurentBaseChange L (modularFunctionFieldFull N))⁄L] →ₗ[L]
      Ω[↥(laurentBaseChange L (modularFunctionFieldFull N))⁄L] :=
  letI := algebraAlong (heckeBetaBar L N ℓ)
  haveI := isScalarTower_along (heckeBetaBar L N ℓ)
  haveI : SMulCommClass L ↥(laurentBaseChange L (modularFunctionFieldFull N))
      ↥(laurentBaseChange L (modularFunctionFieldFull (N * ℓ))) :=
    ⟨fun k f x => by simp only [Algebra.smul_def]; exact mul_left_comm _ _ _⟩
  ((traceDiff L ↥(laurentBaseChange L (modularFunctionFieldFull N))
      ↥(laurentBaseChange L (modularFunctionFieldFull (N * ℓ)))).restrictScalars L).comp
    (pullbackDiff (heckeAlphaBar L N ℓ))

end OmegaAlong

section OmegaModule

variable (N : ℕ) [NeZero N]

def heckeOmegaBar (ℓ : Nat.Primes) :
    Ω[↥(modularFunctionFieldBar N)⁄AlgebraicClosure ℚ] →ₗ[AlgebraicClosure ℚ]
      Ω[↥(modularFunctionFieldBar N)⁄AlgebraicClosure ℚ] :=
  haveI : NeZero (ℓ : ℕ) := ⟨ℓ.2.ne_zero⟩
  heckeOmegaAlong (AlgebraicClosure ℚ) N ℓ

def HeckeOmegaPreservesBar : Prop :=
  ∀ (ℓ : Nat.Primes) (ω : Ω[↥(modularFunctionFieldBar N)⁄AlgebraicClosure ℚ]),
    ω ∈ regularDiffs (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar N) →
      heckeOmegaBar N ℓ ω ∈ regularDiffs (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar N)

open Classical in

def heckeOmegaRegBar (ℓ : Nat.Primes) :
    Module.End ℤ ↥(regularDiffs (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar N)) :=
  if h : HeckeOmegaPreservesBar N then
    ((heckeOmegaBar N ℓ).restrict (fun ω hω => h ℓ ω hω)).toAddMonoidHom.toIntLinearMap
  else 0

def HeckeOmegaCommuteBar : Prop :=
  ∀ ℓ ℓ' : Nat.Primes,
    heckeOmegaRegBar N ℓ * heckeOmegaRegBar N ℓ' = heckeOmegaRegBar N ℓ' * heckeOmegaRegBar N ℓ

theorem isMulCommutative_adjoin_heckeOmegaRegBar (h : HeckeOmegaCommuteBar N) :
    IsMulCommutative (Algebra.adjoin ℤ (Set.range (heckeOmegaRegBar N))) :=
  Algebra.isMulCommutative_adjoin ℤ (by
    rintro _ ⟨ℓ, rfl⟩ _ ⟨ℓ', rfl⟩
    exact h ℓ ℓ')

open scoped IsMulCommutative in

def heckeEvalOmegaBarAux (h : HeckeOmegaCommuteBar N) :
    HeckeAlg →ₐ[ℤ] (Algebra.adjoin ℤ (Set.range (heckeOmegaRegBar N)) :
      Subalgebra ℤ (Module.End ℤ
        ↥(regularDiffs (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar N)))) :=
  haveI := isMulCommutative_adjoin_heckeOmegaRegBar N h
  MvPolynomial.aeval fun ℓ =>
    (⟨heckeOmegaRegBar N ℓ, Algebra.subset_adjoin (Set.mem_range_self ℓ)⟩ :
      Algebra.adjoin ℤ (Set.range (heckeOmegaRegBar N)))

def heckeEvalOmegaBar (h : HeckeOmegaCommuteBar N) :
    HeckeAlg →+* Module.End ℤ
      ↥(regularDiffs (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar N)) :=
  ((Algebra.adjoin ℤ (Set.range (heckeOmegaRegBar N))).val.comp
    (heckeEvalOmegaBarAux N h)).toRingHom

open Classical in

@[implicit_reducible]
def heckeOmegaModuleBar :
    Module HeckeAlg ↥(regularDiffs (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar N)) :=
  if h : HeckeOmegaCommuteBar N then
    Module.compHom _ (heckeEvalOmegaBar N h)
  else
    Module.compHom _ (MvPolynomial.eval₂Hom (Int.castRingHom ℤ) (0 : Nat.Primes → ℤ))

end OmegaModule

section Seam

variable (N : ℕ) [NeZero N]

def heckeKerJ : Ideal HeckeAlg :=
  letI := heckeModuleBar N
  Module.annihilator HeckeAlg (JZero N)

theorem heckeKerJ_eq_ker (h : HeckeOperatorsCommuteBar N) :
    heckeKerJ N = RingHom.ker (heckeEvalBar h) := by
  letI := heckeModuleBar N
  ext t
  rw [heckeKerJ, RingHom.mem_ker, Module.mem_annihilator]
  constructor
  · intro ht
    ext x
    simpa [heckeModuleBar_smul_def h] using ht x
  · intro ht x
    rw [heckeModuleBar_smul_def h, ht]
    rfl

def heckeKerOmega : Ideal HeckeAlg :=
  letI := heckeOmegaModuleBar N
  Module.annihilator HeckeAlg
    ↥(regularDiffs (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar N))

structure HeckeSeam : Prop where
  omega_le_J : heckeKerOmega N ≤ heckeKerJ N
  J_le_omega : heckeKerJ N ≤ heckeKerOmega N
  tate : ∀ (p : ℕ) [Fact p.Prime] (n : ℕ) (t : Fin n → HeckeAlg),
    letI := heckeModuleBar N
    LinearIndependent ℤ (Ideal.Quotient.mk (heckeKerJ N) ∘ t) →
      LinearIndependent ℚ_[p] (rationalHeckeRep p (JZero N) ∘ t)

end Seam

section OmegaAlong

variable (L : Type*) [Field L] [Algebra ℚ L] (N ℓ : ℕ) [NeZero N] [NeZero ℓ]

def heckeOmegaAlongT :
    Ω[↥(laurentBaseChange L (modularFunctionFieldFull N))⁄L] →ₗ[L]
      Ω[↥(laurentBaseChange L (modularFunctionFieldFull N))⁄L] :=
  letI := algebraAlong (heckeAlphaBar L N ℓ)
  haveI := isScalarTower_along (heckeAlphaBar L N ℓ)
  haveI : SMulCommClass L ↥(laurentBaseChange L (modularFunctionFieldFull N))
      ↥(laurentBaseChange L (modularFunctionFieldFull (N * ℓ))) :=
    ⟨fun k f x => by simp only [Algebra.smul_def]; exact mul_left_comm _ _ _⟩
  ((traceDiff L ↥(laurentBaseChange L (modularFunctionFieldFull N))
      ↥(laurentBaseChange L (modularFunctionFieldFull (N * ℓ)))).restrictScalars L).comp
    (pullbackDiff (heckeBetaBar L N ℓ))

end OmegaAlong

section OmegaModule

variable (N : ℕ) [NeZero N]

def heckeOmegaBarT (ℓ : Nat.Primes) :
    Ω[↥(modularFunctionFieldBar N)⁄AlgebraicClosure ℚ] →ₗ[AlgebraicClosure ℚ]
      Ω[↥(modularFunctionFieldBar N)⁄AlgebraicClosure ℚ] :=
  haveI : NeZero (ℓ : ℕ) := ⟨ℓ.2.ne_zero⟩
  heckeOmegaAlongT (AlgebraicClosure ℚ) N ℓ

def HeckeOmegaPreservesBarT : Prop :=
  ∀ (ℓ : Nat.Primes) (ω : Ω[↥(modularFunctionFieldBar N)⁄AlgebraicClosure ℚ]),
    ω ∈ regularDiffs (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar N) →
      heckeOmegaBarT N ℓ ω ∈ regularDiffs (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar N)

open Classical in

def heckeOmegaRegBarQ (ℓ : Nat.Primes) :
    Module.End (AlgebraicClosure ℚ)
      ↥(regularDiffs (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar N)) :=
  if h : HeckeOmegaPreservesBar N then
    (heckeOmegaBar N ℓ).restrict (fun ω hω => h ℓ ω hω)
  else 0

open Classical in

def heckeOmegaRegBarQT (ℓ : Nat.Primes) :
    Module.End (AlgebraicClosure ℚ)
      ↥(regularDiffs (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar N)) :=
  if h : HeckeOmegaPreservesBarT N then
    (heckeOmegaBarT N ℓ).restrict (fun ω hω => h ℓ ω hω)
  else 0

def HeckeOmegaCommuteBarQ : Prop :=
  ∀ ℓ ℓ' : Nat.Primes,
    heckeOmegaRegBarQ N ℓ * heckeOmegaRegBarQ N ℓ' = heckeOmegaRegBarQ N ℓ' * heckeOmegaRegBarQ N ℓ

def HeckeOmegaCommuteBarQT : Prop :=
  ∀ ℓ ℓ' : Nat.Primes,
    heckeOmegaRegBarQT N ℓ * heckeOmegaRegBarQT N ℓ' = heckeOmegaRegBarQT N ℓ' * heckeOmegaRegBarQT N ℓ

theorem isMulCommutative_adjoin_heckeOmegaRegBarQ (h : HeckeOmegaCommuteBarQ N) :
    IsMulCommutative (Algebra.adjoin ℤ (Set.range (heckeOmegaRegBarQ N))) :=
  Algebra.isMulCommutative_adjoin ℤ (by
    rintro _ ⟨ℓ, rfl⟩ _ ⟨ℓ', rfl⟩
    exact h ℓ ℓ')

theorem isMulCommutative_adjoin_heckeOmegaRegBarQT (h : HeckeOmegaCommuteBarQT N) :
    IsMulCommutative (Algebra.adjoin ℤ (Set.range (heckeOmegaRegBarQT N))) :=
  Algebra.isMulCommutative_adjoin ℤ (by
    rintro _ ⟨ℓ, rfl⟩ _ ⟨ℓ', rfl⟩
    exact h ℓ ℓ')

open scoped IsMulCommutative in

def heckeEvalOmegaBarAuxQ (h : HeckeOmegaCommuteBarQ N) :
    HeckeAlg →ₐ[ℤ] (Algebra.adjoin ℤ (Set.range (heckeOmegaRegBarQ N)) :
      Subalgebra ℤ (Module.End (AlgebraicClosure ℚ)
        ↥(regularDiffs (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar N)))) :=
  haveI := isMulCommutative_adjoin_heckeOmegaRegBarQ N h
  MvPolynomial.aeval fun ℓ =>
    (⟨heckeOmegaRegBarQ N ℓ, Algebra.subset_adjoin (Set.mem_range_self ℓ)⟩ :
      Algebra.adjoin ℤ (Set.range (heckeOmegaRegBarQ N)))

def heckeEvalOmegaBarQ (h : HeckeOmegaCommuteBarQ N) :
    HeckeAlg →+* Module.End (AlgebraicClosure ℚ)
      ↥(regularDiffs (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar N)) :=
  ((Algebra.adjoin ℤ (Set.range (heckeOmegaRegBarQ N))).val.comp
    (heckeEvalOmegaBarAuxQ N h)).toRingHom

open scoped IsMulCommutative in

def heckeEvalOmegaBarAuxQT (h : HeckeOmegaCommuteBarQT N) :
    HeckeAlg →ₐ[ℤ] (Algebra.adjoin ℤ (Set.range (heckeOmegaRegBarQT N)) :
      Subalgebra ℤ (Module.End (AlgebraicClosure ℚ)
        ↥(regularDiffs (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar N)))) :=
  haveI := isMulCommutative_adjoin_heckeOmegaRegBarQT N h
  MvPolynomial.aeval fun ℓ =>
    (⟨heckeOmegaRegBarQT N ℓ, Algebra.subset_adjoin (Set.mem_range_self ℓ)⟩ :
      Algebra.adjoin ℤ (Set.range (heckeOmegaRegBarQT N)))

def heckeEvalOmegaBarQT (h : HeckeOmegaCommuteBarQT N) :
    HeckeAlg →+* Module.End (AlgebraicClosure ℚ)
      ↥(regularDiffs (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar N)) :=
  ((Algebra.adjoin ℤ (Set.range (heckeOmegaRegBarQT N))).val.comp
    (heckeEvalOmegaBarAuxQT N h)).toRingHom

open Classical in

def heckeEvalOmegaBarQTotal :
    HeckeAlg →+* Module.End (AlgebraicClosure ℚ)
      ↥(regularDiffs (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar N)) :=
  if h : HeckeOmegaCommuteBarQ N then heckeEvalOmegaBarQ N h
  else (Int.castRingHom _).comp
    (MvPolynomial.eval₂Hom (Int.castRingHom ℤ) (0 : Nat.Primes → ℤ))

open Classical in

def heckeEvalOmegaBarQTTotal :
    HeckeAlg →+* Module.End (AlgebraicClosure ℚ)
      ↥(regularDiffs (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar N)) :=
  if h : HeckeOmegaCommuteBarQT N then heckeEvalOmegaBarQT N h
  else (Int.castRingHom _).comp
    (MvPolynomial.eval₂Hom (Int.castRingHom ℤ) (0 : Nat.Primes → ℤ))
end OmegaModule

namespace HeckeWord

def HeckeInputsAlongT (L : Type*) [Field L] [Algebra ℚ L] (N ℓ : ℕ) [NeZero N]
    [NeZero ℓ] : Prop :=
  ∃ (hα : HeckeAlphaBarIntegral L N ℓ) (_ : HeckeBetaBarIntegral L N ℓ)
    (_ : HasPrincipalDivisors L (laurentBaseChange L (modularFunctionFieldFull (N * ℓ))))
    (hfin : FiniteAlong L (heckeBetaBar L N ℓ)),
    FundamentalIdentityAlong L (heckeAlphaBar L N ℓ) hα ∧
      NormFormulaAlong L (heckeBetaBar L N ℓ) hfin

variable (N : ℕ) [NeZero N]

def letterKey (ℓ : Nat.Primes) : Prop :=
  letI : NeZero (ℓ : ℕ) := ⟨ℓ.2.ne_zero⟩
  (HeckeInputsAlong (AlgebraicClosure ℚ) N ℓ ∧
      HeckeInputsAlongT (AlgebraicClosure ℚ) N ℓ) ∧
    HeckeOmegaPreservesBar N ∧ HeckeOmegaPreservesBarT N

open Classical in

def letterJ : Nat.Primes ⊕ Nat.Primes → Module.End ℤ (JZero N) :=
  Sum.elim
    (fun ℓ =>
      letI : NeZero (ℓ : ℕ) := ⟨ℓ.2.ne_zero⟩
      if h : letterKey N ℓ then
        haveI := h.1.1.snd.snd.fst
        (heckePic0Bar h.1.1.fst h.1.1.snd.fst h.1.1.snd.snd.snd.snd.1
          h.1.1.snd.snd.snd.fst h.1.1.snd.snd.snd.snd.2).toIntLinearMap
      else 0)
    (fun ℓ =>
      letI : NeZero (ℓ : ℕ) := ⟨ℓ.2.ne_zero⟩
      if h : letterKey N ℓ then
        haveI := h.1.2.snd.snd.fst
        (heckePic0BarTranspose h.1.2.fst h.1.2.snd.fst h.1.2.snd.snd.snd.snd.1
          h.1.2.snd.snd.snd.fst h.1.2.snd.snd.snd.snd.2).toIntLinearMap
      else 0)

open Classical in

def letterO :
    Nat.Primes ⊕ Nat.Primes →
      Module.End (AlgebraicClosure ℚ)
        ↥(regularDiffs (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar N)) :=
  Sum.elim
    (fun ℓ =>
      if h : letterKey N ℓ then
        (heckeOmegaBar N ℓ).restrict (fun ω hω => h.2.1 ℓ ω hω)
      else 0)
    (fun ℓ =>
      if h : letterKey N ℓ then
        (heckeOmegaBarT N ℓ).restrict (fun ω hω => h.2.2 ℓ ω hω)
      else 0)

def wordJ (w : List (Nat.Primes ⊕ Nat.Primes)) : Module.End ℤ (JZero N) :=
  (w.map (letterJ N)).prod

def wordO (w : List (Nat.Primes ⊕ Nat.Primes)) :
    Module.End (AlgebraicClosure ℚ)
      ↥(regularDiffs (AlgebraicClosure ℚ) ↥(modularFunctionFieldBar N)) :=
  (w.reverse.map (letterO N)).prod

def wordTr (w : List (Nat.Primes ⊕ Nat.Primes)) : List (Nat.Primes ⊕ Nat.Primes) :=
  (w.map Sum.swap).reverse

def vpEnd (p : ℕ) [Fact p.Prime] (f : Module.End ℤ (JZero N)) :
    Module.End ℚ_[p] (RationalTateModule p (JZero N)) :=
  Module.End.baseChangeHom ℤ_[p] ℚ_[p] (TateModule p (JZero N))
    (TateModule.rep p (JZero N) (Module.End ℤ (JZero N)) f)

end HeckeWord

end ModularCurve

end

Statements phrased using this module (0)

No statement module imports it directly (it is used through other definition modules or by proofs).