Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_HeckeCarrier.lean

definition module

Away-ideals of the Hecke algebra; character-lattice Hecke operators

Throughout, the Hecke algebra is the polynomial ring \mathbb{T} = \mathrm{MvPolynomial}\ \mathrm{Nat.Primes}\ \mathbb{Z}, with \mathrm{heckeGen}\ \ell the variable indexed by a prime \ell. For a finite set S of primes and an ideal \mathfrak m \subseteq \mathbb{T}, ModularCurve.awayIdeal is the ideal generated by the union of two sets: the images in \mathbb{T} of those natural numbers n with n \in \mathfrak m, and those elements \mathrm{heckeGen}\ \ell - C(b), with \ell \notin S and b \in \mathbb{Z}, that lie in \mathfrak m. Accompanying lemmas record that this ideal is contained in \mathfrak m and that each of the two kinds of generator indeed belongs to it. HasAwaySupport S π”ͺ M, for a \mathbb{T}-module M, is the statement that the submodule (\mathrm{awayIdeal}\ S\ \mathfrak m) \cdot M is not all of M, i.e. that the coinvariants M/(\mathrm{awayIdeal}\ S\ \mathfrak m)M are nonzero. anemicInclusion S is the ring map \mathbb{Z}[X_\ell : \ell \notin S] \to \mathbb{T} renaming variables along the inclusion of the subtype, so that X_\ell \mapsto \mathrm{heckeGen}\ \ell, and anemicContraction S π”ͺ is the contraction of \mathfrak m along it, membership being equivalent to membership of the image in \mathfrak m.

The second part works with a degeneracy datum D on finite index sets E, V and a HeckeData H for it, which supplies commuting integer matrices T_\ell on E and T^V_\ell on V. First, \mathrm{heckeDivisorAction}\ T^{\mathrm{t}} is the map x \mapsto T x. The structure LatticeHyp carries integers n_\ell and n^V_\ell together with the assertions, as fields, that every row sum of T_\ell^{\mathrm t} equals n_\ell and every row sum of (T^V_\ell)^{\mathrm t} equals n^V_\ell β€” that is, all column sums of T_\ell, resp. T^V_\ell, are constant, which is what makes the matrix action preserve degree-zero functions. Given such data, latticeOp and latticeOpV are the resulting \mathbb{Z}-linear endomorphisms of the degree-zero lattices \mathrm{characterLattice}\ E and \mathrm{characterLattice}\ V; their coordinates are given by x \mapsto T_\ell x, resp. x \mapsto T^V_\ell x, and they commute pairwise over all primes, by the commutation fields of HeckeData.

Relation to Mathlib

Mathlib supplies the polynomial rings, ideal comap and Submodule smul used here; the Hecke algebra as a free polynomial ring on the primes, the away-ideals, the away-support predicate, and the character-lattice Hecke operators attached to a degeneracy datum are the project's own notions.

Where it is used

This vocabulary serves the character-group side of Ribet's interchange of character groups in the level-lowering argument: the lattices carrying latticeOp and latticeOpV play the role of the character groups of the Jacobians attached to the two levels at an auxiliary prime, while the away-ideals and the anemic subalgebra isolate the Hecke operators at primes outside a bad set, at which the comparison is made.

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, Β§3
  2. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154, Β§4

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Definitions.Def_ModularCurve_ComponentGroupHecke
import Definitions.Def_HeckeGalois_EichlerShimura
import Definitions.Def_CerednikDrinfeld_Ribbon

set_option autoImplicit false

noncomputable section

namespace ModularCurve

def awayIdeal (S : Finset Nat.Primes) (π”ͺ : Ideal HeckeAlg) : Ideal HeckeAlg :=
  Ideal.span ({t | βˆƒ n : β„•, (n : HeckeAlg) ∈ π”ͺ ∧ t = n} βˆͺ
    {t | βˆƒ β„“ : Nat.Primes, β„“ βˆ‰ S ∧ βˆƒ b : β„€,
      heckeGen β„“ - MvPolynomial.C b ∈ π”ͺ ∧ t = heckeGen β„“ - MvPolynomial.C b})

theorem awayIdeal_le (S : Finset Nat.Primes) (π”ͺ : Ideal HeckeAlg) : awayIdeal S π”ͺ ≀ π”ͺ := by
  refine Ideal.span_le.2 ?_
  rintro t (⟨n, hn, rfl⟩ | βŸ¨β„“, -, b, hb, rfl⟩)
  Β· exact hn
  Β· exact hb

theorem natCast_mem_awayIdeal {S : Finset Nat.Primes} {π”ͺ : Ideal HeckeAlg} {n : β„•}
    (hn : (n : HeckeAlg) ∈ π”ͺ) : (n : HeckeAlg) ∈ awayIdeal S π”ͺ :=
  Ideal.subset_span (Or.inl ⟨n, hn, rfl⟩)

