Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_FLTPrelim_GaloisRep.lean

definition modulenamed in PROOF-PATH.mdnamed in route.md §3adapted from the Imperial College London FLT project: FLT/EllipticCurve/Torsion.lean

Galois action on -torsion; irreducibility predicate

For a Weierstrass curve W' : Affine R and a tower of algebras R \to S \to K with K a field (with decidable equality), the module makes the group K \simeq_{\mathrm{alg}[S]} K of S-algebra automorphisms of K act on the group of points (W'\!⁄K).Point of the base change of W' to K: \sigma \bullet P is defined to be Point.map of \sigma viewed as an S-algebra homomorphism (algEquiv_smul_def), and this is upgraded to a DistribMulAction, so the action is by group automorphisms of the Mordell–Weil-type group (W'\!⁄K).Point. Since the action commutes with integer multiples (algEquiv_smul_zsmul), it preserves Submodule.torsionBy ℤ (W'⁄K).Point n, the subgroup of points killed by n (smul_mem_torsionBy), giving an induced DistribMulAction on that n-torsion subgroup; the n-torsion is also equipped with its canonical \mathbb Z/n-module structure, obtained from AddCommGroup.zmodModule using that n annihilates it.

Two predicates are then defined. IsGaloisStable S N, for N a \mathbb Z/n-submodule of the n-torsion, says that \sigma \bullet x \in N for every S-algebra automorphism \sigma of K and every x \in N. GaloisRepIsIrreducible S W' n is the conjunction of: the n-torsion of (W'\!⁄K).Point is Nontrivial (i.e. contains a nonzero point), and every \mathbb Z/n-submodule N of it satisfying IsGaloisStable S N equals \bot or \top. The formulation is basis-free: no identification of the n-torsion with (\mathbb Z/n)^2, no matrix representation, and no primality assumption on n or algebraic-closedness assumption on K is imposed; the acting group is literally the automorphism group K \simeq_{\mathrm{alg}[S]} K. A final instance supplies classical decidable equality on AlgebraicClosure ℚ, the case of K used in the application.

Relation to Mathlib

The curve, its affine points and Point.map, Submodule.torsionBy and AddCommGroup.zmodModule are Mathlib's; the action of S-algebra automorphisms of K on the points, the induced action and \mathbb Z/n-module structure on the n-torsion, and the predicates IsGaloisStable and GaloisRepIsIrreducible are the project's own.

Where it is used

These definitions carry the irreducibility step for the Frey curve: the statement proved about a Frey package P is GaloisRepIsIrreducible ℚ P.freyCurve P.p, i.e. that E_P[p] over an algebraic closure of \mathbb Q is nonzero and has no Galois-stable \mathbb Z/p-submodule other than 0 and everything, which is the hypothesis feeding the modularity/level-lowering part of the argument.

References

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

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

Imports

  • only Mathlib

Imported by

Declarations

Source

/-
Copyright (c) 2024 Imperial College London FLT project contributors.
Released under Apache 2.0 license.
Adapted from the Imperial College London FLT formalization
(https://github.com/ImperialCollegeLondon/FLT).
-/
import Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point ↗
import Mathlib.Algebra.Module.Torsion.Basic ↗
import Mathlib.Algebra.GroupWithZero.Action.Basic ↗
import Mathlib.Algebra.Module.ZMod ↗
import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure ↗

set_option autoImplicit false

universe r s v

namespace WeierstrassCurve.Affine.Point

open WeierstrassCurve

variable {R : Type r} {S : Type s} {K : Type v} [CommRing R] [CommRing S] [Field K]
  [DecidableEq K] {W' : Affine R} [Algebra R S] [Algebra R K] [Algebra S K]
  [IsScalarTower R S K]

noncomputable instance instSMulAlgEquiv : SMul (K ≃ₐ[S] K) (W'⁄K).Point :=
  ⟨fun σ P => Point.map σ.toAlgHom P⟩

lemma algEquiv_smul_def (σ : K ≃ₐ[S] K) (P : (W'⁄K).Point) :
    σ • P = Point.map σ.toAlgHom P :=
  rfl

noncomputable instance instDistribMulActionAlgEquiv :
    DistribMulAction (K ≃ₐ[S] K) (W'⁄K).Point where
  one_smul P := by cases P <;> rfl
  mul_smul σ τ P := by cases P <;> rfl
  smul_zero _ := rfl
  smul_add σ P Q := (Point.map σ.toAlgHom).map_add P Q

lemma algEquiv_smul_zsmul (σ : K ≃ₐ[S] K) (m : ℤ) (P : (W'⁄K).Point) :
    σ • (m • P) = m • (σ • P) :=
  (Point.map σ.toAlgHom).map_zsmul m P

lemma smul_mem_torsionBy {n : ℕ} (σ : K ≃ₐ[S] K) {P : (W'⁄K).Point}
    (hP : P ∈ Submodule.torsionBy ℤ (W'⁄K).Point n) :
    σ • P ∈ Submodule.torsionBy ℤ (W'⁄K).Point n := by
  rw [Submodule.mem_torsionBy_iff] at hP ⊢
  rw [← algEquiv_smul_zsmul, hP, smul_zero]

noncomputable instance instSMulTorsionBy (n : ℕ) :
    SMul (K ≃ₐ[S] K) (Submodule.torsionBy ℤ (W'⁄K).Point n) :=
  ⟨fun σ P => ⟨σ • (P : (W'⁄K).Point), smul_mem_torsionBy σ P.property⟩⟩

noncomputable instance instDistribMulActionTorsionBy (n : ℕ) :
    DistribMulAction (K ≃ₐ[S] K) (Submodule.torsionBy ℤ (W'⁄K).Point n) where
  one_smul P := Subtype.ext <| one_smul _ (P : (W'⁄K).Point)
  mul_smul σ τ P := Subtype.ext <| mul_smul σ τ (P : (W'⁄K).Point)
  smul_zero σ := Subtype.ext <| smul_zero (A := (W'⁄K).Point) σ
  smul_add σ P Q := Subtype.ext <| smul_add σ (P : (W'⁄K).Point) (Q : (W'⁄K).Point)

noncomputable instance instModuleZModTorsionBy (n : ℕ) :
    Module (ZMod n) (Submodule.torsionBy ℤ (W'⁄K).Point n) :=
  AddCommGroup.zmodModule fun x => by
    rw [← Nat.cast_smul_eq_nsmul ℤ n x]
    exact Submodule.smul_torsionBy _ x

variable (S) in

def IsGaloisStable {n : ℕ}
    (N : Submodule (ZMod n) (Submodule.torsionBy ℤ (W'⁄K).Point n)) : Prop :=
  ∀ (σ : K ≃ₐ[S] K), ∀ x ∈ N, σ • x ∈ N

variable (S) in

def GaloisRepIsIrreducible (W' : Affine R) (n : ℕ) : Prop :=
  Nontrivial (Submodule.torsionBy ℤ (W'⁄K).Point n) ∧
    ∀ N : Submodule (ZMod n) (Submodule.torsionBy ℤ (W'⁄K).Point n),
      IsGaloisStable S N → N = ⊥ ∨ N = ⊤

end WeierstrassCurve.Affine.Point

noncomputable instance instDecEqAlgebraicClosureRat :
    DecidableEq (AlgebraicClosure ℚ) :=
  Classical.decEq _

Statements phrased using this module (174)

… and 24 more statements (search for the module name to find them).