Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_HeckeOperator.lean

definition module

Hecke correspondences on base-changed modular function fields

Fix a field L of characteristic zero (L a field with a \mathbb{Q}-algebra structure), a level N and an index \ell, both nonzero. All objects live on the base change laurentBaseChange L (modularFunctionFieldFull N), the intermediate field of L((q)) generated over L by the coefficientwise image of the project's full modular function field of level N (imported from ModularCurve_ArithmeticGalois); at L=\overline{\mathbb{Q}} this is modularFunctionFieldBar N, whose Pic0 is JZero N. Two L-algebra maps from level N to level N\ell are defined: heckeAlphaBar, which is literally IntermediateField.inclusion applied to the monotonicity of laurentBaseChange along the degeneracy inclusion for N \mid N\ell (so it is the identity on underlying Laurent series, coe_heckeAlphaBar), and heckeBetaBar, the substitution q \mapsto q^{\ell} given by the project's qExpand L ℓ on L((q)) (coe_heckeBetaBar), built from the ring homomorphism heckeBetaBarRingHom and shown to fix L; that q \mapsto q^{\ell} maps the level-N field into the level-N\ell field is supplied by the private helpers coeffMap_qExpand', coeffEmb_qExpand', laurentBaseChange_mono' and qExpand_mem_laurentBaseChange'. Two predicates record integrality of these maps as ring homomorphisms: HeckeAlphaBarIntegral, HeckeBetaBarIntegral. Given these, heckeDivBar is Divisor.correspondence (heckeBetaBar …) (heckeAlphaBar …), i.e. push-forward along \alpha of pull-back along \beta, an additive endomorphism of the divisor group of the level-N field over L; heckePic0Bar is the corresponding endomorphism of Pic0, taking as further explicit binders the fundamental identity along \beta and the finiteness and norm formula along \alpha from AlgebraicCurve_Correspondence, together with an instance binder HasPrincipalDivisors L at level N\ell. heckeDivBarTranspose and heckePic0BarTranspose are the same constructions with the roles of \alpha and \beta exchanged. The module only constructs these maps: no primality of \ell is assumed, \ell \mid N and \ell = 1 are permitted, nothing is proved about the operators, and neither orientation is identified with the classical action a_n \mapsto a_{n\ell} + \ell a_{n/\ell} on q-expansions. Two examples check that at L = \overline{\mathbb{Q}} the maps land on modularFunctionFieldBar and give an endomorphism of JZero N.

Relation to Mathlib

Mathlib has no Hecke correspondence on Jacobians of modular curves; the function-field carriers (modularFunctionFieldFull, laurentBaseChange, qExpand), the divisor and Pic0 formalism and Divisor.correspondence/Pic0.correspondence are the project's own, imported from its definition modules. Only IntermediateField.inclusion and the RingHom.IsIntegral predicate used in the integrality definitions come from Mathlib.

Where it is used

These endomorphisms provide the Hecke action on the Jacobian J_0(N) in the form used later for the Eichler–Shimura relation and for the Galois representations attached to modular forms, which is what the Frey curve route to Fermat's Last Theorem requires.

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. G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Publications of the Mathematical Society of Japan 11, Princeton University Press, 1971
  3. F. Diamond, J. Shurman, A First Course in Modular Forms, Graduate Texts in Mathematics 228, Springer, 2005

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

Imports

Imported by

Declarations

Source

import Definitions.Def_AlgebraicCurve_Correspondence
import Definitions.Def_ModularCurve_ArithmeticGalois

set_option autoImplicit false

noncomputable section

open IsDedekindDomain

namespace ModularCurve

open AlgebraicCurve IntermediateField HahnSeries

section PrivateSupply

variable {L : Type*} [Field L] [Algebra ℚ L]

private theorem coeffMap_qExpand' {R S : Type*} [CommRing R] [CommRing S] (f : R →+* S) (n : ℕ)
    [NeZero n] (x : LaurentSeries R) : coeffMap f (qExpand R n x) = qExpand S n (coeffMap f x) := by
  ext k
  by_cases hk : (n : ℤ) ∣ k
  · obtain ⟨m, rfl⟩ := hk
    rw [coeffMap_coeff, qExpand_coeff_mul, qExpand_coeff_mul, coeffMap_coeff]
  · rw [coeffMap_coeff, qExpand_coeff_of_not_dvd n _ hk, qExpand_coeff_of_not_dvd n _ hk,
      map_zero]

