Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_GaloisRep_LocalConditions.lean

definition module

Local conditions on adic Galois representations: determinant, ordinarity, inertia

Four predicates on a Galois representation ρ : GaloisRepAdic A (the project's rank-two representation datum, with carrier ρ.V and action ρ.ρ of \mathrm{Aut}_{\mathbb Q}(\overline{\mathbb Q})) over a commutative local ring A; all are finite-level and topology-free. (1) DetIsCyclotomic ρ p asserts that p lies in the maximal ideal of A and that, for every n, every \sigma and every natural number a such that \sigma\mu=\mu^{a} for all p^{n}-th roots of unity \mu in \overline{\mathbb Q}, one has \det\rho(\sigma)-a \in (p^{n})A. So the determinant is pinned down only by congruences modulo the principal ideals (p^{n}), not by an equality of characters; over a field of characteristic p this says \det\bar\rho is the mod-p cyclotomic character. (2) IsOrdinaryAt ρ p: for every valuation subring P of \overline{\mathbb Q} with P.LiesOverPrime p there is a submodule L of ρ.V which is spanned by the first vector of some A-basis of ρ.V indexed by Fin 2 (hence a free rank-one direct summand), is stable under the decomposition subgroup of P, and satisfies \rho(\sigma)v-v\in L for all v and all \sigma in the inertia subgroup of P (inertia acts trivially on ρ.V/L). (3) IsUnipotentOnInertiaAt ρ q: for every P above q and every inertia element \sigma, \operatorname{charpoly}(\rho(\sigma))=(X-1)^{2} — an equality of characteristic polynomials, which over a non-reduced A is strictly stronger than (\rho(\sigma)-1)^{2}=0. (4) GaloisRep.ordinaryCondition 𝒪 p S and GaloisRep.minimalOrdinaryCondition 𝒪 p S package these as predicates on representations over varying coefficient rings (binder ⦃A⦄, local 𝒪-algebras): the former is DetIsCyclotomic p ∧ IsOrdinaryAt p ∧ unramified (IsUnramifiedAt) at every prime q\notin S, imposing nothing at the primes of S other than p; the latter adds IsUnipotentOnInertiaAt q for every prime q\in S with q\neq p. The names LiesOverPrime, inertiaSubgroupIn and IsUnramifiedAt are not defined here; they come from the imported definitions or from Mathlib. No representability, minimality or uniqueness statement is made in this module, and the 𝒪-algebra structure enters only through the signature.

Relation to Mathlib

The local data are phrased with Mathlib's valuation subrings of \overline{\mathbb Q} and their decomposition subgroups; Mathlib has no notion of a deformation condition on a Galois representation, so ordinaryCondition and minimalOrdinaryCondition, like the underlying GaloisRepAdic, are the project's own.

Where it is used

These predicates are the deformation conditions fed to the project's deformation-ring data: minimalOrdinaryCondition 𝒪 p S stands for the minimal ordinary problem used in the patching and numerical-criterion steps, while ordinaryCondition 𝒪 p S with S containing p and the bad primes is the weaker, type-\Sigma problem through which the representation attached to a semistable elliptic curve is taken to factor.

References

  1. B. Mazur, Deforming Galois representations, in: Galois Groups over \mathbb Q, MSRI Publications 16, Springer, 1989, 385–437
  2. A. Wiles, Modular elliptic curves and Fermat's Last Theorem, Annals of Mathematics 141 (1995), 443–551
  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_GaloisRep_LocalConditions.lean

Imports

Imported by

Declarations

Source

import Definitions.Def_GaloisRep_Adic

namespace GaloisRepAdic

variable {A : Type} [CommRing A] [IsLocalRing A]

def DetIsCyclotomic (ρ : GaloisRepAdic A) (p : ℕ) : Prop :=
  (p : A) ∈ IsLocalRing.maximalIdeal A ∧
    ∀ (n : ℕ) (σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) (a : ℕ),
      (∀ μ : AlgebraicClosure ℚ, μ ^ p ^ n = 1 → σ μ = μ ^ a) →
        LinearMap.det (ρ.ρ σ) - (a : A) ∈ Ideal.span {((p ^ n : ℕ) : A)}

def IsOrdinaryAt (ρ : GaloisRepAdic A) (p : ℕ) : Prop :=
  ∀ P : ValuationSubring (AlgebraicClosure ℚ), P.LiesOverPrime p →
    ∃ L : Submodule A ρ.V,
      (∃ b : Module.Basis (Fin 2) A ρ.V, L = A ∙ b 0) ∧
      (∀ σ ∈ P.decompositionSubgroup ℚ, ∀ v ∈ L, ρ.ρ σ v ∈ L) ∧
      (∀ σ ∈ P.inertiaSubgroupIn ℚ, ∀ v : ρ.V, ρ.ρ σ v - v ∈ L)

def IsUnipotentOnInertiaAt (ρ : GaloisRepAdic A) (q : ℕ) : Prop :=
  ∀ P : ValuationSubring (AlgebraicClosure ℚ), P.LiesOverPrime q →
    ∀ σ ∈ P.inertiaSubgroupIn ℚ, LinearMap.charpoly (ρ.ρ σ) = (Polynomial.X - 1) ^ 2

end GaloisRepAdic

namespace GaloisRep

def ordinaryCondition (𝒪 : Type) [CommRing 𝒪] (p : ℕ) (S : Finset ℕ) :
    ∀ ⦃A : Type⦄ [CommRing A] [IsLocalRing A] [Algebra 𝒪 A], GaloisRepAdic A → Prop :=
  fun _A _ _ _ ρ => ρ.DetIsCyclotomic p ∧ ρ.IsOrdinaryAt p ∧
    ∀ q : ℕ, q.Prime → q ∉ S → ρ.IsUnramifiedAt q

def minimalOrdinaryCondition (𝒪 : Type) [CommRing 𝒪] (p : ℕ) (S : Finset ℕ) :
    ∀ ⦃A : Type⦄ [CommRing A] [IsLocalRing A] [Algebra 𝒪 A], GaloisRepAdic A → Prop :=
  fun _A _ _ _ ρ => ordinaryCondition 𝒪 p S ρ ∧
    ∀ q ∈ S, q.Prime → q ≠ p → ρ.IsUnipotentOnInertiaAt q

end GaloisRep

Statements phrased using this module (213)

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