Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_CuspForm_HeckeGaloisRepDatum.lean

definition module

Hecke–Galois representation datum at a residual eigensystem

This module defines the structure CuspForm.HeckeGaloisRepDatum N S 𝒪 θ T, a bundle of hypotheses about a ring T playing the role of a localised Hecke algebra together with a two-dimensional Galois representation over it. The parameters are: a level N\ge 1; a set S of primes to be excluded; the Hecke algebra \mathbb T= heckeAlgebra N 2 S, which is the \mathbb Z-subalgebra of \operatorname{End}_{\mathbb C} S_2(\Gamma_0(N)) generated by the operators T_\ell for primes \ell\nmid N, \ell\notin S, and U_q for primes q\mid N, q\notin S; a complete discrete valuation ring \mathcal O (a domain, adically complete for its maximal ideal); a ring homomorphism \theta\colon\mathbb T\to\mathcal O/\mathfrak m_{\mathcal O}, i.e. a residual system of Hecke eigenvalues; and a commutative ring T assumed local, noetherian, \mathfrak m_T-adically complete, an \mathcal O-algebra along a local homomorphism, and finite and free as an \mathcal O-module. The fields are: a ring homomorphism \pi\colon\mathbb T\to T; residue_π, saying that the residue of \pi(t) equals the image of \theta(t) under the induced map of residue fields; adjoin_range_π, that the image of \pi generates T as an \mathcal O-algebra; exists_point, that every \chi\colon\mathbb T\to\mathcal O reducing to \theta factors as \chi=\psi\circ\pi for some \mathcal O-algebra map \psi\colon T\to\mathcal O; residue_surjective, that \mathcal O\to T\to T/\mathfrak m_T is surjective, so T has residue field that of \mathcal O; a representation ρ : GaloisRepAdic T, namely a free rank-two T-module V with a monoid homomorphism from \operatorname{Aut}_{\mathbb Q}(\overline{\mathbb Q}) to \operatorname{End}_T V satisfying the adic continuity condition that, for each n, some finite extension of \mathbb Q acts trivially modulo \mathfrak m_T^n V; charpoly_frob, asserting that for every prime \ell with \ell\nmid N, \ell\notin S, every valuation subring A of \overline{\mathbb Q} lying over \ell and every \sigma that is a Frobenius at \ell for A, the characteristic polynomial of \rho(\sigma) is X^2-\pi(T_\ell)X+\ell; and residual_absIrr, that the reduction \kappa(T)\otimes_T V is irreducible after base change to an algebraic closure of the residue field. Nothing is constructed: the structure records the Eichler–Shimura–Deligne input and the ring-theoretic properties of the Hecke side as hypotheses.

Relation to Mathlib

Mathlib has no Hecke algebra acting on cusp forms nor any notion of adic Galois representation; both CuspForm.heckeAlgebra and GaloisRepAdic, and hence this datum, are the project's own definitions built on Mathlib's CuspForm, CongruenceSubgroup.Gamma0, ValuationSubring and local-ring API.

Where it is used

A datum of this kind is the standing hypothesis of the modularity-lifting theorems: the surjectivity of the map from a deformation ring to T, the application of the numerical criterion at T, and the deduction that \mathcal O-points of the deformation ring come from Hecke eigensystems. Local conditions at p and at primes of S, and the comparison of the residual representation with that of an elliptic curve, are imposed separately, so this structure is free of both.

References

  1. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154, §3
  2. H. Carayol, Formes modulaires et représentations galoisiennes à valeurs dans un anneau local complet, in: p-adic Monodromy and the Birch and Swinnerton-Dyer Conjecture, Contemporary Mathematics 165, American Mathematical Society, 1994, 213–237
  3. A. Wiles, Modular elliptic curves and Fermat's Last Theorem, Annals of Mathematics 141 (1995), 443–551

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

Imports

Imported by

Declarations

Source

import Definitions.Def_GaloisRep_Adic
import Definitions.Def_CuspForm_HeckeAlgebra

open Polynomial

namespace CuspForm

structure HeckeGaloisRepDatum (N : ℕ) [NeZero N] (S : Set ℕ)
    (𝒪 : Type) [CommRing 𝒪] [IsDomain 𝒪] [IsDiscreteValuationRing 𝒪]
    [IsAdicComplete (IsLocalRing.maximalIdeal 𝒪) 𝒪]
    (θ : heckeAlgebra N 2 S →+* IsLocalRing.ResidueField 𝒪)
    (T : Type) [CommRing T] [IsLocalRing T] [IsNoetherianRing T]
    [IsAdicComplete (IsLocalRing.maximalIdeal T) T] [Algebra 𝒪 T] [IsLocalHom (algebraMap 𝒪 T)]
    [Module.Finite 𝒪 T] [Module.Free 𝒪 T] : Type 1 where

  π : heckeAlgebra N 2 S →+* T

  residue_π : ∀ t : heckeAlgebra N 2 S,
    IsLocalRing.residue T (π t) = IsLocalRing.ResidueField.map (algebraMap 𝒪 T) (θ t)

  adjoin_range_π : Algebra.adjoin 𝒪 (Set.range π) = ⊤

  exists_point : ∀ χ : heckeAlgebra N 2 S →+* 𝒪,
    (∀ t : heckeAlgebra N 2 S, IsLocalRing.residue 𝒪 (χ t) = θ t) →
      ∃ ψ : T →ₐ[𝒪] 𝒪, ∀ t : heckeAlgebra N 2 S, ψ (π t) = χ t

  residue_surjective : Function.Surjective (IsLocalRing.residue T ∘ algebraMap 𝒪 T)

  ρ : GaloisRepAdic T

  charpoly_frob : ∀ (ℓ : ℕ) (hℓ : ℓ.Prime) (hℓN : ¬ ℓ ∣ N) (hℓS : ℓ ∉ S),
    ∀ A : ValuationSubring (AlgebraicClosure ℚ), A.LiesOverPrime ℓ →
      ∀ σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ, A.IsFrobeniusAt σ ℓ →
        LinearMap.charpoly (ρ.ρ σ) = X ^ 2 - C (π (heckeAlgebra.T hℓ hℓN hℓS)) * X + C ((ℓ : T))

  residual_absIrr : ρ.residual.IsAbsolutelyIrreducible

end CuspForm

Statements phrased using this module (112)