Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ExtCitation_AdmissibleExtension_v2.lean

definition module

Continuous admissible extensions of by

Throughout, p is a prime, V is a \mathbb{Z}/p-vector space carrying a distributive multiplicative action of G_{\mathbb{Q}} = \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}) (realised as AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) commuting with scalars, and C \subseteq V is a \mathbb{Z}/p-submodule. The structure IsAdmissibleExtensionCts p V C extends the project's IsAdmissibleExtension p V C by a single extra field open_kernel, asserting that the pointwise stabiliser \{\sigma \in G_{\mathbb{Q}} \mid \sigma \cdot v = v \text{ for all } v \in V\} is open for the Krull topology; equivalently, the action factors through a finite Galois quotient. The inherited fields say: C is G_{\mathbb{Q}}-stable, G_{\mathbb{Q}} acts trivially on C (so the stability field is subsumed), for every \sigma and every x \in V one has \sigma\cdot x - \bar\chi(\sigma)\,x \in C, where \bar\chi(\sigma) \in \mathbb{Z}/p is the value of the mod p cyclotomic character (cycloExp, built from Mathlib's modularCyclotomicCharacter) — i.e. V/C \cong \mu_p, stated as a congruence rather than an isomorphism; \#C = p and \#V = p^2; for every prime \ell \neq p and every valuation subring A of \overline{\mathbb{Q}} with \ell a non-unit of A, every element of the image of the inertia subgroup of A over \mathbb{Q} acts trivially on all of V (unramified outside p); and for every such A lying over p there is a submodule C' stable under the decomposition subgroup of A with C \oplus C' = V (locally split at p).

ExtVanishingCts p asserts that for every such V and C satisfying IsAdmissibleExtensionCts, the conclusion SplitsGlobally C holds: there is a G_{\mathbb{Q}}-stable complement C' to C in V. ExtVanishingCtsAll quantifies this over all primes p \ge 3. Finally extVanishingCts_of_extVanishing records the immediate implication ExtVanishing p → ExtVanishingCts p, obtained by forgetting the openness field; the continuous version is thus the weaker hypothesis, and every consequence of the non-continuous one remains available.

Relation to Mathlib

Mathlib has no notion of admissible extension of \mu_p by \mathbb{Z}/p, nor of the corresponding \mathrm{Ext}-vanishing statement; these are the project's own. The topology on \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}) used in open_kernel is Mathlib's Krull topology instance, and the mod p cyclotomic character underlying cycloExp is Mathlib's modularCyclotomicCharacter.

Where it is used

These predicates package, in a form citable inside the formalisation, the vanishing of \mathrm{Ext}^1_{\mathrm{Spec}\,\mathbb{Z}}(\mu_p, \mathbb{Z}/p): a two-dimensional mod p Galois module with a trivial sub, cyclotomic quotient, unramified outside p and split at p, must split globally. It is used in the step ruling out reducibility of the mod p representation attached to the p-torsion of a Frey curve.

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. B. Mazur, Rational isogenies of prime degree, Inventiones Mathematicae 44 (1978), 129–162
  3. J.-M. Fontaine, Il n'y a pas de variété abélienne sur Z, Inventiones Mathematicae 81 (1985), 515–538

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_ExtCitation_AdmissibleExtension

set_option autoImplicit false

namespace ExtCitation

open ValuationSubring

variable (p : ℕ) [Fact p.Prime]
variable (V : Type) [AddCommGroup V] [Module (ZMod p) V]
  [DistribMulAction (AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) V]
  [SMulCommClass (AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) (ZMod p) V]

structure IsAdmissibleExtensionCts (C : Submodule (ZMod p) V) : Prop
    extends IsAdmissibleExtension p V C where

  open_kernel : IsOpen {σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ | ∀ v : V, σ • v = v}

def ExtVanishingCts : Prop :=
  ∀ (V : Type) [AddCommGroup V] [Module (ZMod p) V]
    [DistribMulAction (AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) V]
    [SMulCommClass (AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) (ZMod p) V]
    (C : Submodule (ZMod p) V),
    IsAdmissibleExtensionCts p V C → SplitsGlobally C

def ExtVanishingCtsAll : Prop :=
  ∀ p : ℕ, (hp : p.Prime) → 3 ≤ p → @ExtVanishingCts p ⟨hp⟩

variable {p V} in

theorem extVanishingCts_of_extVanishing (h : ExtVanishing p) : ExtVanishingCts p :=
  fun V _ _ _ _ C hadm => h V C hadm.toIsAdmissibleExtension

end ExtCitation

Statements phrased using this module (5)