Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_FLTPrelim_Ramification.lean

definition module

Unramifiedness at a prime of torsion Galois representations

Three auxiliary notions and one instantiation. First, for a valuation subring A of a field L and a natural number q, ValuationSubring.LiesOverPrime A q says simply that the image of q in L lies in A.nonunits, i.e. q belongs to the maximal ideal of A; no primality of q is required by the definition. Second, for an extension L/K, ValuationSubring.inertiaSubgroupIn K A is the image of Mathlib's inertia subgroup A.inertiaSubgroup K (a subgroup of the decomposition subgroup, i.e. of the stabiliser of A in L \simeq_{\mathrm{alg}[K]} L) under the inclusion (A.decompositionSubgroup K).subtype, so that inertia is presented as a subgroup of the full automorphism group L \simeq_{\mathrm{alg}[K]} L rather than of the decomposition subgroup.

Third, given a tower R \to S \to K with S, K fields and an affine Weierstrass curve W' over R, WeierstrassCurve.Affine.Point.GaloisRepUnramifiedAt S K W' n q asserts: for every valuation subring A of K with q \in A.\mathrm{nonunits}, every \sigma in the inertia subgroup of A over S (viewed in K \simeq_{\mathrm{alg}[S]} K), and every x in the n-torsion submodule Submodule.torsionBy ℤ (W'⁄K).Point n of the point group of the base change of W' to K, one has \sigma \bullet x = x. The action \sigma \bullet x of automorphisms on points is the one supplied by the project's Galois-representation module. Thus the predicate is the triviality of inertia on n-torsion, stated place by place rather than through a representation object.

Finally, FreyPackage.GaloisRepUnramifiedAt P q is this predicate for R = S = \mathbb{Q}, K = \overline{\mathbb{Q}}, the curve P.freyCurve and n = P.p: the mod-p representation on \overline{\mathbb{Q}}-points of the Frey curve killed by p is unramified at q.

Relation to Mathlib

ValuationSubring.LiesOverPrime and ValuationSubring.inertiaSubgroupIn are thin wrappers around Mathlib's valuation-subring API (nonunits, inertiaSubgroup, decompositionSubgroup), the latter only transporting Mathlib's inertia subgroup along the inclusion of the decomposition subgroup. The unramifiedness predicates for torsion points of a Weierstrass curve are the project's own; Mathlib has no such notion.

Where it is used

These predicates express the local conditions on the mod-p representation attached to a Frey package at primes q not dividing the relevant level, which are what the Serre-type level-lowering and irreducibility arguments consume. The Frey-package instance is the form in which the unramifiedness of E[p] outside the primes of bad reduction and p enters the main line of the argument.

References

  1. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154
  2. J. H. Silverman, The Arithmetic of Elliptic Curves, Graduate Texts in Mathematics 106, Springer, 1986
  3. J.-P. Serre, Propriétés galoisiennes des points d'ordre fini des courbes elliptiques, Inventiones Mathematicae 15 (1972), 259–331

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

Imports

Imported by

Declarations

Source

import Mathlib.RingTheory.Valuation.RamificationGroup ↗
import Mathlib.RingTheory.Valuation.ValuationSubring ↗
import Definitions.Def_FLTPrelim_FreyPackage
import Definitions.Def_FLTPrelim_GaloisRep

set_option autoImplicit false

noncomputable section

universe u

namespace ValuationSubring

variable {L : Type u} [Field L]

def LiesOverPrime (A : ValuationSubring L) (q : ℕ) : Prop :=
  (q : L) ∈ A.nonunits

variable (K : Type*) [Field K] [Algebra K L]

def inertiaSubgroupIn (A : ValuationSubring L) : Subgroup (L ≃ₐ[K] L) :=
  (A.inertiaSubgroup K).map (A.decompositionSubgroup K).subtype

end ValuationSubring

namespace WeierstrassCurve.Affine.Point

open WeierstrassCurve

variable {R : Type*} {S : Type*} {K : Type*} [CommRing R] [Field S] [Field K]
  [DecidableEq K] [Algebra R S] [Algebra R K] [Algebra S K] [IsScalarTower R S K]

variable (S K) in

def GaloisRepUnramifiedAt (W' : Affine R) (n : ℕ) (q : ℕ) : Prop :=
  ∀ A : ValuationSubring K, A.LiesOverPrime q →
    ∀ σ ∈ A.inertiaSubgroupIn S,
    ∀ x : Submodule.torsionBy ℤ (W'⁄K).Point n, σ • x = x

end WeierstrassCurve.Affine.Point

namespace FreyPackage

open WeierstrassCurve.Affine.Point

def GaloisRepUnramifiedAt (P : FreyPackage) (q : ℕ) : Prop :=
  WeierstrassCurve.Affine.Point.GaloisRepUnramifiedAt (K := AlgebraicClosure ℚ) ℚ
    P.freyCurve P.p q

end FreyPackage

end

Statements phrased using this module (1,674)

… and 1,524 more statements (search for the module name to find them).