Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_SpecializationWitness.lean

definition module

Commuting Hecke families and specialization witness data

Two layers are set up here over the free Hecke algebra \mathbb{T} = HeckeAlg = \mathbb{Z}[X_q : q \text{ prime}] (a multivariate polynomial ring indexed by Nat.Primes, with X_q written heckeGen q). First, a CommutingHeckeFamily on an additive commutative group J' is a structure with one data field, a family T : q \mapsto T_q of \mathbb{Z}-linear endomorphisms of J' indexed by the primes, and one proof field, that T_q and T_{q'} commute for all primes q, q'. From this the \mathbb{Z}-subalgebra of \operatorname{End}_{\mathbb{Z}}(J') generated by the range of T is shown commutative and given a CommRing structure; evaluating X_q \mapsto T_q then yields a ring homomorphism endHom : \mathbb{T} \to \operatorname{End}_{\mathbb{Z}}(J') with endHom_heckeGen recording X_q \mapsto T_q, and hence (via Module.compHom, as a reducible definition rather than a global instance) a \mathbb{T}-module structure on J' in which X_q \cdot y = T_q y.

Second, for a field extension L/K, a natural number p, a \mathbb{T}-module J carrying an action of \operatorname{Gal}(L/K) = L \simeq_{\alpha[K]} L by additive bijections, a valuation subring A \subseteq L and a prime \ell, the structure SpecializationWitnessData bundles: a carrier J' in Type with an additive group structure (registered as an instance), a commuting Hecke family fam on J', additive maps \mathrm{sp} : J \to J' and F : J' \to J', and five proof fields — \mathrm{sp}(X_q \cdot x) = T_q(\mathrm{sp}\, x) for every prime q (equivariance asserted only on the generators), \mathrm{sp}(\sigma \cdot x) = \mathrm{sp}\, x for \sigma in the image in \operatorname{Gal}(L/K) of the inertia subgroup of A, \mathrm{sp}(\sigma \cdot x) = F(\mathrm{sp}\, x) for every \sigma acting on the residue field of A by x \mapsto x^{\ell} within the decomposition group, injectivity of \mathrm{sp} on elements killed by a power of p, and the relation F^2 y - T_{\ell}(F y) + \ell y = 0 for all y \in J'. Note that A is not required to lie over \ell; that condition enters only where such data are produced.

Relation to Mathlib

Mathlib has no Hecke algebra or Hecke operator; HeckeAlg is simply a polynomial ring over \mathbb{Z} on symbols indexed by the primes, and the Hecke action is transported through Module.compHom. The inertia and decomposition subgroups of a valuation subring are Mathlib's; their image in \operatorname{Gal}(L/K) (inertiaSubgroupIn) and the Frobenius condition IsFrobeniusAt are the project's own.

Where it is used

These structures are the interface between a concrete special-fibre model carrying divisorial Hecke correspondences and a relative Frobenius — in the intended application the Jacobian of a modular curve reduced at a good prime \ell — and the existential statement SpecializationExists, from which the Eichler–Shimura clauses UnramifiedOutside and FrobeniusQuadratic for the p-torsion Galois representations attached to modular forms are deduced.

References

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

Imports

Imported by

Declarations

Source

import Definitions.Def_HeckeGalois_EichlerShimura

set_option autoImplicit false

noncomputable section

namespace ModularCurve

section Family

variable (J' : Type*) [AddCommGroup J']

structure CommutingHeckeFamily : Type _ where

  T : Nat.Primes → Module.End ℤ J'

  comm : ∀ q q' : Nat.Primes, Commute (T q) (T q')

variable {J'}

namespace CommutingHeckeFamily

variable (fam : CommutingHeckeFamily J')

theorem isMulCommutative_adjoin :
    IsMulCommutative (Algebra.adjoin ℤ (Set.range fam.T)) := by
  refine Algebra.isMulCommutative_adjoin ℤ ?_
  rintro x ⟨q, rfl⟩ y ⟨q', rfl⟩
  exact fam.comm q q'

instance commRing_adjoin : CommRing ↥(Algebra.adjoin ℤ (Set.range fam.T)) where
  __ := (inferInstance : Ring ↥(Algebra.adjoin ℤ (Set.range fam.T)))
  mul_comm a b := fam.isMulCommutative_adjoin.is_comm.comm a b

noncomputable def endHom : HeckeAlg →+* Module.End ℤ J' :=
  ((Algebra.adjoin ℤ (Set.range fam.T)).val).toRingHom.comp
    (MvPolynomial.aeval
      (fun q : Nat.Primes =>
        (⟨fam.T q, Algebra.subset_adjoin (Set.mem_range_self q)⟩ :
          Algebra.adjoin ℤ (Set.range fam.T))) :
      HeckeAlg →ₐ[ℤ] Algebra.adjoin ℤ (Set.range fam.T)).toRingHom

theorem endHom_heckeGen (q : Nat.Primes) : fam.endHom (heckeGen q) = fam.T q := by
  show ((Algebra.adjoin ℤ (Set.range fam.T)).val)
      ((MvPolynomial.aeval
        (fun q : Nat.Primes =>
          (⟨fam.T q, Algebra.subset_adjoin (Set.mem_range_self q)⟩ :
            Algebra.adjoin ℤ (Set.range fam.T))))
        (MvPolynomial.X q)) = fam.T q
  rw [MvPolynomial.aeval_X]
  rfl

@[reducible] noncomputable def module : Module HeckeAlg J' :=
  Module.compHom _ fam.endHom

theorem module_heckeGen_smul (q : Nat.Primes) (y : J') :
    letI := fam.module
    heckeGen q • y = fam.T q y := by
  letI := fam.module
  show fam.endHom (heckeGen q) y = fam.T q y
  rw [fam.endHom_heckeGen]

end CommutingHeckeFamily

end Family

section Packaging

variable {K L : Type*} [Field K] [Field L] [Algebra K L]
variable (p : ℕ) (J : Type*) [AddCommGroup J] [Module HeckeAlg J]
  [DistribMulAction (L ≃ₐ[K] L) J]

structure SpecializationWitnessData (A : ValuationSubring L) (ℓ : ℕ) (hℓ : ℓ.Prime) :
    Type _ where

  J' : Type

  [addCommGroup : AddCommGroup J']

  fam : CommutingHeckeFamily J'

  sp : J →+ J'

  F : J' →+ J'

  hecke_comm_gen : ∀ (q : Nat.Primes) (x : J), sp (heckeGen q • x) = fam.T q (sp x)

  inertia_comm : ∀ σ ∈ A.inertiaSubgroupIn K, ∀ x : J, sp (σ • x) = sp x

  frobenius_comm : ∀ σ : L ≃ₐ[K] L, A.IsFrobeniusAt σ ℓ → ∀ x : J, sp (σ • x) = F (sp x)

  injective_torsion : ∀ x : J, (∃ n : ℕ, p ^ n • x = 0) → sp x = 0 → x = 0

  relation : ∀ y : J', F (F y) - fam.T ⟨ℓ, hℓ⟩ (F y) + ℓ • y = 0

attribute [instance] SpecializationWitnessData.addCommGroup

end Packaging

end ModularCurve

Statements phrased using this module (0)

No statement module imports it directly (it is used through other definition modules or by proofs).