Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_GaloisRep_DeformationCondition.lean

definition module

Artinian test algebras, deformation conditions, tangent finiteness

Fix a commutative local ring \mathcal{O}. GaloisRep.IsArtinianTestAlgebra is a Prop-valued structure on a local \mathcal{O}-algebra A with three fields: the structure map \mathcal{O}\to A is a local homomorphism, the composite \mathcal{O}\to A\to A/\mathfrak{m}_A is surjective (so A has the residue field of \mathcal{O}, expressed by surjectivity rather than by a chosen isomorphism), and A is an Artinian ring.

GaloisRep.IsDeformationCondition is a Prop-valued structure taking a predicate \mathcal{D} on GaloisRepAdic A, uniformly in local \mathcal{O}-algebras A — here a GaloisRepAdic A is a free rank-two A-module V together with a monoid homomorphism from \mathrm{Aut}_{\mathbb{Q}}(\overline{\mathbb{Q}}) to \mathrm{End}_A V that is \mathfrak{m}_A-adically continuous in the sense that for each n some finite subextension L/\mathbb{Q} has its pointwise stabiliser acting trivially on V/\mathfrak{m}_A^nV. Its five fields are: (1) on Artinian test algebras, \mathcal{D} is invariant under the existence of an A-linear Galois-equivariant isomorphism; (2) \mathcal{D} is preserved by base change B\otimes_A V along any local \mathcal{O}-algebra map \varphi:A\to B between Artinian test algebras; (3) it is reflected along such a \varphi when \varphi is injective; (4) if P presents the fibre product of f:A\to C and g:B\to C (all four Artinian test algebras, f\circ p_A=g\circ p_B, x\mapsto(p_Ax,p_Bx) injective, and every pair with fa=gb is of this form, with p_A,p_B local), then \mathcal{D} of both base changes implies \mathcal{D}(\rho); (5) for A Noetherian local, \mathfrak{m}_A-adically complete, with local structure map and surjective composite to the residue field, \mathcal{D}(\rho) holds exactly when \mathcal{D} holds of the base change along every surjective local \mathcal{O}-algebra map onto an Artinian test algebra.

GaloisRep.TangentFinite asserts, for \bar\rho a residual representation over k=\mathcal{O}/\mathfrak{m} and a predicate \mathcal{D}, that the type of those \rho over the dual numbers k[\varepsilon] satisfying \mathcal{D} whose residual representation is isomorphic to the base change of \bar\rho, taken modulo the equivalence relation of isomorphism of representations (the setoid being supplied explicitly from reflexivity, symmetry and transitivity), is finite.

Relation to Mathlib

Mathlib has no notion of a deformation condition or of deformations of Galois representations; these are the project's own, built from Mathlib's IsLocalRing, IsLocalHom, IsArtinianRing, IsAdicComplete, IsLocalRing.residue and DualNumber.

Where it is used

These are the axioms under which the deformation functor of a residual representation is shown to be representable by a complete local \mathcal{O}-algebra, uniformly in the condition \mathcal{D}; tangent finiteness is what makes the representing ring Noetherian. Concrete conditions (minimality, behaviour at p, prescribed level structure at auxiliary primes) are then checked against this interface in the Taylor–Wiles comparison of deformation rings with Hecke algebras.

References

  1. B. Mazur, Deforming Galois representations, in: Galois Groups over \mathbb{Q}, MSRI Publications 16, Springer, 1989, 385–437
  2. M. Schlessinger, Functors of Artin rings, Transactions of the American Mathematical Society 130 (1968), 208–222
  3. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154, §2.4

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_GaloisRep_Adic

set_option autoImplicit false

noncomputable section

namespace GaloisRep

open IsLocalRing

variable (𝒪 : Type) [CommRing 𝒪] [IsLocalRing 𝒪]

structure IsArtinianTestAlgebra (A : Type) [CommRing A] [IsLocalRing A] [Algebra 𝒪 A] : Prop where
  isLocalHom : IsLocalHom (algebraMap 𝒪 A)
  residue_surjective : Function.Surjective (IsLocalRing.residue A ∘ algebraMap 𝒪 A)
  isArtinian : IsArtinianRing A

