Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_WeierstrassCurve_PeuRamifiee.lean

definition module

The peu ramifiée divisibility condition on Weierstrass discriminants

Two declarations are given. First, WeierstrassCurve.IsPeuRamifieeAt W p ℓ, for a Weierstrass curve W over \mathbb{Q} and natural numbers p,\ell, is defined to be the single divisibility statement (p : \mathbb{Z}) \mid \mathrm{padicValRat}\,\ell\,W.\Delta: the integer p divides the \ell-adic valuation of the discriminant \Delta of the given Weierstrass presentation. Note that this is a condition on the chosen Weierstrass model (through Mathlib's WeierstrassCurve.Δ), not on an isomorphism class of elliptic curves, and that neither p nor \ell is assumed prime, nor is any reduction type at \ell assumed; in particular no Galois representation or Tate parameter appears in the definition. The intended reading is the classical one: for a curve with multiplicative reduction at \ell, divisibility of v_\ell(\Delta) by p is the criterion for the restriction of the mod p representation to the decomposition group at \ell to be peu ramifiée in Serre's sense, and for \ell = p to be finite (come from a finite flat group scheme over \mathbb{Z}_p); but what is formalised here is only the valuation divisibility.

Second, ModularCurve.peuRamifieeGuard W p ℓ is the constant predicate on ideals of the project's Hecke algebra HeckeAlg whose value at every ideal is W.IsPeuRamifieeAt p ℓ; the ideal argument is discarded. It exists so that the divisibility condition can be supplied where the level-lowering machinery expects a predicate on Hecke ideals.

Relation to Mathlib

Both declarations are the project's own; they are built from Mathlib's WeierstrassCurve.Δ (the discriminant of a Weierstrass presentation) and padicValRat (the \ell-adic valuation of a rational number). Mathlib has no notion of a peu ramifiée, or finite-at-\ell, local condition. HeckeAlg comes from the project's own at-p package module.

Where it is used

In the Fermat application the condition is imposed at \ell = p on the Frey curve attached to a hypothetical solution, where v_p(\Delta) is divisible by p, supplying the finiteness (Serre weight 2) input to the level-lowering step; the guard form is what the descent statements about at-p support consume.

References

  1. J.-P. Serre, Sur les représentations modulaires de degré 2 de \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}), Duke Mathematical Journal 54 (1987), 179–230
  2. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154
  3. J. H. Silverman, Advanced Topics in the Arithmetic of Elliptic Curves, Graduate Texts in Mathematics 151, Springer, 1994

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

Imports

Imported by

Declarations

Source

import Mathlib.NumberTheory.Padics.PadicVal.Basic ↗
import Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass ↗
import Definitions.Def_ModularCurve_AtPPackage

open scoped Classical in
section

namespace WeierstrassCurve

def IsPeuRamifieeAt (W : WeierstrassCurve ℚ) (p ℓ : ℕ) : Prop :=
  (p : ℤ) ∣ padicValRat ℓ W.Δ

end WeierstrassCurve

namespace ModularCurve

def peuRamifieeGuard (W : WeierstrassCurve ℚ) (p ℓ : ℕ) : Ideal HeckeAlg → Prop :=
  fun _ => W.IsPeuRamifieeAt p ℓ

end ModularCurve

end

Statements phrased using this module (9)