private theorem coeffEmb_qExpand' (L : Type*) [Field L] [Algebra ℚ L] (n : ℕ) [NeZero n]
    (x : LaurentSeries ℚ) : coeffEmb L (qExpand ℚ n x) = qExpand L n (coeffEmb L x) :=
  coeffMap_qExpand' _ n x

variable (L) in
private theorem laurentBaseChange_mono' {F₀ F₁ : IntermediateField ℚ (LaurentSeries ℚ)}
    (h : F₀ ≤ F₁) : laurentBaseChange L F₀ ≤ laurentBaseChange L F₁ := by
  rw [laurentBaseChange, IntermediateField.adjoin_le_iff]
  rintro _ ⟨y, hy, rfl⟩
  exact coeffEmb_mem_laurentBaseChange L (h hy)

private theorem qExpand_mem_laurentBaseChange' {F₀ : IntermediateField ℚ (LaurentSeries ℚ)} (n : ℕ)
    [NeZero n] {F₁ : IntermediateField ℚ (LaurentSeries ℚ)} (hF : ∀ y ∈ F₀, qExpand ℚ n y ∈ F₁)
    {x : LaurentSeries L} (hx : x ∈ laurentBaseChange L F₀) :
    qExpand L n x ∈ laurentBaseChange L F₁ := by
  rw [mem_laurentBaseChange_iff] at hx
  induction hx using Subfield.closure_induction with
  | mem y hy =>
      rcases hy with ⟨a, rfl⟩ | ⟨z, hz, rfl⟩
      · rw [algebraMap_laurentSeries_eq_single, qExpand_single, mul_zero,
          ← algebraMap_laurentSeries_eq_single]
        exact (laurentBaseChange L F₁).algebraMap_mem _
      · rw [← coeffEmb_qExpand']
        exact coeffEmb_mem_laurentBaseChange L (hF z hz)
  | one => simp
  | add x y _ _ hx hy => simpa using add_mem hx hy
  | neg x _ hx => simpa using neg_mem hx
  | inv x _ hx => simpa using inv_mem hx
  | mul x y _ _ hx hy => simpa using mul_mem hx hy

end PrivateSupply

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

section DegeneracyMapsBar

variable (L) in

def heckeAlphaBar :
    laurentBaseChange L (modularFunctionFieldFull N) →ₐ[L]
      laurentBaseChange L (modularFunctionFieldFull (N * ℓ)) :=
  IntermediateField.inclusion
    (laurentBaseChange_mono' L (full_degeneracy_le (dvd_mul_right N ℓ)))

@[simp]
theorem coe_heckeAlphaBar (x : laurentBaseChange L (modularFunctionFieldFull N)) :
    (heckeAlphaBar L N ℓ x : LaurentSeries L) = (x : LaurentSeries L) :=
  IntermediateField.coe_inclusion _ x

variable (L) in

def heckeBetaBarRingHom :
    laurentBaseChange L (modularFunctionFieldFull N) →+*
      laurentBaseChange L (modularFunctionFieldFull (N * ℓ)) where
  toFun x := ⟨qExpand L ℓ (x : LaurentSeries L),
    qExpand_mem_laurentBaseChange' ℓ
      (fun y hy => full_degeneracy_map_le (N := N) ℓ ⟨y, hy, rfl⟩) x.2⟩
  map_one' := Subtype.ext (map_one (qExpand L ℓ))
  map_mul' _ _ := Subtype.ext (map_mul (qExpand L ℓ) _ _)
  map_zero' := Subtype.ext (map_zero (qExpand L ℓ))
  map_add' _ _ := Subtype.ext (map_add (qExpand L ℓ) _ _)

omit [NeZero N] in
@[simp]
theorem coe_heckeBetaBarRingHom (x : laurentBaseChange L (modularFunctionFieldFull N)) :
    (heckeBetaBarRingHom L N ℓ x : LaurentSeries L) = qExpand L ℓ (x : LaurentSeries L) :=
  rfl

variable (L) in

def heckeBetaBar :
    laurentBaseChange L (modularFunctionFieldFull N) →ₐ[L]
      laurentBaseChange L (modularFunctionFieldFull (N * ℓ)) :=
  { heckeBetaBarRingHom L N ℓ with
    commutes' := fun a => Subtype.ext <| by
      show qExpand L ℓ (algebraMap L (LaurentSeries L) a) = algebraMap L (LaurentSeries L) a
      rw [algebraMap_laurentSeries_eq_single, qExpand_single, mul_zero] }

theorem heckeAlphaBar_eq_inclusion
    (h : laurentBaseChange L (modularFunctionFieldFull N)
      ≤ laurentBaseChange L (modularFunctionFieldFull (N * ℓ))) :
    heckeAlphaBar L N ℓ = IntermediateField.inclusion h :=
  rfl

omit [NeZero N] in
@[simp]
theorem coe_heckeBetaBar (x : laurentBaseChange L (modularFunctionFieldFull N)) :
    (heckeBetaBar L N ℓ x : LaurentSeries L) = qExpand L ℓ (x : LaurentSeries L) :=
  rfl

end DegeneracyMapsBar

section HeckePic0Bar

variable (L) in

def HeckeAlphaBarIntegral : Prop :=
  (heckeAlphaBar L N ℓ).toRingHom.IsIntegral

variable (L) in

def HeckeBetaBarIntegral : Prop :=
  (heckeBetaBar L N ℓ).toRingHom.IsIntegral

variable {N ℓ}
variable (hα : HeckeAlphaBarIntegral L N ℓ) (hβ : HeckeBetaBarIntegral L N ℓ)
variable [HasPrincipalDivisors L (laurentBaseChange L (modularFunctionFieldFull (N * ℓ)))]

def heckeDivBar :
    Divisor L (laurentBaseChange L (modularFunctionFieldFull N)) →+
      Divisor L (laurentBaseChange L (modularFunctionFieldFull N)) :=
  Divisor.correspondence (heckeBetaBar L N ℓ) (heckeAlphaBar L N ℓ) hβ hα

def heckePic0Bar
    (hFI : FundamentalIdentityAlong L (heckeBetaBar L N ℓ) hβ)
    (hfin : FiniteAlong L (heckeAlphaBar L N ℓ))
    (hN : NormFormulaAlong L (heckeAlphaBar L N ℓ) hfin) :
    Pic0 L (laurentBaseChange L (modularFunctionFieldFull N)) →+
      Pic0 L (laurentBaseChange L (modularFunctionFieldFull N)) :=
  Pic0.correspondence (heckeBetaBar L N ℓ) (heckeAlphaBar L N ℓ) hβ hα hFI hfin hN

end HeckePic0Bar

section Transpose

variable {N ℓ}
variable (hα : HeckeAlphaBarIntegral L N ℓ) (hβ : HeckeBetaBarIntegral L N ℓ)
variable [HasPrincipalDivisors L (laurentBaseChange L (modularFunctionFieldFull (N * ℓ)))]

def heckeDivBarTranspose :
    Divisor L (laurentBaseChange L (modularFunctionFieldFull N)) →+
      Divisor L (laurentBaseChange L (modularFunctionFieldFull N)) :=
  Divisor.correspondence (heckeAlphaBar L N ℓ) (heckeBetaBar L N ℓ) hα hβ

def heckePic0BarTranspose
    (hFI : FundamentalIdentityAlong L (heckeAlphaBar L N ℓ) hα)
    (hfin : FiniteAlong L (heckeBetaBar L N ℓ))
    (hN : NormFormulaAlong L (heckeBetaBar L N ℓ) hfin) :
    Pic0 L (laurentBaseChange L (modularFunctionFieldFull N)) →+
      Pic0 L (laurentBaseChange L (modularFunctionFieldFull N)) :=
  Pic0.correspondence (heckeAlphaBar L N ℓ) (heckeBetaBar L N ℓ) hα hβ hFI hfin hN

end Transpose

section ModularInstance

example :
    (modularFunctionFieldBar N) →ₐ[AlgebraicClosure ℚ] (modularFunctionFieldBar (N * ℓ)) :=
  heckeAlphaBar (AlgebraicClosure ℚ) N ℓ

example (hα : HeckeAlphaBarIntegral (AlgebraicClosure ℚ) N ℓ)
    (hβ : HeckeBetaBarIntegral (AlgebraicClosure ℚ) N ℓ)
    [HasPrincipalDivisors (AlgebraicClosure ℚ) (modularFunctionFieldBar (N * ℓ))]
    (hFI : FundamentalIdentityAlong (AlgebraicClosure ℚ) (heckeBetaBar (AlgebraicClosure ℚ) N ℓ) hβ)
    (hfin : FiniteAlong (AlgebraicClosure ℚ) (heckeAlphaBar (AlgebraicClosure ℚ) N ℓ))
    (hN : NormFormulaAlong (AlgebraicClosure ℚ) (heckeAlphaBar (AlgebraicClosure ℚ) N ℓ) hfin) :
    JZero N →+ JZero N :=
  heckePic0Bar hα hβ hFI hfin hN

end ModularInstance

end ModularCurve

end

Statements phrased using this module (68)