Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_CuspForm_NewLattice.lean

definition module

The q-new integral lattice and its reduction mod p

Fix M with M \neq 0, a prime q, and an Atkin–Lehner datum A for (M,q), i.e. a factorisation M = qR together with integers a,b satisfying qa - Rb = 1 (these data determine the matrix \begin{pmatrix} qa & b \\ qR & q\end{pmatrix} of determinant q and hence the slash operator alSlash). Write \mathcal{T} = heckeAlgebra M 2 {ℓ | ℓ ∣ M}, the \mathbb{Z}-subalgebra of \mathrm{End}_{\mathbb C} S_2(\Gamma_0(M)) generated by the operators heckeTLin for primes \ell \nmid M; because the excluded set is the set of divisors of M, no U-operator occurs among the generators, so this is the anemic Hecke algebra. newLattice A hq is the \mathbb{Z}-submodule of S_2(\Gamma_0(M)) consisting of those f such that for every t \in \mathcal{T} the form tf lies in intLattice M 2 (the \mathbb{Z}-span of the forms all of whose q-expansion coefficients are rational integers) and is killed both by traceLin A hq, the map f \mapsto f + U_q(f\mid_2 W) into S_2(\Gamma_0(R)), and by traceLin A hq ∘ atkinLehnerLin A 2, i.e. by the same trace applied to f \mid_2 W. By construction this is the largest \mathcal{T}-stable subgroup of the integral lattice annihilated by both traces: apply_mem_newLattice gives stability, and newLatticeIncl_mem_intLattice, newLatticeIncl_mem give the two containments by taking t = 1.

The remaining declarations package this. newLatticeEnd is the ring homomorphism \mathcal{T} \to \mathrm{End}_{\mathbb Z}(L) obtained by restricting scalars to \mathbb Z and restricting operators to L = newLattice A hq, and supplies the \mathcal{T}-module structure, with newLattice_coe_smul and newLatticeIncl_smul recording that the action is the operator action on cusp forms. For p : \mathbb{N}, pNewLattice A hq p is the \mathcal{T}-submodule pL of elements p \cdot b, newLatticeRed A hq p is the quotient L/pL as a \mathcal{T}-module, newLatticeRedMk the (surjective) projection, and natCast_smul_newLatticeRed says p acts as zero on the quotient. newLatticeIncl is the injective, Hecke-equivariant inclusion L \hookrightarrow S_2(\Gamma_0(M)).

Relation to Mathlib

Built on Mathlib's CuspForm, CongruenceSubgroup.Gamma0, slash actions and Submodule (including its quotient modules). The ingredients combined here — the Hecke algebra of operators on weight-2 cusp forms, the integral lattice of forms with integral q-expansions, the Atkin–Lehner slash operator and the level-lowering trace — are the project's own definitions.

Where it is used

The lattice of q-new integral forms and its reduction modulo p as a module over the anemic Hecke algebra are the objects on which the level-lowering step operates: one shows that a mod p eigenform of level M = qR whose associated representation is unramified (or suitably mild) at q gives a class in L/pL that is then transferred to level R.

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
  2. A. O. L. Atkin and J. Lehner, Hecke operators on \Gamma_0(m), Mathematische Annalen 185 (1970), 134–160
  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_CuspForm_NewLattice.lean

Imports

Imported by

  • no other definition module

Declarations

Source

import Definitions.Def_CuspForm_HeckeAlgebra
import Definitions.Def_CuspForm_IntegralStructure
import Definitions.Def_CuspForm_LevelLoweringTrace
import Definitions.Def_CuspForm_AtkinLehnerOperator

set_option autoImplicit false

noncomputable section

namespace CuspForm

open ModularForm

variable {M q : ℕ} [NeZero M] (A : AtkinLehnerDatum M q) (hq : q.Prime)

