Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_LanglandsTunnell_DetDictionaryRow.lean

definition module

Determinant dictionary for a Galois group isomorphic to

Fix a number field L that is Galois over \mathbb{Q}, and fix a group isomorphism e \colon \mathrm{Gal}(L/\mathbb{Q}) \xrightarrow{\ \sim\ } \mathrm{GL}_2(\mathbb{Z}/3) (a MulEquiv; no continuity or further structure is demanded, the field being of finite degree). The predicate DetDictionaryRow e asserts that e reads the mod-3 cyclotomic character off determinants of Frobenius elements: for every natural number \ell that is prime and different from 3, and for every ideal Q of the ring of integers \mathcal{O}_L which is prime, lies over the ideal \ell\mathbb{Z} of \mathbb{Z} (the project's abbreviation ratPrimeIdeal ℓ for \mathrm{span}\{\ell\}), and has finite residue ring \mathcal{O}_L/Q, if the inertia subgroup of Q inside \mathrm{Gal}(L/\mathbb{Q}) is trivial, then the determinant of the matrix underlying e(\mathrm{Frob}_Q) equals the image of \ell in \mathbb{Z}/3. Here \mathrm{Frob}_Q is Mathlib's arithmetic Frobenius arithFrobAt at Q for the extension \mathbb{Z} \subseteq \mathcal{O}_L, which is well defined precisely under the unramifiedness hypothesis imposed.

Several points of shape are worth recording. The primality of \ell, the primality of Q, the lying-over, the finiteness of the residue ring and the triviality of inertia are all explicit (anonymous) hypotheses rather than inferred instances. The condition is a property of the pair (L, e), i.e. of a chosen presentation of the Galois group, not of L alone: replacing e by a composite with an automorphism of \mathrm{GL}_2(\mathbb{Z}/3) changes the quadratic character cut out by \det \circ\, e. Nothing is asserted at \ell = 3, and no instance of the predicate is produced here.

Relation to Mathlib

Built on Mathlib's arithmetic Frobenius arithFrobAt and inertia subgroup Ideal.inertia for Galois extensions; the dictionary condition itself, and the abbreviation ratPrimeIdeal for the ideal generated by a rational prime, are the project's own.

Where it is used

The condition is the tower-side form of the requirement that a mod-3 two-dimensional representation of \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}) have determinant the mod-3 cyclotomic character, which is a hypothesis in the Langlands–Tunnell step attaching a modular form to the mod-3 representation on the 3-torsion of the 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, §3
  2. R. P. Langlands, Base Change for GL(2), Annals of Mathematics Studies 96, Princeton University Press, 1980
  3. J. Tunnell, Artin's conjecture for representations of octahedral type, Bulletin of the American Mathematical Society (N.S.) 5 (1981), 173–175

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Definitions.Def_TaylorWiles_Primes

set_option autoImplicit false

namespace LanglandsTunnell

open NumberField Ideal FrobeniusDensity

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

def DetDictionaryRow (e : (L ≃ₐ[ℚ] L) ≃* Matrix.GeneralLinearGroup (Fin 2) (ZMod 3)) :
    Prop :=
  ∀ (ℓ : ℕ), ℓ.Prime → ℓ ≠ 3 →
    ∀ (Q : Ideal (𝓞 L)) (_ : Q.IsPrime) (_ : Q.LiesOver (ratPrimeIdeal ℓ))
      (_ : Finite (𝓞 L ⧸ Q)),
      Q.inertia (L ≃ₐ[ℚ] L) = ⊥ →
      ((e (arithFrobAt ℤ (L ≃ₐ[ℚ] L) Q) : Matrix.GeneralLinearGroup (Fin 2) (ZMod 3)) :
        Matrix (Fin 2) (Fin 2) (ZMod 3)).det = (ℓ : ZMod 3)

end LanglandsTunnell

Statements phrased using this module (8)