Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_JZeroNeronAtPDataSameIdeal.lean

definition module

Néron datum at with same-ideal level detection

Fix N\ge 1 and a prime q with q\nmid N, and a valuation subring A of \overline{\mathbb Q} lying over q (i.e. q is a non-unit of A). The structure ModularCurve.JZeroNeronAtPDataSameIdeal extends ModularCurve.JZeroNeronAtPData — hence carries, verbatim, all the data and axioms of an at-q Néron datum for J_0(Nq): the filtration \mathrm{toric}\le\mathrm{fin}\le\mathrm{finPart} inside the m-torsion of JZero (N*q) with its compatibilities in m, its stability under the Hecke algebra and under the decomposition group at A, the inertia clauses, the homomorphism to J_0(N)\times J_0(N) with prescribed kernel and image, the finite Hecke-module \Phi with its specialisation maps and Eisenstein property, the Frobenius and monodromy clauses, the Raynaud clause, the rank pins \#\mathrm{toric}(m)=m^{\text{toricRank}} and \#\mathrm{fin}(m)=m^{\text{toricRank}+2\,\text{abelianRank}}, and the detection clause producing HasLowerLevelTorsion (primesOf (N*q)) 𝔪 (JZero N) — and adds exactly one further field.

That field, fin_heckeTorsion_detects_lowerLevel_sameIdeal, asserts: assuming the Hecke inputs and the commutation of the Hecke operators at both levels Nq and N, for every maximal ideal \mathfrak m of the polynomial Hecke algebra \mathbb Z[X_\ell:\ell\text{ prime}] with q\in\mathfrak m and X_q\notin\mathfrak m, if some x\in\mathrm{fin}(q) is \mathfrak m-torsion in JZero (N*q) (for the Hecke action heckeModuleBar (N*q)) and x\notin\mathrm{toric}(q), then the \mathfrak m-torsion submodule of JZero N (for heckeModuleBar N) is non-zero. Compared with the inherited clause this is stronger in its conclusion — non-vanishing of \mathfrak m-torsion for the same ideal \mathfrak m, rather than existence of an element annihilated by the integers in \mathfrak m and by the good X_\ell-b lying in \mathfrak m — at the price of the extra hypothesis X_q\notin\mathfrak m.

The predicate HasJZeroNeronAtPDataSameIdeal N q hqN states that such a structure is inhabited for every valuation subring A of \overline{\mathbb Q} over q.

Relation to Mathlib

Mathlib has no Jacobians or Néron models of modular curves; the special-fibre geometry at q is axiomatised here by structure fields, and the Hecke algebra is realised as the polynomial ring \mathbb Z[X_\ell] over the primes. Mathlib supplies the ambient notions used (valuation subrings with their decomposition and inertia subgroups, torsion submodules, Hopf algebras).

Where it is used

This is the form of Mazur's principle datum used for level lowering at the prime q exactly dividing the level: from a non-toric \mathfrak m-torsion point in the finite part of J_0(Nq)[q], with X_q\notin\mathfrak m, one concludes that the same maximal ideal \mathfrak m supports torsion in J_0(N), i.e. that the residual representation attached to \mathfrak m already arises at level N. In the Fermat argument this removes the primes of multiplicative reduction from the level of the representation attached to the Frey curve.

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 \ell representations of Gal(Q̄/Q), in: Motives, Proceedings of Symposia in Pure Mathematics 55, 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_ModularCurve_JZeroNeronAtPDataSameIdeal.lean

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_JZeroNeronAtPData

set_option autoImplicit false

noncomputable section

namespace ModularCurve

structure JZeroNeronAtPDataSameIdeal (N q : ℕ) [NeZero N] [Fact q.Prime] (hqN : ¬ q ∣ N)
    (A : ValuationSubring (AlgebraicClosure ℚ)) (hA : A.LiesOverPrime q)
    extends JZeroNeronAtPData N q hqN A hA where

  fin_heckeTorsion_detects_lowerLevel_sameIdeal :
    HeckeInputsAll (N * q) → HeckeOperatorsCommuteBar (N * q) →
    HeckeInputsAll N → HeckeOperatorsCommuteBar N →
      ∀ 𝔪 : Ideal HeckeAlg, 𝔪.IsMaximal → ((q : ℕ) : HeckeAlg) ∈ 𝔪 → heckeGen ⟨q, Fact.out⟩ ∉ 𝔪 →
        ∀ x ∈ fin q, (letI := heckeModuleBar (N * q); x ∈ heckeTorsion (JZero (N * q)) 𝔪) →
          x ∉ toric q →
            (letI := heckeModuleBar N; heckeTorsion (JZero N) 𝔪 ≠ ⊥)

def HasJZeroNeronAtPDataSameIdeal (N q : ℕ) [NeZero N] [Fact q.Prime] (hqN : ¬ q ∣ N) : Prop :=
  ∀ (A : ValuationSubring (AlgebraicClosure ℚ)) (hA : A.LiesOverPrime q), Nonempty (JZeroNeronAtPDataSameIdeal N q hqN A hA)

end ModularCurve

end

Statements phrased using this module (0)

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