Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_TaylorWiles_Primes.lean

definition module

Taylor–Wiles primes, Frobenius density statement, seed data

The module sets up the vocabulary for the auxiliary primes of the patching argument, over a number field L that is finite Galois over \mathbb{Q}.

For a 2\times 2 matrix M over a commutative ring R, Matrix.HasDistinctRationalEigenvalues M is defined purely in terms of the characteristic polynomial: there exist \alpha,\beta\in R with \alpha\neq\beta, \operatorname{tr}M=\alpha+\beta and \det M=\alpha\beta. Accompanying this are the 2\times2 Cayley–Hamilton identity M^2=(\operatorname{tr}M)M-(\det M)\cdot 1, its consequence M^{k+2}=(\operatorname{tr}M)M^{k+1}-(\det M)M^{k}, and the resulting trace recursion \operatorname{tr}(M^{k+2})=\operatorname{tr}(M)\operatorname{tr}(M^{k+1})-\det(M)\operatorname{tr}(M^{k}).

In the FrobeniusDensity namespace, ratPrimeIdeal ℓ is the ideal (\ell)\subseteq\mathbb{Z}, with helper lemmas that it is nonzero and maximal for \ell prime, that nonzero ideals of \mathcal{O}_L have finite quotient, and that a prime of \mathcal{O}_L lying over (\ell) is nonzero. Then RealizesCyclicAt L σ ℓ asserts that \ell is prime and that for every prime ideal Q of \mathcal{O}_L lying over (\ell) — with the finiteness of the residue ring \mathcal{O}_L/Q supplied as a further hypothesis binder, although the helper lemmas make it derivable — there is k coprime to the order of \sigma such that \sigma^k is conjugate in \mathrm{Gal}(L/\mathbb{Q}) to the arithmetic Frobenius arithFrobAt ℤ (L ≃ₐ[ℚ] L) Q. Statement is the Frobenius-density assertion: for every \sigma and every finite set S of naturals there is \ell\notin S with RealizesCyclicAt L σ ℓ.

A ResidualRep L 𝕜 is a monoid homomorphism \mathrm{Gal}(L/\mathbb{Q})\to M_2(\mathbb{k}) (values are automatically invertible, the source being a group). For such \rho and naturals p,n, IsTaylorWilesPrime ρ p n q says: q is prime, q\equiv 1 \pmod{p^n}, and for every prime Q over (q) (again with a finiteness binder) the matrix \rho(\mathrm{Frob}_Q) has distinct eigenvalues in \mathbb{k} in the above sense. Finally Seed ρ p n S is a structure bundling an element \sigma, a proof that \rho(\sigma) has distinct eigenvalues, and a proof that every \ell\notin S realising a coprime power of \sigma as Frobenius satisfies \ell\equiv 1\pmod{p^n}; SeedExists is the nonemptiness of that structure.

Relation to Mathlib

The Frobenius element is Mathlib's arithFrobAt, and the ramification/finite-quotient facts are Mathlib's; the eigenvalue predicate, the Taylor–Wiles prime predicate, the Frobenius-density statement and the seed structure are the project's own. The elementary 2\times2 Cayley–Hamilton and trace-recursion lemmas are placed in the Matrix namespace.

Where it is used

These predicates are the interface through which the patching argument obtains its auxiliary primes: one needs, for each depth n, primes q\equiv 1\pmod{p^n} at which the residual representation has Frobenius with distinct eigenvalues, and the seed datum reduces their existence to a Frobenius-density statement, both Taylor–Wiles conditions being stable under passing to coprime powers of the seed element.

References

  1. R. Taylor and A. Wiles, Ring-theoretic properties of certain Hecke algebras, Annals of Mathematics 141 (1995), 553–572
  2. 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_TaylorWiles_Primes.lean

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib.RingTheory.Frobenius ↗
import Mathlib.NumberTheory.RamificationInertia.Galois ↗
import Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients ↗
import Mathlib.LinearAlgebra.Matrix.Trace ↗
import Mathlib.LinearAlgebra.Matrix.Determinant.Basic ↗

set_option autoImplicit false

namespace Matrix

variable {R : Type*} [CommRing R]

theorem sq_eq_trace_smul_sub_det_smul_one (M : Matrix (Fin 2) (Fin 2) R) :
    M ^ 2 = M.trace • M - M.det • (1 : Matrix (Fin 2) (Fin 2) R) := by
  ext i j
  simp only [pow_two, Matrix.mul_apply, Fin.sum_univ_two, Matrix.trace_fin_two,
    Matrix.det_fin_two, Matrix.sub_apply, Matrix.smul_apply, Matrix.one_apply, smul_eq_mul]
  fin_cases i <;> fin_cases j <;> simp <;> ring