structure IsDeformationCondition
    (𝒟 : ∀ ⦃A : Type⦄ [CommRing A] [IsLocalRing A] [Algebra 𝒪 A], GaloisRepAdic A → Prop) :
    Prop where

  of_isEquiv : ∀ ⦃A : Type⦄ [CommRing A] [IsLocalRing A] [Algebra 𝒪 A],
    IsArtinianTestAlgebra 𝒪 A → ∀ ⦃ρ ρ' : GaloisRepAdic A⦄, ρ.IsEquiv ρ' → 𝒟 ρ → 𝒟 ρ'

  baseChangeAlong : ∀ ⦃A B : Type⦄ [CommRing A] [IsLocalRing A] [Algebra 𝒪 A]
    [CommRing B] [IsLocalRing B] [Algebra 𝒪 B],
    IsArtinianTestAlgebra 𝒪 A → IsArtinianTestAlgebra 𝒪 B →
    ∀ (φ : A →ₐ[𝒪] B) (hφ : IsLocalHom (φ : A →+* B)) ⦃ρ : GaloisRepAdic A⦄,
      𝒟 ρ → 𝒟 (ρ.baseChangeAlong (φ : A →+* B) hφ)

  of_baseChangeAlong_injective : ∀ ⦃A B : Type⦄ [CommRing A] [IsLocalRing A] [Algebra 𝒪 A]
    [CommRing B] [IsLocalRing B] [Algebra 𝒪 B],
    IsArtinianTestAlgebra 𝒪 A → IsArtinianTestAlgebra 𝒪 B →
    ∀ (φ : A →ₐ[𝒪] B) (hφ : IsLocalHom (φ : A →+* B)), Function.Injective φ →
      ∀ ⦃ρ : GaloisRepAdic A⦄, 𝒟 (ρ.baseChangeAlong (φ : A →+* B) hφ) → 𝒟 ρ

  of_fibreProduct : ∀ ⦃A B C P : Type⦄ [CommRing A] [IsLocalRing A] [Algebra 𝒪 A]
    [CommRing B] [IsLocalRing B] [Algebra 𝒪 B] [CommRing C] [IsLocalRing C] [Algebra 𝒪 C]
    [CommRing P] [IsLocalRing P] [Algebra 𝒪 P],
    IsArtinianTestAlgebra 𝒪 A → IsArtinianTestAlgebra 𝒪 B → IsArtinianTestAlgebra 𝒪 C →
    IsArtinianTestAlgebra 𝒪 P →
    ∀ (f : A →ₐ[𝒪] C) (g : B →ₐ[𝒪] C) (pA : P →ₐ[𝒪] A) (pB : P →ₐ[𝒪] B)
      (hpA : IsLocalHom (pA : P →+* A)) (hpB : IsLocalHom (pB : P →+* B)),
      f.comp pA = g.comp pB →
      Function.Injective (fun x => (pA x, pB x)) →
      (∀ a b, f a = g b → ∃ x, pA x = a ∧ pB x = b) →
      ∀ ⦃ρ : GaloisRepAdic P⦄,
        𝒟 (ρ.baseChangeAlong (pA : P →+* A) hpA) → 𝒟 (ρ.baseChangeAlong (pB : P →+* B) hpB) → 𝒟 ρ

  iff_forall_surjective : ∀ ⦃A : Type⦄ [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    [IsAdicComplete (maximalIdeal A) A] [Algebra 𝒪 A],
    IsLocalHom (algebraMap 𝒪 A) → Function.Surjective (IsLocalRing.residue A ∘ algebraMap 𝒪 A) →
    ∀ (ρ : GaloisRepAdic A),
      𝒟 ρ ↔ ∀ ⦃B : Type⦄ [CommRing B] [IsLocalRing B] [Algebra 𝒪 B], IsArtinianTestAlgebra 𝒪 B →
        ∀ (q : A →ₐ[𝒪] B) (hq : IsLocalHom (q : A →+* B)), Function.Surjective q →
          𝒟 (ρ.baseChangeAlong (q : A →+* B) hq)

def TangentFinite (ρbar : ResidualGaloisRep (ResidueField 𝒪))
    (𝒟 : ∀ ⦃A : Type⦄ [CommRing A] [IsLocalRing A] [Algebra 𝒪 A], GaloisRepAdic A → Prop) : Prop :=
  letI : Algebra 𝒪 (DualNumber (ResidueField 𝒪)) :=
    ((algebraMap (ResidueField 𝒪) (DualNumber (ResidueField 𝒪))).comp
      (algebraMap 𝒪 (ResidueField 𝒪))).toAlgebra
  letI : Algebra (ResidueField 𝒪) (ResidueField (DualNumber (ResidueField 𝒪))) :=
    ((IsLocalRing.residue (DualNumber (ResidueField 𝒪))).comp
      (algebraMap (ResidueField 𝒪) (DualNumber (ResidueField 𝒪)))).toAlgebra
  Finite (Quotient (⟨fun ρ ρ' : {ρ : GaloisRepAdic (DualNumber (ResidueField 𝒪)) //
      𝒟 ρ ∧ ρ.residual.IsEquiv (ρbar.baseChange (ResidueField (DualNumber (ResidueField 𝒪)))) } =>
      ρ.1.IsEquiv ρ'.1, ⟨fun ρ => ⟨GaloisRepAdic.Equiv.refl ρ.1⟩,
        fun ⟨e⟩ => ⟨e.symm⟩, fun ⟨e⟩ ⟨e'⟩ => ⟨e.trans e'⟩⟩⟩ : Setoid _))

end GaloisRep

end

Statements phrased using this module (19)