Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_FreyPackage_MazurAttachmentApparatus.lean

definition module

Hecke-ideal and residual matrix-representation data for Mazur's principle

Throughout, HeckeAlg is the polynomial ring \mathbb{Z}[T_\ell : \ell \text{ prime}] (with heckeGen \ell the variable T_\ell), JZero M is the degree-zero divisor class group of the base-changed modular function field of level M over \overline{\mathbb{Q}}, and mazurGaloisGroup abbreviates \mathrm{Aut}_{\mathbb{Q}}(\overline{\mathbb{Q}}) for \overline{\mathbb{Q}} = AlgebraicClosure β„š. Five predicates on an ideal \mathfrak m \subseteq HeckeAlg are introduced. EigenformIdealData P M g π”ͺ is a structure whose fields assert that \mathfrak m is maximal, contains p, is not eventually Eisenstein (no finite set S of primes with T_\ell - (\ell+1) \in \mathfrak m for all \ell \notin S), and satisfies T_\ell - b \in \mathfrak m whenever an integer b equals the \ell-th q-expansion coefficient of g. IdealGoodPrimeCurveCongruence p M W π”ͺ asserts T_\ell - a_\ell(W) \in \mathfrak m for every prime \ell of good reduction for the chosen integral Weierstrass model W with \ell \nmid M, \ell \neq p, where a_\ell(W) is the Frobenius trace of that model. IsAttachedMatrixRep π”ͺ Sρ ρmat says of a monoid homomorphism \rho into 2\times2 matrices over HeckeAlg/\mathfrak m (invertibility is not imposed) that for each prime \ell \notin S_\rho, each valuation subring A of \overline{\mathbb{Q}} lying over \ell and each \sigma that is a Frobenius at \ell for A, \operatorname{tr}\rho(\sigma) = T_\ell \bmod \mathfrak m and \det\rho(\sigma) = \ell \bmod \mathfrak m; adding openness of \ker\rho gives IsAttachedMatrixRepWithOpenKer. AttachedRepUnramifiedAtQ q π”ͺ quantifies over all such \rho with open kernel: if q is a unit mod \mathfrak m, then \rho is trivial on the inertia subgroup of every A over q and \det\rho(\mathrm{Frob}_q) = q. CurveAttachmentMatrixData P q N π”ͺ posits a matrix representation \rho and an element c with: the trace and determinant conditions at primes not dividing Nqp; irreducibility, in the form that the only \rho-stable submodules of (\mathbb{T}/\mathfrak m)^2 are \bot and \top; \rho(c)^2 = 1 and \det\rho(c) = -1; and a Galois number field F \subseteq \overline{\mathbb{Q}} with \mathrm{Gal}(\overline{\mathbb{Q}}/F) contained both in \ker\rho and in the subgroup fixing the \mathfrak m-torsion of JZero (N*q) pointwise.