def newLattice : Submodule ℤ (CuspForm (CongruenceSubgroup.Gamma0 M) 2) where
  carrier := {f | ∀ t ∈ heckeAlgebra M 2 {ℓ | ℓ ∣ M},
    t f ∈ intLattice M 2 ∧ traceLin A hq (t f) = 0 ∧ traceLin A hq (atkinLehnerLin A 2 (t f)) = 0}
  zero_mem' t _ := by
    rw [map_zero]
    exact ⟨Submodule.zero_mem _, by rw [map_zero], by rw [map_zero, map_zero]⟩
  add_mem' {f g} hf hg t ht := by
    obtain ⟨hf₁, hf₂, hf₃⟩ := hf t ht
    obtain ⟨hg₁, hg₂, hg₃⟩ := hg t ht
    rw [map_add]
    exact ⟨Submodule.add_mem _ hf₁ hg₁, by rw [map_add, hf₂, hg₂, add_zero],
      by rw [map_add, map_add, hf₃, hg₃, add_zero]⟩
  smul_mem' c {f} hf t ht := by
    obtain ⟨hf₁, hf₂, hf₃⟩ := hf t ht
    rw [map_zsmul]
    exact ⟨Submodule.smul_mem _ c hf₁, by rw [map_zsmul, hf₂, smul_zero],
      by rw [map_zsmul, map_zsmul, hf₃, smul_zero]⟩

variable {A hq}

theorem mem_newLattice_iff {f : CuspForm (CongruenceSubgroup.Gamma0 M) 2} :
    f ∈ newLattice A hq ↔ ∀ t ∈ heckeAlgebra M 2 {ℓ | ℓ ∣ M},
      t f ∈ intLattice M 2 ∧ traceLin A hq (t f) = 0 ∧ traceLin A hq (atkinLehnerLin A 2 (t f)) = 0 :=
  Iff.rfl

theorem apply_mem_newLattice {t : Module.End ℂ (CuspForm (CongruenceSubgroup.Gamma0 M) 2)}
    (ht : t ∈ heckeAlgebra M 2 {ℓ | ℓ ∣ M}) {f : CuspForm (CongruenceSubgroup.Gamma0 M) 2}
    (hf : f ∈ newLattice A hq) : t f ∈ newLattice A hq :=
  fun s hs => hf (s * t) (Subalgebra.mul_mem _ hs ht)

variable (A hq) in

def newLatticeEnd : heckeAlgebra M 2 {ℓ | ℓ ∣ M} →+* Module.End ℤ (newLattice A hq) where
  toFun t := ((t : Module.End ℂ (CuspForm (CongruenceSubgroup.Gamma0 M) 2)).restrictScalars ℤ).restrict
    fun _ hf => apply_mem_newLattice t.2 hf
  map_one' := LinearMap.ext fun _ => Subtype.ext rfl
  map_mul' _ _ := LinearMap.ext fun _ => Subtype.ext rfl
  map_zero' := LinearMap.ext fun _ => Subtype.ext rfl
  map_add' _ _ := LinearMap.ext fun _ => Subtype.ext rfl

instance instSMulHeckeAlgebraNewLattice : SMul (heckeAlgebra M 2 {ℓ | ℓ ∣ M}) (newLattice A hq) :=
  ⟨fun t a => newLatticeEnd A hq t a⟩

instance instModuleHeckeAlgebraNewLattice : Module (heckeAlgebra M 2 {ℓ | ℓ ∣ M}) (newLattice A hq) :=
  Module.compHom (newLattice A hq) (newLatticeEnd A hq)

theorem newLattice_coe_smul (t : heckeAlgebra M 2 {ℓ | ℓ ∣ M}) (a : newLattice A hq) :
    ((t • a : newLattice A hq) : CuspForm (CongruenceSubgroup.Gamma0 M) 2)
      = (t : Module.End ℂ (CuspForm (CongruenceSubgroup.Gamma0 M) 2)) a :=
  rfl

variable (A hq) in

def pNewLattice (p : ℕ) : Submodule (heckeAlgebra M 2 {ℓ | ℓ ∣ M}) (newLattice A hq) where
  carrier := {a | ∃ b : newLattice A hq, a = (p : heckeAlgebra M 2 {ℓ | ℓ ∣ M}) • b}
  zero_mem' := ⟨0, (smul_zero _).symm⟩
  add_mem' := by
    rintro _ _ ⟨b, rfl⟩ ⟨c, rfl⟩
    exact ⟨b + c, (smul_add _ _ _).symm⟩
  smul_mem' := by
    rintro t _ ⟨b, rfl⟩
    exact ⟨t • b, by rw [smul_smul, smul_smul, mul_comm]⟩

theorem mem_pNewLattice_iff (p : ℕ) {a : newLattice A hq} :
    a ∈ pNewLattice A hq p ↔ ∃ b : newLattice A hq, a = (p : heckeAlgebra M 2 {ℓ | ℓ ∣ M}) • b :=
  Iff.rfl

variable (A hq) in

abbrev newLatticeRed (p : ℕ) : Type :=
  newLattice A hq ⧸ pNewLattice A hq p

