Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_Patching_SystemTypes.lean

definition moduleadapted from the Imperial College London FLT project: FLT/Patching/Utils/TopologicallyFG.lean

Typeclass vocabulary for Taylor–Wiles patching systems

Six declarations set up the language in which an abstract patching argument over an index type \iota can be stated. IsLocalRing.IsAdicTopology R, for a commutative local ring R carrying a topological ring structure, is the one-field class asserting that this topology is the \mathfrak{m}_R-adic one, in Mathlib's sense of IsAdic (maximalIdeal R). Algebra.TopologicallyFG R S, for an R-algebra S that is a topological ring, asserts that there is a finite subset s \subseteq S whose generated subalgebra R[s] is dense in S; an instance records that an R-algebra of finite type is topologically finitely generated in this sense. Module.depth R M, for a module M over a local ring R, is defined with values in \mathbb{N} \cup \{\infty\} as the supremum of the lengths of those lists s of elements of R which are weakly M-regular (Mathlib's RingTheory.Sequence.IsWeaklyRegular) and all of whose entries lie in \mathfrak{m}_R; no nonvanishing condition on M/sM is imposed, and the supremum of the empty set of lengths cannot occur since the empty list qualifies.

Three classes express the uniformity and convergence conditions consumed by patching. For a family (R_i)_{i \in \iota} of local rings, Algebra.UniformlyBoundedRank asks that for every k there be a single n \in \mathbb{N} with \#(R_i/\mathfrak{m}_{R_i}^k) < n for all i, the cardinalities being taken as Nat.card, which vanishes on infinite types, so that the bound constrains the finite quotients. For a family (M_i) of modules over a fixed ring R, Module.UniformlyBoundedRank asks for one n \in \mathbb{N} bounding every rank \operatorname{rank}_{R/\operatorname{Ann}_R(M_i)} M_i, the module structure over the quotient by the annihilator being the canonical one. Finally, IsPatchingSystem R M F, for a topological ring R, a family (M_i) of R-modules and a filter F on \iota, asserts that for every ideal \alpha \subseteq R that is open as a subset, one has \operatorname{Ann}_R(M_i) \le \alpha for F-almost all i; that is, the annihilators tend to 0 along F.

Relation to Mathlib

The ingredients IsAdic, Algebra.FiniteType, RingTheory.Sequence.IsWeaklyRegular, Module.annihilator and Module.quotientAnnihilator are Mathlib's; the adic-topology class, the topological finite generation class (implied by Algebra.FiniteType, registered as an instance), the \mathbb{N}\cup\{\infty\}-valued depth of a module over a local ring, and the three patching predicates are the project's own.

Where it is used

These predicates are the hypotheses on a tower (\Lambda, R_i, M_i) that the Taylor–Wiles patching method consumes: the R_i are deformation rings at the successive Taylor–Wiles levels and the M_i the associated modules of automorphic forms, and the uniform bounds together with the vanishing of the annihilators along a filter (an ultrafilter, in the applications) produce a patched module over a patched ring whose freeness is detected by a depth and dimension count. They thereby underlie the abstract form of the R = \mathbb{T} statement used for modularity lifting in the proof of Fermat's Last Theorem.

References

  1. R. Taylor and A. Wiles, Ring-theoretic properties of certain Hecke algebras, Annals of Mathematics 141 (1995), 553–572
  2. M. Kisin, Moduli of finite flat group schemes, and modularity, Annals of Mathematics 170 (2009), 1085–1180
  3. W. Bruns and J. Herzog, Cohen–Macaulay Rings, Cambridge Studies in Advanced Mathematics 39, Cambridge University Press, 1993

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

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology ↗
import Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic ↗
import Mathlib.RingTheory.FiniteType ↗
import Mathlib.Topology.Algebra.Ring.Basic ↗
import Mathlib.RingTheory.Regular.RegularSequence ↗
import Mathlib.Algebra.Module.Torsion.Basic ↗
import Mathlib.LinearAlgebra.Dimension.Finrank ↗
import Mathlib.Order.Filter.Ultrafilter.Defs ↗
import Mathlib.Data.ENat.Lattice ↗

set_option autoImplicit false

open IsLocalRing

namespace IsLocalRing

class IsAdicTopology (R : Type*) [CommRing R] [IsLocalRing R]
    [TopologicalSpace R] [IsTopologicalRing R] : Prop where
  isAdic : IsAdic (maximalIdeal R)

end IsLocalRing

class Algebra.TopologicallyFG (R S : Type*) [CommRing R] [Ring S] [Algebra R S]
    [TopologicalSpace S] [IsTopologicalRing S] : Prop where
  out : ∃ s : Finset S, Dense (Algebra.adjoin R (s : Set S) : Set S)

instance (priority := 100) {R S : Type*} [CommRing R] [Ring S] [Algebra R S]
    [TopologicalSpace S] [IsTopologicalRing S] [Algebra.FiniteType R S] :
    Algebra.TopologicallyFG R S where
  out := have ⟨s, hs⟩ := Algebra.FiniteType.out (R := R) (A := S); ⟨s, by simp [hs]⟩

open RingTheory in

noncomputable def Module.depth (R M : Type*) [CommRing R] [IsLocalRing R]
    [AddCommGroup M] [Module R M] : ℕ∞ :=
  sSup { List.length s | (s : List R)
    (_ : Sequence.IsWeaklyRegular M s)
    (_ : ∀ r ∈ s, r ∈ maximalIdeal R) }

section PatchingPredicates

attribute [local instance] Module.quotientAnnihilator

variable {ι : Type*}

class Algebra.UniformlyBoundedRank (R : ι → Type*) [∀ i, CommRing (R i)]
    [∀ i, IsLocalRing (R i)] : Prop where
  cond : ∀ k, ∃ n : ℕ, ∀ i, Nat.card (R i ⧸ maximalIdeal (R i) ^ k) < n

class Module.UniformlyBoundedRank (R : Type*) (M : ι → Type*) [CommRing R]
    [∀ i, AddCommGroup (M i)] [∀ i, Module R (M i)] : Prop where
  cond : ∃ n : ℕ, ∀ i, Module.rank (R ⧸ Module.annihilator R (M i)) (M i) < n

class IsPatchingSystem (R : Type*) (M : ι → Type*) [CommRing R] [TopologicalSpace R]
    [∀ i, AddCommGroup (M i)] [∀ i, Module R (M i)] (F : Filter ι) : Prop where
  cond : ∀ α : Ideal R, IsOpen (X := R) α → ∀ᶠ i in F, Module.annihilator R (M i) ≤ α

end PatchingPredicates

Statements phrased using this module (12)