Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_JZeroTateModule.lean

definition module

Rational Tate module, Hecke action, rank-two cyclotomic predicate

Throughout, p is a prime and J an abelian group; \mathbb{T} = HeckeAlg is the polynomial ring \mathbb{Z}[X_\ell : \ell \text{ prime}] on the set of primes, and TateModule p J is the group of sequences (x_n)_{n\in\mathbb{N}} in J with p^n x_n = 0 and p\,x_{n+1} = x_n, a \mathbb{Z}_p-module. First, for J a \mathbb{T}-module, tateHeckeRep upgrades the monoid homomorphism TateModule.rep to a ring homomorphism \mathbb{T} \to \operatorname{End}_{\mathbb{Z}_p}(T_pJ), acting coordinatewise by t\cdot(x_n) = (t\cdot x_n); the two accompanying lemmas record this action componentwise. Next, RationalTateModule p J is V = \mathbb{Q}_p \otimes_{\mathbb{Z}_p} T_pJ. For a monoid G acting distributively on J, rationalGaloisRep is the composite of TateModule.rep with base change along \mathbb{Z}_p \to \mathbb{Q}_p, a monoid homomorphism G \to \operatorname{End}_{\mathbb{Q}_p}(V) sending g to a \otimes x \mapsto a \otimes g\cdot x; similarly rationalHeckeRep is the ring homomorphism \mathbb{T} \to \operatorname{End}_{\mathbb{Q}_p}(V) obtained from tateHeckeRep by base change. The \mathbb{Q}_p-Hecke algebra rationalHeckeAlgebra is the \mathbb{Q}_p-subalgebra A \subseteq \operatorname{End}_{\mathbb{Q}_p}(V) generated by the image of rationalHeckeRep, and each \mathbb{T}-operator lies in it.

The main predicate RationalRankTwoCyclotomicOf N p J, formulated for an extension L/K of fields with J carrying actions of \mathbb{T} and of L \simeq_K L, asserts the existence of a basis b_0, b_1 of V as an A-module indexed by Fin 2 such that for every prime \ell \nmid Np, every valuation subring A' of L with LiesOverPrime \ell and every \sigma : L \simeq_K L that is a Frobenius at \ell for A' in the sense of IsFrobeniusAt, the four A-coordinates c_{ji} = (b.\mathrm{repr}(\sigma b_j))_i of the images satisfy c_{00}c_{11} - c_{10}c_{01} = \ell in A. Thus the assertion is freeness of rank two over A together with a cyclotomic determinant condition stated as an identity in the coordinates of \sigma b_0, \sigma b_1; no commutation between the Galois and Hecke actions is imposed, so \sigma need not act A-linearly. Finally RationalRankTwoCyclotomic M p is the instance K = \mathbb{Q}, L = \overline{\mathbb{Q}}, N = M and J = JZero M, the degree-zero divisor class group of the level-M modular curve in the project's Laurent-series model, with its arithmetic Galois action and a given \mathbb{T}-module structure.

Relation to Mathlib

Mathlib has neither Tate modules nor Hecke algebras in this form; TateModule and HeckeAlg are the project's own, while the base-change homomorphisms (Module.End.baseChangeHom), Algebra.adjoin and Module.Basis are Mathlib's.

Where it is used

The rational Tate module with its Hecke and Galois actions is the vehicle for the Eichler–Shimura input: the predicate RationalRankTwoCyclotomic expresses, for a chosen model of J_0(M), that V_p J_0(M) is free of rank two over the \mathbb{Q}_p-Hecke algebra with cyclotomic determinant on Frobenius elements, from which two-dimensional Galois representations attached to Hecke eigensystems occurring in J_0(M) are obtained.

References

  1. G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Publications of the Mathematical Society of Japan 11, Princeton University Press, 1971, Chapter 7
  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_JZeroTateModule.lean

Imports

Imported by

Declarations

Source

import Definitions.Def_ModularCurve_ArithmeticGalois
import Definitions.Def_HeckeGalois_EichlerShimura
import Definitions.Def_EllipticCurve_TateModule
import Mathlib.LinearAlgebra.TensorProduct.Tower ↗
import Mathlib.Algebra.Algebra.Subalgebra.Lattice ↗
import Mathlib.LinearAlgebra.Basis.Defs ↗

set_option autoImplicit false

noncomputable section

open scoped TensorProduct

namespace ModularCurve

section Integral

variable (p : ℕ) [Fact p.Prime] (J : Type) [AddCommGroup J] [Module HeckeAlg J]

