Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_FreyPackage_ModMCarrier_OldSublattice.lean

definition module

Degeneracy maps, oldform sublattice and reductions at Atkin–Lehner level

Fix M with M \neq 0 and an Atkin–Lehner datum W for (M,q'), i.e. a natural number W.R with M = q' \cdot W.R together with integers a,b satisfying q'a - W.R\,b = 1. Two \mathbb{C}-linear degeneracy maps S_k(\Gamma_0(W.R)) \to S_k(\Gamma_0(M)) are available: levelInclusionLin, attached to any divisibility R \mid M, which sends a cusp form to the same function on \mathbb{H}, the invariance and cusp conditions transferring because \Gamma_0(M) \le \Gamma_0(R) (the lemma CongruenceSubgroup.Gamma0_le_Gamma0_of_dvd, proved by reduction of the lower-left entry); and rescaleLin, the slash action by \mathrm{diag}(q',1), i.e. f \mapsto f \mid_k \begin{pmatrix} q' & 0 \\ 0 & 1\end{pmatrix}. The object oldformSublattice W is the \mathbb{Z}-submodule of S_2(\Gamma_0(M)) generated by the images under these two maps of CuspForm.intLattice W.R 2, the \mathbb{Z}-span of those weight-two cusp forms on \Gamma_0(W.R) all of whose q-expansion coefficients are rational integers; the two membership lemmas record that each degeneracy image of an integral form lies in it.

Over a field k, writing \mathrm{latticeRed}\,k\,L = k \otimes_{\mathbb{Z}} L, the maps ι₀red and ι₁red are the k-linear base changes of the restrictions of the two degeneracy maps to the integral lattices, landing in k \otimes_{\mathbb{Z}} \mathrm{oldformSublattice}\,W, and f₀red is the class 1 \otimes f of an integral form f. Separately, for an ideal \mathfrak{m} of the integral closure \overline{\mathbb{Z}} of \mathbb{Z} in \mathbb{C}, WitnessResidueField 𝔪 is the quotient ring \overline{\mathbb{Z}}/\mathfrak{m} with its quotient map (no maximality of \mathfrak{m} is imposed by the definition). Finally, atkinLehnerDatumOfPrimeNotDvd produces, for a prime q' with q' \nmid N, an Atkin–Lehner datum for (N q', q') with cofactor N, the Bézout integers coming from \gcd(q',N) = 1.

Relation to Mathlib

Mathlib supplies CuspForm, the slash action and the groups Gamma0; the monotonicity lemma for Gamma0 under divisibility is added here in Mathlib's CongruenceSubgroup namespace. The integral structure on cusp forms, the degeneracy maps, the oldform sublattice and the base-change construction k \otimes_{\mathbb{Z}} L on lattices of cusp forms are the project's own.

Where it is used

The oldform sublattice is the lattice on which the Atkin–Lehner-twisted trace from level M = q'R to level R behaves integrally, and its reduction modulo a residue characteristic carries the two degeneracy maps entering Ihara-type statements. These are the inputs to the level-raising step that produces, from a modular form of level R, a form of level M whose mod-\ell representation agrees with the given one, as used in the Frey–Serre–Ribet part of the argument.

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. A. O. L. Atkin and J. Lehner, Hecke operators on \Gamma_0(m), Mathematische Annalen 185 (1970), 134–160
  3. F. Diamond and J. Im, Modular forms and modular curves, in: Seminar on Fermat's Last Theorem, CMS Conference Proceedings 17, American Mathematical Society, 1995, 39–133

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_FreyPackage_ModMCarrier_LatticeRed
import Definitions.Def_FreyPackage_ModMCarrier_Rescale
import Definitions.Def_CuspForm_IntegralStructure
import Definitions.Def_ModularForm_AtkinLehnerDatum

set_option autoImplicit false
noncomputable section
open CongruenceSubgroup ModularForm
open scoped TensorProduct

lemma CongruenceSubgroup.Gamma0_le_Gamma0_of_dvd {R M : ℕ} (hRM : R ∣ M) :
    Gamma0 M ≤ Gamma0 R := by
  intro γ hγ
  rw [Gamma0_mem] at hγ ⊢
  have : ZMod.castHom hRM (ZMod R) (((γ : Matrix (Fin 2) (Fin 2) ℤ) 1 0 : ℤ) : ZMod M)
      = (((γ : Matrix (Fin 2) (Fin 2) ℤ) 1 0 : ℤ) : ZMod R) := map_intCast _ _
  rw [← this, hγ, map_zero]

namespace FreyPackage.ModMCarrier

def levelInclusionLin {R M : ℕ} [NeZero M] (hRM : R ∣ M) (k : ℤ) :
    CuspForm (Gamma0 R) k →ₗ[ℂ] CuspForm (Gamma0 M) k where
  toFun f :=
    { toFun := ⇑f
      slash_action_eq' := fun γ hγ =>
        f.slash_action_eq' γ (Subgroup.map_mono (Gamma0_le_Gamma0_of_dvd hRM) hγ)
      holo' := f.holo'
      zero_at_cusps' := fun {c} hc => f.zero_at_cusps'
        (hc.mono (Subgroup.map_mono (Gamma0_le_Gamma0_of_dvd hRM))) }
  map_add' f g := rfl
  map_smul' c f := rfl

@[simp] lemma coe_levelInclusionLin {R M : ℕ} [NeZero M] (hRM : R ∣ M) (k : ℤ)
    (f : CuspForm (Gamma0 R) k) : ⇑(levelInclusionLin hRM k f) = ⇑f := rfl

lemma _root_.ModularForm.AtkinLehnerDatum.R_dvd {M q' : ℕ} (W : ModularForm.AtkinLehnerDatum M q') :
    W.R ∣ M := ⟨q', W.hM.trans (Nat.mul_comm q' W.R)⟩