instance instAddCommGroupNewLatticeRed (p : ℕ) : AddCommGroup (newLatticeRed A hq p) :=
  Submodule.Quotient.addCommGroup _

instance instModuleHeckeAlgebraNewLatticeRed (p : ℕ) :
    Module (heckeAlgebra M 2 {ℓ | ℓ ∣ M}) (newLatticeRed A hq p) :=
  Submodule.Quotient.module _

instance instSMulHeckeAlgebraNewLatticeRed (p : ℕ) :
    SMul (heckeAlgebra M 2 {ℓ | ℓ ∣ M}) (newLatticeRed A hq p) :=
  (instModuleHeckeAlgebraNewLatticeRed p).toDistribMulAction.toMulAction.toSMul

instance instMulActionHeckeAlgebraNewLatticeRed (p : ℕ) :
    MulAction (heckeAlgebra M 2 {ℓ | ℓ ∣ M}) (newLatticeRed A hq p) :=
  (instModuleHeckeAlgebraNewLatticeRed p).toDistribMulAction.toMulAction

instance instDistribMulActionHeckeAlgebraNewLatticeRed (p : ℕ) :
    DistribMulAction (heckeAlgebra M 2 {ℓ | ℓ ∣ M}) (newLatticeRed A hq p) :=
  (instModuleHeckeAlgebraNewLatticeRed p).toDistribMulAction

instance instSMulWithZeroHeckeAlgebraNewLatticeRed (p : ℕ) :
    SMulWithZero (heckeAlgebra M 2 {ℓ | ℓ ∣ M}) (newLatticeRed A hq p) :=
  (instModuleHeckeAlgebraNewLatticeRed p).toMulActionWithZero.toSMulWithZero

instance instMulActionWithZeroHeckeAlgebraNewLatticeRed (p : ℕ) :
    MulActionWithZero (heckeAlgebra M 2 {ℓ | ℓ ∣ M}) (newLatticeRed A hq p) :=
  (instModuleHeckeAlgebraNewLatticeRed p).toMulActionWithZero

variable (A hq) in

def newLatticeRedMk (p : ℕ) :
    newLattice A hq →ₗ[heckeAlgebra M 2 {ℓ | ℓ ∣ M}] newLatticeRed A hq p :=
  Submodule.mkQ _

theorem newLatticeRedMk_surjective (p : ℕ) : Function.Surjective (newLatticeRedMk A hq p) :=
  Submodule.mkQ_surjective _

theorem natCast_smul_newLatticeRed (p : ℕ) (x : newLatticeRed A hq p) :
    (p : heckeAlgebra M 2 {ℓ | ℓ ∣ M}) • x = 0 := by
  obtain ⟨a, rfl⟩ := newLatticeRedMk_surjective p x
  rw [← LinearMap.map_smul]
  exact (Submodule.Quotient.mk_eq_zero _).mpr ⟨a, rfl⟩

variable (A hq) in

def newLatticeIncl : newLattice A hq →+ CuspForm (CongruenceSubgroup.Gamma0 M) 2 :=
  (newLattice A hq).subtype.toAddMonoidHom

theorem newLatticeIncl_apply (a : newLattice A hq) :
    newLatticeIncl A hq a = (a : CuspForm (CongruenceSubgroup.Gamma0 M) 2) :=
  rfl

theorem newLatticeIncl_injective : Function.Injective (newLatticeIncl A hq) :=
  Subtype.val_injective

theorem newLatticeIncl_smul (t : heckeAlgebra M 2 {ℓ | ℓ ∣ M}) (a : newLattice A hq) :
    newLatticeIncl A hq (t • a)
      = (t : Module.End ℂ (CuspForm (CongruenceSubgroup.Gamma0 M) 2)) (newLatticeIncl A hq a) :=
  rfl

theorem newLatticeIncl_mem_intLattice (a : newLattice A hq) : newLatticeIncl A hq a ∈ intLattice M 2 :=
  (a.2 1 (Subalgebra.one_mem _)).1

theorem newLatticeIncl_mem (a : newLattice A hq) :
    newLatticeIncl A hq a ∈
      LinearMap.ker (traceLin A hq) ⊓ LinearMap.ker ((traceLin A hq) ∘ₗ (atkinLehnerLin A 2)) :=
  ⟨(a.2 1 (Subalgebra.one_mem _)).2.1, (a.2 1 (Subalgebra.one_mem _)).2.2⟩

end CuspForm

end

Statements phrased using this module (3)