Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_LanglandsTunnell_IsGaloisAttachmentOf.lean

definition module

Attachment of an octahedral datum to a mod 3 representation

This module defines a single predicate, IsGaloisAttachmentOf, relating a residual representation to the Hecke data carried by an octahedral Galois datum. Its arguments are a group homomorphism \rho from the absolute Galois group of \mathbb{Q}, realised as the group of \mathbb{Q}-algebra automorphisms of AlgebraicClosure ℚ, to \mathrm{GL}_2(\mathbb{Z}/3); a datum D of the project's type OctahedralGaloisDatum ℚ (ℤ√(-2)), i.e. a finite group G together with a surjection G \twoheadrightarrow S_4 (the permutations of Fin 4) and a Hecke eigensystem D.attached over \mathbb{Z}[\sqrt{-2}] for the field \mathbb{Q} (a record consisting of a nonzero level ideal and two functions a, b on the height-one spectrum of \mathcal{O}_{\mathbb{Q}}); and a finite set S of natural numbers, the excluded primes.

The predicate asserts: for every prime p with p \notin S, every valuation subring A of \overline{\mathbb{Q}} lying over p (in the sense that p is a non-unit of A), and every \sigma in the Galois group that is a Frobenius at p for A — that is, \sigma lies in the decomposition subgroup of A over \mathbb{Q} and acts on the residue field of A by x \mapsto x^{p} — one has \mathrm{red}\big(a_{p}\big) \;=\; \mathrm{tr}\,\rho(\sigma) \in \mathbb{Z}/3, where a_{p} = D.attached.a (ratPrime p) is the a-value of the attached eigensystem at the height-one prime of \mathcal{O}_{\mathbb{Q}} corresponding to p, \mathrm{red} : \mathbb{Z}[\sqrt{-2}] \to \mathbb{Z}/3 is the ring homomorphism sending \sqrt{-2} to -1 (legitimate since (-1)^2 = -2 in \mathbb{Z}/3), and the trace is that of the underlying 2 \times 2 matrix of \rho(\sigma).

Note that only the traces of Frobenius elements, and only the a-values, are constrained: nothing is required of the b-values (determinants), of the level, or of the octahedral group-theoretic part of D, and no compatibility at primes in S is imposed. Thus the predicate is a mod 3 Frobenius-trace matching condition, not an assertion that \rho is realised by D up to isomorphism.

Relation to Mathlib

Mathlib has no notion of Hecke eigensystem or of octahedral Galois datum; these are the project's own records. The predicates ValuationSubring.LiesOverPrime and ValuationSubring.IsFrobeniusAt are likewise defined in the project, on top of Mathlib's decomposition subgroup and residue field of a valuation subring; red is obtained from Mathlib's Zsqrtd.lift.

Where it is used

The predicate is the interface between the mod 3 representation coming from a Frey curve and the automorphic side in the Langlands–Tunnell step: an octahedral datum whose attached Hecke eigensystem matches the Frobenius traces of \rho modulo 3 outside a finite set of primes is what allows a cuspidal eigensystem with the same Frobenius data to be produced and then realised by a weight one form, and hence by a weight two form congruent to it modulo 3.

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. J. Tunnell, Artin's conjecture for representations of octahedral type, Bulletin of the American Mathematical Society (N.S.) 5 (1981), 173–175
  3. R. P. Langlands, Base Change for GL(2), Annals of Mathematics Studies 96, Princeton University Press, 1980

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

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_LanglandsTunnell_OctahedralDatum
import Definitions.Def_LanglandsTunnell_ExplicitLift
import Definitions.Def_LanglandsTunnell_RealizationDictionary
import Definitions.Def_EllipticCurve_FrobeniusTrace

set_option autoImplicit false

open AutomorphicForm FLT.TunnellOctahedralGlobalCarrier FLT.ExplicitLift
open scoped MatrixGroups

namespace FLT.TunnellOctahedralGlobalCarrier

local notation "Γℚ" => (AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ)

def IsGaloisAttachmentOf (ρ : Γℚ →* GL (Fin 2) (ZMod 3))
    (D : OctahedralGaloisDatum ℚ (ℤ√(-2))) (S : Finset ℕ) : Prop :=
  ∀ p : Nat.Primes, (p : ℕ) ∉ S →
    ∀ A : ValuationSubring (AlgebraicClosure ℚ), A.LiesOverPrime (p : ℕ) →
      ∀ σ : Γℚ, A.IsFrobeniusAt σ (p : ℕ) →
        red (D.attached.a (ratPrime p))
          = ((ρ σ : GL (Fin 2) (ZMod 3)) : Matrix (Fin 2) (Fin 2) (ZMod 3)).trace

end FLT.TunnellOctahedralGlobalCarrier

Statements phrased using this module (0)

No statement module imports it directly (it is used through other definition modules or by proofs).