theorem pow_add_two_eq_trace_smul_sub_det_smul (M : Matrix (Fin 2) (Fin 2) R) (k : ℕ) :
    M ^ (k + 2) = M.trace • M ^ (k + 1) - M.det • M ^ k := by
  have h : M ^ (k + 2) = M ^ k * M ^ 2 := by rw [← pow_add]
  rw [h, sq_eq_trace_smul_sub_det_smul_one, Matrix.mul_sub, mul_smul_comm, mul_smul_comm,
    mul_one, ← pow_succ]

theorem trace_pow_add_two (M : Matrix (Fin 2) (Fin 2) R) (k : ℕ) :
    (M ^ (k + 2)).trace = M.trace * (M ^ (k + 1)).trace - M.det * (M ^ k).trace := by
  rw [pow_add_two_eq_trace_smul_sub_det_smul, Matrix.trace_sub, Matrix.trace_smul,
    Matrix.trace_smul, smul_eq_mul, smul_eq_mul]

def HasDistinctRationalEigenvalues (M : Matrix (Fin 2) (Fin 2) R) : Prop :=
  ∃ α β : R, α ≠ β ∧ M.trace = α + β ∧ M.det = α * β

end Matrix

namespace FrobeniusDensity

open NumberField Ideal

variable (L : Type*) [Field L] [NumberField L] [IsGalois ℚ L]

abbrev ratPrimeIdeal (ℓ : ℕ) : Ideal ℤ := Ideal.span {(ℓ : ℤ)}

theorem ratPrimeIdeal_ne_bot {ℓ : ℕ} (hℓ : ℓ.Prime) : ratPrimeIdeal ℓ ≠ ⊥ := by
  rw [Ne, Ideal.span_singleton_eq_bot]
  exact_mod_cast hℓ.ne_zero

instance isMaximal_ratPrimeIdeal (ℓ : ℕ) [Fact ℓ.Prime] : (ratPrimeIdeal ℓ).IsMaximal :=
  PrincipalIdealRing.isMaximal_of_irreducible
    (Nat.prime_iff_prime_int.mp Fact.out).irreducible

variable {L}

omit [IsGalois ℚ L] in

theorem finite_quotient_of_ne_bot {Q : Ideal (𝓞 L)} (hQ : Q ≠ ⊥) : Finite (𝓞 L ⧸ Q) :=
  Ring.HasFiniteQuotients.finiteQuotient hQ

omit [IsGalois ℚ L] in

theorem ne_bot_of_liesOver_ratPrimeIdeal {ℓ : ℕ} (hℓ : ℓ.Prime) {Q : Ideal (𝓞 L)}
    [Q.IsPrime] [Q.LiesOver (ratPrimeIdeal ℓ)] : Q ≠ ⊥ :=
  Ideal.ne_bot_of_liesOver_of_ne_bot (ratPrimeIdeal_ne_bot hℓ) Q

variable (L)

def RealizesCyclicAt (σ : L ≃ₐ[ℚ] L) (ℓ : ℕ) : Prop :=
  ∃ _ : ℓ.Prime, ∀ (Q : Ideal (𝓞 L)) (_ : Q.IsPrime) (_ : Q.LiesOver (ratPrimeIdeal ℓ))
    (_ : Finite (𝓞 L ⧸ Q)),
    ∃ k : ℕ, k.Coprime (orderOf σ) ∧ IsConj (σ ^ k) (arithFrobAt ℤ (L ≃ₐ[ℚ] L) Q)

def Statement : Prop :=
  ∀ (σ : L ≃ₐ[ℚ] L) (S : Finset ℕ), ∃ ℓ : ℕ, ℓ ∉ S ∧ RealizesCyclicAt L σ ℓ

end FrobeniusDensity

namespace TaylorWiles

open NumberField Ideal FrobeniusDensity

variable {L : Type*} [Field L] [NumberField L] [IsGalois ℚ L]
variable {𝕜 : Type*} [Field 𝕜]

variable (L) in

abbrev ResidualRep (𝕜 : Type*) [Field 𝕜] := (L ≃ₐ[ℚ] L) →* Matrix (Fin 2) (Fin 2) 𝕜

variable (ρ : ResidualRep L 𝕜) (p n : ℕ)

def IsTaylorWilesPrime (q : ℕ) : Prop :=
  q.Prime ∧ q ≡ 1 [MOD p ^ n] ∧
    ∀ (Q : Ideal (𝓞 L)) (_ : Q.IsPrime) (_ : Q.LiesOver (ratPrimeIdeal q))
      (_ : Finite (𝓞 L ⧸ Q)),
      (ρ (arithFrobAt ℤ (L ≃ₐ[ℚ] L) Q)).HasDistinctRationalEigenvalues

structure Seed (S : Finset ℕ) where

  σ : L ≃ₐ[ℚ] L

  regular : (ρ σ).HasDistinctRationalEigenvalues

  congruent : ∀ ℓ : ℕ, ℓ ∉ S → RealizesCyclicAt L σ ℓ → ℓ ≡ 1 [MOD p ^ n]

def SeedExists (S : Finset ℕ) : Prop := Nonempty (Seed ρ p n S)

end TaylorWiles

Statements phrased using this module (25)