Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_HeckeModule.lean

definition module

Hecke algebra action on , guarded by commutation

For N\ge 1 (a NeZero N fence, so level 0 is unstatable) this module turns the project's individual Hecke operators on JZero N into a module structure over the project's Hecke algebra HeckeAlg. First, heckeOperatorBar N ℓ : Module.End ℤ (JZero N) is, for a prime \ell, the total operator heckeOperatorAlong (AlgebraicClosure ℚ) N ℓ of the imported module (so: the operator taken along \overline{\mathbb{Q}}, with the NeZero instance for \ell supplied from primality) read as a \mathbb{Z}-linear endomorphism; heckeOperatorBar_apply records that this is definitionally the same map. Second, HeckeOperatorsCommuteBar N is the proposition that these endomorphisms commute pairwise, for all pairs of primes; it is only defined here, never proved here. Third, from such a hypothesis h, isMulCommutative_adjoin_heckeOperatorBar gives that the \mathbb{Z}-subalgebra of Module.End ℤ (JZero N) generated by the range of heckeOperatorBar N is commutative, whence heckeEvalBarAux h is the MvPolynomial.aeval map into that subalgebra sending the variable at \ell to heckeOperatorBar N ℓ, and heckeEvalBar h : HeckeAlg →+* Module.End ℤ (JZero N) is its composite with the inclusion; heckeEvalBar_heckeGen and heckeEvalBar_C record the values on generators and on integer constants. (The use of MvPolynomial.aeval, MvPolynomial.C and MvPolynomial.constantCoeff on HeckeAlg exhibits it as the polynomial ring over \mathbb{Z} on the primes, with heckeGen ℓ the variable at \ell.) Finally heckeModuleBar N : Module HeckeAlg (JZero N) is a total definition by cases on the decidable-by-classical-choice proposition HeckeOperatorsCommuteBar N: if it holds, the action is Module.compHom along heckeEvalBar h; otherwise it is the junk action through t \mapsto its constant term, under which every heckeGen ℓ acts by 0. The remaining lemmas are the normal forms for computing with this dite: t \bullet x = heckeEvalBar h t x and heckeGen ℓ • x = heckeOperatorBar N ℓ x under h, the two junk-branch analogues, and heckeModuleBar_C_smul, which holds in both branches. Note that heckeModuleBar is a plain def (marked @[implicit_reducible]), not an instance.

Relation to Mathlib

Mathlib has no Hecke algebra or Hecke action on Jacobians of modular curves; HeckeAlg, heckeGen, JZero and heckeOperatorAlong are the project's own, imported from other definition modules. The construction itself is assembled from Mathlib's MvPolynomial.aeval, Algebra.adjoin, IsMulCommutative and Module.compHom.

Where it is used

This is the form in which the Hecke action on J_0(N) is fed to the later parts of the argument: statements about the Eisenstein ideal, the cuspidal class and specialisation are phrased against an explicit Module HeckeAlg (JZero N) binder and instantiated at heckeModuleBar N. Since nothing about commutation is proved here, consumers of the non-junk normal forms must carry HeckeOperatorsCommuteBar N as a hypothesis.

References

  1. B. Mazur, Modular curves and the Eisenstein ideal, Publications Mathématiques de l'IHÉS 47 (1977), 33–186
  2. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154
  3. 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_HeckeModule.lean

Imports

Imported by

Declarations

Source

import Definitions.Def_ModularCurve_HeckeOperatorTotal
import Definitions.Def_HeckeGalois_EichlerShimura

set_option autoImplicit false

noncomputable section

namespace ModularCurve

open AlgebraicCurve

section Operators

variable (N : ℕ) [NeZero N]

def heckeOperatorBar (ℓ : Nat.Primes) : Module.End ℤ (JZero N) :=
  haveI : NeZero (ℓ : ℕ) := ⟨ℓ.2.ne_zero⟩
  (heckeOperatorAlong (AlgebraicClosure ℚ) N ℓ).toIntLinearMap

theorem heckeOperatorBar_apply (ℓ : Nat.Primes) (x : JZero N) :
    heckeOperatorBar N ℓ x =
      (haveI : NeZero (ℓ : ℕ) := ⟨ℓ.2.ne_zero⟩; heckeOperatorAlong (AlgebraicClosure ℚ) N ℓ x) :=
  rfl

def HeckeOperatorsCommuteBar : Prop :=
  ∀ ℓ ℓ' : Nat.Primes,
    heckeOperatorBar N ℓ * heckeOperatorBar N ℓ' = heckeOperatorBar N ℓ' * heckeOperatorBar N ℓ

end Operators

section Eval

variable {N : ℕ} [NeZero N]

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

open scoped IsMulCommutative in