theorem heckeGen_sub_C_mem_awayIdeal {S : Finset Nat.Primes} {π”ͺ : Ideal HeckeAlg} {β„“ : Nat.Primes}
    (hβ„“ : β„“ βˆ‰ S) {b : β„€} (hb : heckeGen β„“ - MvPolynomial.C b ∈ π”ͺ) :
    heckeGen β„“ - MvPolynomial.C b ∈ awayIdeal S π”ͺ :=
  Ideal.subset_span (Or.inr βŸ¨β„“, hβ„“, b, hb, rfl⟩)

def HasAwaySupport (S : Finset Nat.Primes) (π”ͺ : Ideal HeckeAlg) (M : Type*) [AddCommGroup M]
    [Module HeckeAlg M] : Prop :=
  (awayIdeal S π”ͺ β€’ ⊀ : Submodule HeckeAlg M) β‰  ⊀

def anemicInclusion (S : Finset Nat.Primes) :
    MvPolynomial {β„“ : Nat.Primes // β„“ βˆ‰ S} β„€ β†’+* HeckeAlg :=
  (MvPolynomial.rename (Subtype.val : {β„“ : Nat.Primes // β„“ βˆ‰ S} β†’ Nat.Primes)).toRingHom

theorem anemicInclusion_X (S : Finset Nat.Primes) (β„“ : {β„“ : Nat.Primes // β„“ βˆ‰ S}) :
    anemicInclusion S (MvPolynomial.X β„“) = heckeGen β„“.1 :=
  MvPolynomial.rename_X _ β„“

def anemicContraction (S : Finset Nat.Primes) (π”ͺ : Ideal HeckeAlg) :
    Ideal (MvPolynomial {β„“ : Nat.Primes // β„“ βˆ‰ S} β„€) :=
  π”ͺ.comap (anemicInclusion S)

theorem mem_anemicContraction {S : Finset Nat.Primes} {π”ͺ : Ideal HeckeAlg}
    {t : MvPolynomial {β„“ : Nat.Primes // β„“ βˆ‰ S} β„€} :
    t ∈ anemicContraction S π”ͺ ↔ anemicInclusion S t ∈ π”ͺ :=
  Ideal.mem_comap

end ModularCurve

namespace CerednikDrinfeld

open ModularCurve

variable {E V : Type*} [Fintype E] [Fintype V] [DecidableEq V] {D : DegeneracyData E V}

theorem heckeDivisorAction_transpose (T : Matrix E E β„€) (x : E β†’ β„€) :
    heckeDivisorAction T.transpose x = T.mulVec x := by
  ext j
  simp [heckeDivisorAction_apply, Matrix.mulVec, dotProduct, Matrix.transpose_apply]

namespace HeckeData

variable (H : HeckeData D)

structure LatticeHyp (H : HeckeData D) where

  n : Nat.Primes β†’ β„€

  colSum : βˆ€ β„“, HeckeRowSums (H.T β„“).transpose (n β„“)

  nV : Nat.Primes β†’ β„€

  colSumV : βˆ€ β„“, HeckeRowSums (H.Tv β„“).transpose (nV β„“)

variable (h : H.LatticeHyp)

def latticeOp (β„“ : Nat.Primes) : characterLattice E β†’β‚—[β„€] characterLattice E :=
  heckeCharacterAction (H.T β„“).transpose (h.colSum β„“)

theorem coe_latticeOp (β„“ : Nat.Primes) (x : characterLattice E) :
    (H.latticeOp h β„“ x : E β†’ β„€) = (H.T β„“).mulVec x :=
  heckeDivisorAction_transpose _ _

theorem latticeOp_comm (β„“ β„“' : Nat.Primes) (x : characterLattice E) :
    H.latticeOp h β„“ (H.latticeOp h β„“' x) = H.latticeOp h β„“' (H.latticeOp h β„“ x) := by
  apply Subtype.ext
  simp only [coe_latticeOp, Matrix.mulVec_mulVec, (H.comm β„“ β„“').eq]

def latticeOpV (β„“ : Nat.Primes) : characterLattice V β†’β‚—[β„€] characterLattice V :=
  heckeCharacterAction (H.Tv β„“).transpose (h.colSumV β„“)

theorem coe_latticeOpV (β„“ : Nat.Primes) (x : characterLattice V) :
    (H.latticeOpV h β„“ x : V β†’ β„€) = (H.Tv β„“).mulVec x :=
  heckeDivisorAction_transpose _ _

theorem latticeOpV_comm (β„“ β„“' : Nat.Primes) (x : characterLattice V) :
    H.latticeOpV h β„“ (H.latticeOpV h β„“' x) = H.latticeOpV h β„“' (H.latticeOpV h β„“ x) := by
  apply Subtype.ext
  simp only [coe_latticeOpV, Matrix.mulVec_mulVec, (H.commv β„“ β„“').eq]

end HeckeData

end CerednikDrinfeld

Statements phrased using this module (1)