Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_X1HeckeOperator.lean

definition module

Hecke degeneracy maps and Hecke operators on

Throughout, L is a field of characteristic zero (a field with a \mathbb{Q}-algebra structure), M a level and \ell \geq 1. For a congruence subgroup \Gamma, the project's q-expansion function field is the intermediate field of L((q)) generated over L by the quotients \mathrm{int}(p_f)/\mathrm{int}(p_g) of integral q-expansions of two modular forms of equal weight on \Gamma; laurentBaseChange L F₀ denotes the subfield of L((q)) generated by L and the coefficientwise image of F_0 \subseteq \mathbb{Q}((q)). Two maps between base-changed fields are defined. First, heckeAlphaOneBar L M ℓ is the inclusion L\cdot F(\Gamma_1(M)) \hookrightarrow L\cdot F(\Gamma_1(M) \cap \Gamma_0(M\ell)), available because the first field is contained in the second. Secondly, HeckeBetaOneDefined M ℓ is the predicate that the substitution q \mapsto q^{\ell} (the ring homomorphism qExpand, multiplying exponents by \ell) carries F(\Gamma_1(M)) into F(\Gamma_1(M) \cap \Gamma_0(M\ell)); granted this, heckeBetaOneBarOf is the induced L-algebra map on base changes, and heckeBetaOneBar is the total definition equal to it when the predicate holds and to heckeAlphaOneBar otherwise. Auxiliary lemmas record that coefficient maps commute with q \mapsto q^{\ell}, that laurentBaseChange is monotone, and the resulting membership transfer.

With integrality predicates HeckeAlphaOneBarIntegral, HeckeBetaOneBarIntegral for the two maps, and a HasPrincipalDivisors assumption on the upper field, heckeDivOneBar is the correspondence \beta^{*} followed by \alpha_{*} on divisors, and heckePic0OneBar the induced endomorphism of \mathrm{Pic}^0, given the fundamental identity along \beta and finiteness plus the pushforward norm formula along \alpha; heckeDivOneBarTranspose and heckePic0OneBarTranspose interchange the two maps. Finally HeckeInputsOneAlong bundles all these hypotheses as a proposition, and heckeOperatorOneAlong is the total endomorphism of \mathrm{Pic}^0, equal to heckePic0OneBar when the inputs hold and to 0 otherwise; over \overline{\mathbb{Q}} it is an endomorphism of JOne M.

Relation to Mathlib

Mathlib supplies modular forms, the congruence subgroups \Gamma_0, \Gamma_1 and Laurent series, but no modular curve as an algebraic curve and no Hecke action on its Jacobian; the degeneracy maps, the divisor/\mathrm{Pic}^0 correspondences and the Hecke operators here are the project's own, built on its function-field model.

Where it is used

These operators provide the Hecke action on the Jacobian J_1(M) needed to cut out the abelian variety, and hence the Galois representation, attached to a newform; the torsion of \mathrm{Pic}^0 with its arithmetic Galois action supplies the representations used in the Frey curve argument.

References

  1. F. Diamond and J. Shurman, A First Course in Modular Forms, Graduate Texts in Mathematics 228, Springer, 2005, §5.6
  2. G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Princeton University Press, 1971

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

Imports

Imported by

Declarations

Source

import Definitions.Def_AlgebraicCurve_Correspondence
import Definitions.Def_ModularCurve_X1

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 (M ℓ : ℕ) [NeZero ℓ]

section DegeneracyMaps

variable (L) in

def heckeAlphaOneBar :
    laurentBaseChange L (x1FunctionField M) →ₐ[L]
      laurentBaseChange L (x1x0FunctionFieldC ℚ M (M * ℓ)) :=
  IntermediateField.inclusion (laurentBaseChange_mono₁ L (x1FunctionFieldC_le_x1x0 ℚ M (M * ℓ)))

omit [NeZero ℓ] in
@[simp]
theorem coe_heckeAlphaOneBar (x : laurentBaseChange L (x1FunctionField M)) :
    (heckeAlphaOneBar L M ℓ x : LaurentSeries L) = (x : LaurentSeries L) :=
  IntermediateField.coe_inclusion _ x

omit [NeZero ℓ] in

theorem heckeAlphaOneBar_eq_inclusion
    (h : laurentBaseChange L (x1FunctionField M) ≤ laurentBaseChange L (x1x0FunctionFieldC ℚ M (M * ℓ))) :
    heckeAlphaOneBar L M ℓ = IntermediateField.inclusion h :=
  rfl

def HeckeBetaOneDefined : Prop :=
  ∀ y ∈ x1FunctionField M, qExpand ℚ ℓ y ∈ x1x0FunctionFieldC ℚ M (M * ℓ)