def heckeEvalBarAux (h : HeckeOperatorsCommuteBar N) :
    HeckeAlg →ₐ[ℤ] (Algebra.adjoin ℤ (Set.range (heckeOperatorBar N)) :
      Subalgebra ℤ (Module.End ℤ (JZero N))) :=
  haveI := isMulCommutative_adjoin_heckeOperatorBar h
  MvPolynomial.aeval fun ℓ =>
    (⟨heckeOperatorBar N ℓ, Algebra.subset_adjoin (Set.mem_range_self ℓ)⟩ :
      Algebra.adjoin ℤ (Set.range (heckeOperatorBar N)))

def heckeEvalBar (h : HeckeOperatorsCommuteBar N) : HeckeAlg →+* Module.End ℤ (JZero N) :=
  ((Algebra.adjoin ℤ (Set.range (heckeOperatorBar N))).val.comp (heckeEvalBarAux h)).toRingHom

theorem heckeEvalBar_apply (h : HeckeOperatorsCommuteBar N) (t : HeckeAlg) :
    heckeEvalBar h t = (heckeEvalBarAux h t : Module.End ℤ (JZero N)) :=
  rfl

open scoped IsMulCommutative in
theorem heckeEvalBarAux_heckeGen (h : HeckeOperatorsCommuteBar N) (ℓ : Nat.Primes) :
    heckeEvalBarAux h (heckeGen ℓ) =
      ⟨heckeOperatorBar N ℓ, Algebra.subset_adjoin (Set.mem_range_self ℓ)⟩ :=
  haveI := isMulCommutative_adjoin_heckeOperatorBar h
  MvPolynomial.aeval_X _ ℓ

theorem heckeEvalBar_heckeGen (h : HeckeOperatorsCommuteBar N) (ℓ : Nat.Primes) :
    heckeEvalBar h (heckeGen ℓ) = heckeOperatorBar N ℓ := by
  rw [heckeEvalBar_apply, heckeEvalBarAux_heckeGen]

theorem heckeEvalBar_C (h : HeckeOperatorsCommuteBar N) (a : ℤ) :
    heckeEvalBar h (MvPolynomial.C a) = (a : Module.End ℤ (JZero N)) := by
  rw [← MvPolynomial.algebraMap_eq, eq_intCast, map_intCast]

end Eval

section TheModule

variable (N : ℕ) [NeZero N]

open Classical in

@[implicit_reducible]
def heckeModuleBar : Module HeckeAlg (JZero N) :=
  if h : HeckeOperatorsCommuteBar N then Module.compHom (JZero N) (heckeEvalBar h)
  else Module.compHom (JZero N) (MvPolynomial.eval₂Hom (Int.castRingHom ℤ) (0 : Nat.Primes → ℤ))

variable {N}

theorem heckeModuleBar_smul_def (h : HeckeOperatorsCommuteBar N) (t : HeckeAlg) (x : JZero N) :
    (letI := heckeModuleBar N; t • x) = heckeEvalBar h t x := by
  have e : heckeModuleBar N = Module.compHom (JZero N) (heckeEvalBar h) := dif_pos h
  rw [e]
  rfl

theorem heckeModuleBar_heckeGen_smul (h : HeckeOperatorsCommuteBar N) (ℓ : Nat.Primes)
    (x : JZero N) : (letI := heckeModuleBar N; heckeGen ℓ • x) = heckeOperatorBar N ℓ x := by
  rw [heckeModuleBar_smul_def h, heckeEvalBar_heckeGen]

theorem heckeModuleBar_smul_of_not (h : ¬ HeckeOperatorsCommuteBar N) (t : HeckeAlg) (x : JZero N) :
    (letI := heckeModuleBar N; t • x) = MvPolynomial.constantCoeff t • x := by
  have e : heckeModuleBar N =
      Module.compHom (JZero N)
        (MvPolynomial.eval₂Hom (Int.castRingHom ℤ) (0 : Nat.Primes → ℤ)) :=
    dif_neg h
  rw [e]
  show (MvPolynomial.eval₂Hom (Int.castRingHom ℤ) (0 : Nat.Primes → ℤ) t) • x = _
  rw [MvPolynomial.eval₂Hom_zero_apply, eq_intCast, Int.cast_id]

theorem heckeModuleBar_heckeGen_smul_of_not (h : ¬ HeckeOperatorsCommuteBar N) (ℓ : Nat.Primes)
    (x : JZero N) : (letI := heckeModuleBar N; heckeGen ℓ • x) = 0 := by
  rw [heckeModuleBar_smul_of_not h, heckeGen, MvPolynomial.constantCoeff_X, zero_zsmul]

theorem heckeModuleBar_C_smul (a : ℤ) (x : JZero N) :
    (letI := heckeModuleBar N; (MvPolynomial.C a : HeckeAlg) • x) = a • x := by
  by_cases h : HeckeOperatorsCommuteBar N
  · rw [heckeModuleBar_smul_def h, heckeEvalBar_C, Module.End.intCast_apply]
  · rw [heckeModuleBar_smul_of_not h, MvPolynomial.constantCoeff_C]

end TheModule

end ModularCurve

end

Statements phrased using this module (372)

… and 222 more statements (search for the module name to find them).