end FreyPackage.ModMCarrier

namespace FreyPackage.ModMCarrier

section WitnessResidueField

abbrev WitnessResidueField (𝔪 : Ideal (integralClosure ℤ ℂ)) : Type :=
  (integralClosure ℤ ℂ) ⧸ 𝔪

abbrev witnessResidueMap (𝔪 : Ideal (integralClosure ℤ ℂ)) :
    integralClosure ℤ ℂ →+* WitnessResidueField 𝔪 :=
  Ideal.Quotient.mk 𝔪

lemma witnessResidueMap_mem (𝔪 : Ideal (integralClosure ℤ ℂ)) :
    ∀ x ∈ 𝔪, witnessResidueMap 𝔪 x = 0 :=
  fun _ hx => Ideal.Quotient.eq_zero_iff_mem.mpr hx

end WitnessResidueField

section OldSublattice
variable {M q' : ℕ} [NeZero M] (W : ModularForm.AtkinLehnerDatum M q')

local instance instNeZeroR : NeZero W.R :=
  ⟨fun h => NeZero.ne M (W.hM.trans (by rw [h, mul_zero]))⟩

def oldformSublattice : Submodule ℤ (CuspForm (Gamma0 M) 2) :=
  (CuspForm.intLattice W.R 2).map ((levelInclusionLin W.R_dvd 2).restrictScalars ℤ) ⊔
  (CuspForm.intLattice W.R 2).map ((rescaleLin W.q_mul_R_dvd 2).restrictScalars ℤ)

lemma levelInclusionLin_mem_oldformSublattice :
    ∀ x ∈ CuspForm.intLattice W.R 2,
      levelInclusionLin W.R_dvd 2 x ∈ oldformSublattice W :=
  fun _ hx => Submodule.mem_sup_left (Submodule.mem_map_of_mem hx)

lemma rescaleLin_mem_oldformSublattice :
    ∀ x ∈ CuspForm.intLattice W.R 2,
      rescaleLin W.q_mul_R_dvd 2 x ∈ oldformSublattice W :=
  fun _ hx => Submodule.mem_sup_right (Submodule.mem_map_of_mem hx)

section ReducedMaps
variable (k : Type*) [Field k]

def f₀red {f : CuspForm (Gamma0 W.R) 2} (hf : f ∈ CuspForm.intLattice W.R 2) :
    latticeRed k (CuspForm.intLattice W.R 2) :=
  latticeRed.mk k _ ⟨f, hf⟩

def ι₀red : latticeRed k (CuspForm.intLattice W.R 2) →ₗ[k] latticeRed k (oldformSublattice W) :=
  latticeRed.mapOf k _ _ (levelInclusionLin W.R_dvd 2) (levelInclusionLin_mem_oldformSublattice W)

def ι₁red : latticeRed k (CuspForm.intLattice W.R 2) →ₗ[k] latticeRed k (oldformSublattice W) :=
  latticeRed.mapOf k _ _ (rescaleLin W.q_mul_R_dvd 2) (rescaleLin_mem_oldformSublattice W)

end ReducedMaps
end OldSublattice

section OfPrimeNotDvd
variable (N q' : ℕ)

def atkinLehnerDatumOfPrimeNotDvd (hq' : q'.Prime) (hnd : ¬ q' ∣ N) :
    ModularForm.AtkinLehnerDatum (N * q') q' where
  R := N
  hM := Nat.mul_comm N q'
  a := (Nat.gcdA q' N)
  b := -(Nat.gcdB q' N)
  bezout := by
    have hcop : Nat.gcd q' N = 1 := (hq'.coprime_iff_not_dvd).mpr hnd
    have hab := Nat.gcd_eq_gcd_ab q' N
    rw [hcop, Nat.cast_one] at hab
    push_cast
    linarith [hab]

@[simp] lemma atkinLehnerDatumOfPrimeNotDvd_R (hq' : q'.Prime) (hnd : ¬ q' ∣ N) :
    (atkinLehnerDatumOfPrimeNotDvd N q' hq' hnd).R = N := rfl

end OfPrimeNotDvd

end FreyPackage.ModMCarrier

Statements phrased using this module (3)