def tateHeckeRep : HeckeAlg →+* Module.End ℤ_[p] (TateModule p J) where
  toMonoidHom := TateModule.rep p J HeckeAlg
  map_zero' := by
    refine LinearMap.ext fun x => Subtype.ext (funext fun n => ?_)
    show (0 : HeckeAlg) • (x : ℕ → J) n = 0
    exact zero_smul HeckeAlg ((x : ℕ → J) n)
  map_add' s t := by
    refine LinearMap.ext fun x => Subtype.ext (funext fun n => ?_)
    show (s + t) • (x : ℕ → J) n = s • (x : ℕ → J) n + t • (x : ℕ → J) n
    exact add_smul s t ((x : ℕ → J) n)

theorem tateHeckeRep_apply (t : HeckeAlg) :
    tateHeckeRep p J t = TateModule.rep p J HeckeAlg t :=
  rfl

theorem coe_tateHeckeRep_apply_apply (t : HeckeAlg) (x : TateModule p J) (n : ℕ) :
    ((tateHeckeRep p J t x : TateModule p J) : ℕ → J) n = t • (x : ℕ → J) n :=
  rfl

end Integral

section Rational

variable (p : ℕ) [Fact p.Prime] (J : Type) [AddCommGroup J]

abbrev RationalTateModule : Type :=
  ℚ_[p] ⊗[ℤ_[p]] TateModule p J

def rationalGaloisRep (G : Type) [Monoid G] [DistribMulAction G J] :
    G →* Module.End ℚ_[p] (RationalTateModule p J) :=
  (Module.End.baseChangeHom ℤ_[p] ℚ_[p] (TateModule p J) :
      Module.End ℤ_[p] (TateModule p J) →* Module.End ℚ_[p] (RationalTateModule p J)).comp
    (TateModule.rep p J G)

theorem rationalGaloisRep_apply (G : Type) [Monoid G] [DistribMulAction G J] (g : G) :
    rationalGaloisRep p J G g = (TateModule.rep p J G g).baseChange ℚ_[p] :=
  rfl

theorem rationalGaloisRep_tmul (G : Type) [Monoid G] [DistribMulAction G J] (g : G) (a : ℚ_[p])
    (x : TateModule p J) :
    rationalGaloisRep p J G g (a ⊗ₜ x) = a ⊗ₜ TateModule.rep p J G g x :=
  rfl

variable [Module HeckeAlg J]

def rationalHeckeRep : HeckeAlg →+* Module.End ℚ_[p] (RationalTateModule p J) :=
  (Module.End.baseChangeHom ℤ_[p] ℚ_[p] (TateModule p J)).toRingHom.comp (tateHeckeRep p J)

theorem rationalHeckeRep_apply (t : HeckeAlg) :
    rationalHeckeRep p J t = (tateHeckeRep p J t).baseChange ℚ_[p] :=
  rfl

theorem rationalHeckeRep_tmul (t : HeckeAlg) (a : ℚ_[p]) (x : TateModule p J) :
    rationalHeckeRep p J t (a ⊗ₜ x) = a ⊗ₜ tateHeckeRep p J t x :=
  rfl

def rationalHeckeAlgebra : Subalgebra ℚ_[p] (Module.End ℚ_[p] (RationalTateModule p J)) :=
  Algebra.adjoin ℚ_[p] (Set.range (rationalHeckeRep p J))

theorem rationalHeckeRep_mem_rationalHeckeAlgebra (t : HeckeAlg) :
    rationalHeckeRep p J t ∈ rationalHeckeAlgebra p J :=
  Algebra.subset_adjoin (Set.mem_range_self t)

end Rational

section Predicate

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

def RationalRankTwoCyclotomicOf : Prop :=
  ∃ b : Module.Basis (Fin 2) (rationalHeckeAlgebra p J) (RationalTateModule p J),
    ∀ ℓ : ℕ, ℓ.Prime → ¬ ℓ ∣ N * p →
      ∀ A' : ValuationSubring L, A'.LiesOverPrime ℓ →
        ∀ σ : L ≃ₐ[K] L, A'.IsFrobeniusAt σ ℓ →
          (b.repr (rationalGaloisRep p J (L ≃ₐ[K] L) σ (b 0))) 0
              * (b.repr (rationalGaloisRep p J (L ≃ₐ[K] L) σ (b 1))) 1
            - (b.repr (rationalGaloisRep p J (L ≃ₐ[K] L) σ (b 1))) 0
              * (b.repr (rationalGaloisRep p J (L ≃ₐ[K] L) σ (b 0))) 1
            = (ℓ : rationalHeckeAlgebra p J)

end Predicate

section ModularInstance

def RationalRankTwoCyclotomic (M p : ℕ) [Fact p.Prime] [Module HeckeAlg (JZero M)] : Prop :=
  RationalRankTwoCyclotomicOf (K := ℚ) (L := AlgebraicClosure ℚ) M p (JZero M)

end ModularInstance

end ModularCurve

end

Statements phrased using this module (66)