variable (L) in

def heckeBetaOneBarRingHomOf (h : HeckeBetaOneDefined M ℓ) :
    laurentBaseChange L (x1FunctionField M) →+*
      laurentBaseChange L (x1x0FunctionFieldC ℚ M (M * ℓ)) where
  toFun x := ⟨qExpand L ℓ (x : LaurentSeries L), qExpand_mem_laurentBaseChange₁ ℓ h 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 ℓ) _ _)

variable (L) in

def heckeBetaOneBarOf (h : HeckeBetaOneDefined M ℓ) :
    laurentBaseChange L (x1FunctionField M) →ₐ[L]
      laurentBaseChange L (x1x0FunctionFieldC ℚ M (M * ℓ)) :=
  { heckeBetaOneBarRingHomOf L M ℓ h 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] }

@[simp]
theorem coe_heckeBetaOneBarOf (h : HeckeBetaOneDefined M ℓ) (x : laurentBaseChange L (x1FunctionField M)) :
    (heckeBetaOneBarOf L M ℓ h x : LaurentSeries L) = qExpand L ℓ (x : LaurentSeries L) :=
  rfl

open Classical in
variable (L) in

def heckeBetaOneBar :
    laurentBaseChange L (x1FunctionField M) →ₐ[L]
      laurentBaseChange L (x1x0FunctionFieldC ℚ M (M * ℓ)) :=
  if h : HeckeBetaOneDefined M ℓ then heckeBetaOneBarOf L M ℓ h else heckeAlphaOneBar L M ℓ

theorem heckeBetaOneBar_eq (h : HeckeBetaOneDefined M ℓ) :
    (heckeBetaOneBar L M ℓ) = heckeBetaOneBarOf L M ℓ h := by
  rw [heckeBetaOneBar, dif_pos h]

theorem heckeBetaOneBar_of_not (h : ¬ HeckeBetaOneDefined M ℓ) :
    (heckeBetaOneBar L M ℓ) = heckeAlphaOneBar L M ℓ := by
  rw [heckeBetaOneBar, dif_neg h]

theorem coe_heckeBetaOneBar (h : HeckeBetaOneDefined M ℓ) (x : laurentBaseChange L (x1FunctionField M)) :
    (heckeBetaOneBar L M ℓ x : LaurentSeries L) = qExpand L ℓ (x : LaurentSeries L) := by
  rw [heckeBetaOneBar_eq M ℓ h, coe_heckeBetaOneBarOf]

end DegeneracyMaps

section HeckePic0OneBar

variable (L) in

def HeckeAlphaOneBarIntegral : Prop :=
  (heckeAlphaOneBar L M ℓ).toRingHom.IsIntegral

variable (L) in

def HeckeBetaOneBarIntegral : Prop :=
  (heckeBetaOneBar L M ℓ).toRingHom.IsIntegral

variable {M ℓ}
variable (hα : HeckeAlphaOneBarIntegral L M ℓ) (hβ : HeckeBetaOneBarIntegral L M ℓ)
variable [HasPrincipalDivisors L (laurentBaseChange L (x1x0FunctionFieldC ℚ M (M * ℓ)))]

def heckeDivOneBar :
    Divisor L (laurentBaseChange L (x1FunctionField M)) →+
      Divisor L (laurentBaseChange L (x1FunctionField M)) :=
  Divisor.correspondence (heckeBetaOneBar L M ℓ) (heckeAlphaOneBar L M ℓ) hβ hα

def heckePic0OneBar
    (hFI : FundamentalIdentityAlong L (heckeBetaOneBar L M ℓ) hβ)
    (hfin : FiniteAlong L (heckeAlphaOneBar L M ℓ))
    (hN : NormFormulaAlong L (heckeAlphaOneBar L M ℓ) hfin) :
    Pic0 L (laurentBaseChange L (x1FunctionField M)) →+
      Pic0 L (laurentBaseChange L (x1FunctionField M)) :=
  Pic0.correspondence (heckeBetaOneBar L M ℓ) (heckeAlphaOneBar L M ℓ) hβ hα hFI hfin hN

def heckeDivOneBarTranspose :
    Divisor L (laurentBaseChange L (x1FunctionField M)) →+
      Divisor L (laurentBaseChange L (x1FunctionField M)) :=
  Divisor.correspondence (heckeAlphaOneBar L M ℓ) (heckeBetaOneBar L M ℓ) hα hβ