MazurPerWitnessIdealSupplyFamily P q packages these: for every level N with q \nmid N, assuming the p-torsion representation of the Frey curve is irreducible in the sense of having no proper nonzero Galois-stable \mathbb{Z}/p-submodule and is unramified at q, then for every weight-two cusp form g on \Gamma_0(Nq) and maximal ideal \mathfrak m_w \ni p of the integral closure of \mathbb{Z} in \mathbb{C} exhibiting g as a congruent witness for the integral Frey model, with a_q(g)^2 = 1 (the project's IsNewAt q), and given the Hecke input and commutation hypotheses at level Nq, there is an ideal \mathfrak m satisfying all four conditions above together with non-vanishing of the \mathfrak m-torsion in JZero (N*q), the Hecke action being the one induced by the correspondences.

Relation to Mathlib

Mathlib has no abstract Hecke algebra, no residual Hecke eigenvalue ideals and no notion of a Galois representation attached to such an ideal; these are the project's own notions, built on Mathlib's MvPolynomial, Ideal.Quotient, Matrix (Fin 2) (Fin 2) and AlgEquiv.restrictNormalHom, and on the project's decomposition/inertia and Frobenius predicates for valuation subrings.

Where it is used

These predicates supply the input data for the formalisation of Mazur's principle, the level-lowering step that removes the auxiliary prime q from the level of a weight-two form congruent to the Frey curve; the conclusions recorded here (non-Eisenstein maximal ideal, congruences with the Frey Frobenius traces, unramifiedness at q of the attached residual representation, irreducibility and oddness, and non-vanishing of the \mathfrak m-torsion in the Jacobian) are exactly what that argument consumes.

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
  2. K. A. Ribet, Report on mod β„“ representations of Gal(QΜ„/Q), in: Motives, Proceedings of Symposia in Pure Mathematics 55, Part 2, American Mathematical Society, 1994, 639–676

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_FLTPrelim_FreyPackage
import Definitions.Def_FreyPackage_LevelRaising
import Definitions.Def_FreyPackage_GaloisRep
import Definitions.Def_GaloisRep_GlobalUnramifiedAt
import Definitions.Def_ModularCurve_HeckeModule
import Definitions.Def_ModularCurve_HeckeInputsAll
import Definitions.Def_ModularCurve_MazurPrincipleCore

set_option autoImplicit false

noncomputable section

namespace FreyPackage

open ModularCurve
open scoped CongruenceSubgroup

abbrev mazurGaloisGroup : Type := AlgebraicClosure β„š ≃ₐ[β„š] AlgebraicClosure β„š

structure EigenformIdealData (P : FreyPackage) (M : β„•) (g : CuspForm (CongruenceSubgroup.Gamma0 M) 2)
    (π”ͺ : Ideal HeckeAlg) : Prop where
  hmax : π”ͺ.IsMaximal
  hpmem : ((P.p : β„•) : HeckeAlg) ∈ π”ͺ
  heis : Β¬ IsEventuallyEisenstein π”ͺ
  heigen : βˆ€ (β„“ : Nat.Primes) (b : β„€), (algebraMap β„€ β„‚ b = ModularFormClass.qCoeff g β„“) β†’
    heckeGen β„“ - MvPolynomial.C b ∈ π”ͺ

def IdealGoodPrimeCurveCongruence (p M : β„•) (W : WeierstrassCurve β„€) (π”ͺ : Ideal HeckeAlg) : Prop :=
  βˆ€ (β„“ : β„•) (hβ„“ : β„“.Prime), W.IsGoodPrimeFor β„“ β†’ Β¬ β„“ ∣ M β†’ β„“ β‰  p β†’
    heckeGen βŸ¨β„“, hβ„“βŸ© - MvPolynomial.C (W.apOfModel β„“ : β„€) ∈ π”ͺ

def IsAttachedMatrixRep (π”ͺ : Ideal HeckeAlg) (Sρ : Finset β„•)
    (ρmat : mazurGaloisGroup β†’* Matrix (Fin 2) (Fin 2) (HeckeAlg β§Έ π”ͺ)) : Prop :=
  βˆ€ β„“ : β„•, (hβ„“ : β„“.Prime) β†’ β„“ βˆ‰ Sρ β†’
    βˆ€ A : ValuationSubring (AlgebraicClosure β„š), A.LiesOverPrime β„“ β†’
      βˆ€ Οƒ : AlgebraicClosure β„š ≃ₐ[β„š] AlgebraicClosure β„š, A.IsFrobeniusAt Οƒ β„“ β†’
        Ideal.Quotient.mk π”ͺ (heckeGen βŸ¨β„“, hβ„“βŸ©) = (ρmat Οƒ).trace ∧
        Ideal.Quotient.mk π”ͺ ((β„“ : HeckeAlg)) = (ρmat Οƒ).det

def IsAttachedMatrixRepWithOpenKer (π”ͺ : Ideal HeckeAlg) (Sρ : Finset β„•)
    (ρmat : mazurGaloisGroup β†’* Matrix (Fin 2) (Fin 2) (HeckeAlg β§Έ π”ͺ)) : Prop :=
  IsAttachedMatrixRep π”ͺ Sρ ρmat ∧ IsOpen (ρmat.ker : Set mazurGaloisGroup)

def AttachedRepUnramifiedAtQ (q : β„•) (π”ͺ : Ideal HeckeAlg) : Prop :=
  βˆ€ (Sρ : Finset β„•) (ρmat : mazurGaloisGroup β†’* Matrix (Fin 2) (Fin 2) (HeckeAlg β§Έ π”ͺ)),
    IsAttachedMatrixRepWithOpenKer π”ͺ Sρ ρmat β†’ IsUnit ((q : β„•) : HeckeAlg β§Έ π”ͺ) β†’
      βˆ€ A : ValuationSubring (AlgebraicClosure β„š), A.LiesOverPrime q β†’
        (βˆ€ Οƒ ∈ A.inertiaSubgroupIn β„š, ρmat Οƒ = 1) ∧
        βˆ€ frob : mazurGaloisGroup, A.IsFrobeniusAt frob q β†’ (ρmat frob).det = ((q : β„•) : HeckeAlg β§Έ π”ͺ)

def CurveAttachmentMatrixData (P : FreyPackage) (q N : β„•) [NeZero q] [NeZero N]
    [Module HeckeAlg (JZero (N * q))] (π”ͺ : Ideal HeckeAlg) : Prop :=
  βˆƒ (ρmat : mazurGaloisGroup β†’* Matrix (Fin 2) (Fin 2) (HeckeAlg β§Έ π”ͺ))
    (c : mazurGaloisGroup),
    (βˆ€ β„“ : β„•, (hβ„“ : β„“.Prime) β†’ β„“ βˆ‰ ((N * q) * P.p).primeFactors β†’
      βˆ€ A : ValuationSubring (AlgebraicClosure β„š), A.LiesOverPrime β„“ β†’
        βˆ€ Οƒ : AlgebraicClosure β„š ≃ₐ[β„š] AlgebraicClosure β„š, A.IsFrobeniusAt Οƒ β„“ β†’
          (ρmat Οƒ).trace = Ideal.Quotient.mk π”ͺ (heckeGen βŸ¨β„“, hβ„“βŸ©))
    ∧ (βˆ€ β„“ : β„•, β„“.Prime β†’ β„“ βˆ‰ ((N * q) * P.p).primeFactors β†’
      βˆ€ A : ValuationSubring (AlgebraicClosure β„š), A.LiesOverPrime β„“ β†’
        βˆ€ Οƒ : AlgebraicClosure β„š ≃ₐ[β„š] AlgebraicClosure β„š, A.IsFrobeniusAt Οƒ β„“ β†’
          (ρmat Οƒ).det = ((β„“ : β„•) : HeckeAlg β§Έ π”ͺ))
    ∧ (βˆ€ Wsub : Submodule (HeckeAlg β§Έ π”ͺ) (Fin 2 β†’ HeckeAlg β§Έ π”ͺ),
        (βˆ€ g, βˆ€ v ∈ Wsub, (ρmat g).mulVec v ∈ Wsub) β†’ Wsub = βŠ₯ ∨ Wsub = ⊀)
    ∧ ρmat c * ρmat c = 1
    ∧ (ρmat c).det = -1
    ∧ βˆƒ (F : Type) (_ : Field F) (_ : NumberField F) (_ : IsGalois β„š F)
        (_ : Algebra F (AlgebraicClosure β„š)) (_ : IsScalarTower β„š F (AlgebraicClosure β„š)),
        (AlgEquiv.restrictNormalHom (F := β„š) (K₁ := AlgebraicClosure β„š) F).ker ≀ ρmat.ker
        ∧ (AlgEquiv.restrictNormalHom (F := β„š) (K₁ := AlgebraicClosure β„š) F).ker ≀
             fixingSubgroup mazurGaloisGroup
               (heckeTorsion (JZero (N * q)) π”ͺ : Set (JZero (N * q)))

def MazurPerWitnessIdealSupplyFamily (P : FreyPackage) (q : β„•) [NeZero q] : Prop :=
  βˆ€ (N : β„•) [NeZero N], Β¬ q ∣ N β†’
    WeierstrassCurve.Affine.Point.GaloisRepIsIrreducible (K := AlgebraicClosure β„š) β„š P.freyCurve P.p β†’
    GlobalGaloisRep.IsUnramifiedAt P.freyGaloisRep q β†’
    βˆ€ (g : CuspForm (CongruenceSubgroup.Gamma0 (N * q)) 2) (π”ͺw : Ideal (integralClosure β„€ β„‚)),
      P.IsCongruentWitness (N * q) g (freyCurveInt P) π”ͺw β†’ g.IsNewAt q β†’
      HeckeInputsAll (N * q) β†’ HeckeOperatorsCommuteBar (N * q) β†’
      βˆƒ π”ͺ : Ideal HeckeAlg,
        P.EigenformIdealData (N * q) g π”ͺ ∧
        IdealGoodPrimeCurveCongruence P.p (N * q) (freyCurveInt P) π”ͺ ∧
        AttachedRepUnramifiedAtQ q π”ͺ ∧
        (letI := heckeModuleBar (N * q)
         P.CurveAttachmentMatrixData q N π”ͺ ∧ heckeTorsion (JZero (N * q)) π”ͺ β‰  βŠ₯)

end FreyPackage

end

Statements phrased using this module (2)