Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_GaloisRep_StrictOrdinary.lean

definition module

Strictly ordinary condition and strict deformation types

Over a commutative local ring A, a GaloisRepAdic A consists of a free A-module V of rank 2 with an A-linear action \rho of \mathrm{Gal}(\overline{\mathbb Q}/\mathbb Q) satisfying the \mathfrak m_A-adic continuity condition. GaloisRepAdic.IsStrictOrdinaryAt ρ p asserts that p\in\mathfrak m_A and that for every valuation subring P of \overline{\mathbb Q} with p a nonunit of P there is an A-submodule L\subseteq V with: L=A\,b_0 for some A-basis (b_0,b_1) of V; L stable under the decomposition subgroup of P over \mathbb Q; \rho(\sigma)v-v\in L for all v\in V and all \sigma in the inertia subgroup (the image in the full Galois group of the inertia subgroup of P inside its decomposition subgroup); and, for each \sigma in the decomposition subgroup, scalars x,z\in A with \rho(\sigma)w=xw on L and \rho(\sigma)v-zv\in L on V, subject to x-az\in(p^n) whenever \sigma raises every p^n-th root of unity \mu to the power a. The first three clauses are exactly IsOrdinaryAt, and IsStrictOrdinaryAt.isOrdinaryAt records this by discarding the fourth; the fourth expresses, as congruences at every finite level rather than as an identity of characters, that the character on L is the cyclotomic character times the character on V/L.

GaloisRep.strictOrdinaryCondition 𝒪 p S is the predicate on GaloisRepAdic A for local \mathcal O-algebras A given by: the determinant congruence condition DetIsCyclotomic at p, strict ordinarity at p, and unramifiedness (trivial action of every inertia subgroup) at every prime q\notin S. minimalStrictOrdinaryCondition adds, for every prime q\in S with q\neq p, that every inertia element at q has characteristic polynomial (X-1)^2. The two further lemmas deduce ordinaryCondition and minimalOrdinaryCondition from their strict counterparts.

Relation to Mathlib

Mathlib has no notion of deformation condition for Galois representations; these predicates are the project's own, built on Mathlib's ValuationSubring.decompositionSubgroup and inertiaSubgroup (via the project's inertiaSubgroupIn, the image of the inertia subgroup in the full Galois group).

Where it is used

These are the local conditions cutting out the strict, and minimal strict, deformation problems used on the ordinary side of the modularity lifting argument; the implications recorded here let statements proved for the ordinary conditions be applied to representations known only to be strictly ordinary.

References

  1. A. Wiles, Modular elliptic curves and Fermat's Last Theorem, Annals of Mathematics 141 (1995), 443–551
  2. R. Taylor and A. Wiles, Ring-theoretic properties of certain Hecke algebras, Annals of Mathematics 141 (1995), 553–572
  3. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154, §3

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

Imports

Imported by

Declarations

Source

import Definitions.Def_GaloisRep_LocalConditions

namespace GaloisRepAdic

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

def IsStrictOrdinaryAt (ρ : GaloisRepAdic A) (p : ℕ) : Prop :=
  (p : A) ∈ IsLocalRing.maximalIdeal A ∧
  ∀ 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) ∧
      (∀ σ ∈ P.decompositionSubgroup ℚ, ∃ x z : A,
        (∀ w ∈ L, ρ.ρ σ w = x • w) ∧ (∀ v : ρ.V, ρ.ρ σ v - z • v ∈ L) ∧
        ∀ (n a : ℕ), (∀ μ : AlgebraicClosure ℚ, μ ^ p ^ n = 1 → σ μ = μ ^ a) →
          x - (a : A) * z ∈ Ideal.span {((p ^ n : ℕ) : A)})

theorem IsStrictOrdinaryAt.isOrdinaryAt {ρ : GaloisRepAdic A} {p : ℕ}
    (h : ρ.IsStrictOrdinaryAt p) : ρ.IsOrdinaryAt p := fun P hP => by
  obtain ⟨L, hb, hD, hI, -⟩ := h.2 P hP
  exact ⟨L, hb, hD, hI⟩

end GaloisRepAdic

namespace GaloisRep

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

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

theorem ordinaryCondition_of_strictOrdinaryCondition {𝒪 : Type} [CommRing 𝒪] {p : ℕ}
    {S : Finset ℕ} {A : Type} [CommRing A] [IsLocalRing A] [Algebra 𝒪 A] {ρ : GaloisRepAdic A}
    (h : strictOrdinaryCondition 𝒪 p S ρ) : ordinaryCondition 𝒪 p S ρ :=
  ⟨h.1, h.2.1.isOrdinaryAt, h.2.2⟩

theorem minimalOrdinaryCondition_of_minimalStrictOrdinaryCondition {𝒪 : Type} [CommRing 𝒪]
    {p : ℕ} {S : Finset ℕ} {A : Type} [CommRing A] [IsLocalRing A] [Algebra 𝒪 A]
    {ρ : GaloisRepAdic A} (h : minimalStrictOrdinaryCondition 𝒪 p S ρ) :
    minimalOrdinaryCondition 𝒪 p S ρ :=
  ⟨ordinaryCondition_of_strictOrdinaryCondition h.1, h.2⟩

end GaloisRep

Statements phrased using this module (35)