def heckePic0OneBarTranspose
    (hFI : FundamentalIdentityAlong L (heckeAlphaOneBar L M ℓ) hα)
    (hfin : FiniteAlong L (heckeBetaOneBar L M ℓ))
    (hN : NormFormulaAlong L (heckeBetaOneBar L M ℓ) hfin) :
    Pic0 L (laurentBaseChange L (x1FunctionField M)) →+
      Pic0 L (laurentBaseChange L (x1FunctionField M)) :=
  Pic0.correspondence (heckeAlphaOneBar L M ℓ) (heckeBetaOneBar L M ℓ) hα hβ hFI hfin hN

end HeckePic0OneBar

section Total

variable (L)

def HeckeInputsOneAlong : Prop :=
  ∃ (_ : HeckeBetaOneDefined M ℓ) (_ : HeckeAlphaOneBarIntegral L M ℓ) (hβ : HeckeBetaOneBarIntegral L M ℓ)
    (_ : HasPrincipalDivisors L (laurentBaseChange L (x1x0FunctionFieldC ℚ M (M * ℓ))))
    (hfin : FiniteAlong L (heckeAlphaOneBar L M ℓ)),
    FundamentalIdentityAlong L (heckeBetaOneBar L M ℓ) hβ ∧
      NormFormulaAlong L (heckeAlphaOneBar L M ℓ) hfin

open Classical in

def heckeOperatorOneAlong :
    Pic0 L (laurentBaseChange L (x1FunctionField M)) →+
      Pic0 L (laurentBaseChange L (x1FunctionField M)) :=
  if h : HeckeInputsOneAlong L M ℓ then
    haveI := h.snd.snd.snd.fst
    heckePic0OneBar h.snd.fst h.snd.snd.fst h.snd.snd.snd.snd.snd.1 h.snd.snd.snd.snd.fst
      h.snd.snd.snd.snd.snd.2
  else 0

variable {L M ℓ}

theorem heckeInputsOneAlong_intro (h0 : HeckeBetaOneDefined M ℓ)
    (hα : HeckeAlphaOneBarIntegral L M ℓ) (hβ : HeckeBetaOneBarIntegral L M ℓ)
    [hP : HasPrincipalDivisors L (laurentBaseChange L (x1x0FunctionFieldC ℚ M (M * ℓ)))]
    (hFI : FundamentalIdentityAlong L (heckeBetaOneBar L M ℓ) hβ)
    (hfin : FiniteAlong L (heckeAlphaOneBar L M ℓ))
    (hN : NormFormulaAlong L (heckeAlphaOneBar L M ℓ) hfin) : HeckeInputsOneAlong L M ℓ :=
  ⟨h0, hα, hβ, hP, hfin, hFI, hN⟩

theorem HeckeInputsOneAlong.betaOneDefined (h : HeckeInputsOneAlong L M ℓ) : HeckeBetaOneDefined M ℓ :=
  h.fst

theorem heckeOperatorOneAlong_eq (h0 : HeckeBetaOneDefined M ℓ)
    (hα : HeckeAlphaOneBarIntegral L M ℓ) (hβ : HeckeBetaOneBarIntegral L M ℓ)
    [HasPrincipalDivisors L (laurentBaseChange L (x1x0FunctionFieldC ℚ M (M * ℓ)))]
    (hFI : FundamentalIdentityAlong L (heckeBetaOneBar L M ℓ) hβ)
    (hfin : FiniteAlong L (heckeAlphaOneBar L M ℓ))
    (hN : NormFormulaAlong L (heckeAlphaOneBar L M ℓ) hfin) :
    heckeOperatorOneAlong L M ℓ = heckePic0OneBar hα hβ hFI hfin hN := by
  have h : HeckeInputsOneAlong L M ℓ := heckeInputsOneAlong_intro h0 hα hβ hFI hfin hN
  rw [heckeOperatorOneAlong, dif_pos h]

theorem heckeOperatorOneAlong_of_not (h : ¬ HeckeInputsOneAlong L M ℓ) :
    heckeOperatorOneAlong L M ℓ = 0 := by
  rw [heckeOperatorOneAlong, dif_neg h]

end Total

section ModularInstance

variable (M ℓ : ℕ) [NeZero ℓ]

example :
    x1FunctionFieldBar M →ₐ[AlgebraicClosure ℚ]
      laurentBaseChange (AlgebraicClosure ℚ) (x1x0FunctionFieldC ℚ M (M * ℓ)) :=
  heckeAlphaOneBar (AlgebraicClosure ℚ) M ℓ

example : JOne M →+ JOne M :=
  heckeOperatorOneAlong (AlgebraicClosure ℚ) M ℓ

end ModularInstance

end ModularCurve

end

Statements phrased using this module (85)