Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_Deformations_MvPowerSeriesObj.lean

definition moduleadapted from the Imperial College London FLT project: FLT/Deformations/Categories.lean

Power series rings as objects of the pro-Artinian category

This module places multivariate formal power series rings in the category \mathcal{C}_{\mathcal O} of local pro-Artinian \mathcal O-algebras. Two preliminary lemmas concern a commutative topological local ring R that is pro-Artinian (linearly topologised by ideals, T_0, complete, and with R/I Artinian for every open ideal I): every x in the maximal ideal of R is topologically nilpotent, because each open ideal contains a power of the maximal ideal; and, for a finite index type \sigma, a family x : \sigma \to R with all x_j in the maximal ideal satisfies Mathlib's MvPowerSeries.HasEval, so power series may be evaluated at it (the cofiniteness condition being vacuous for finite \sigma).

For a commutative ring \mathcal O and an index type \sigma, \mathrm{MvPowerSeries}\,\sigma\,\mathcal O carries the product topology over that of \mathcal O; it is compact when \mathcal O is. When \mathcal O is local, each variable X_j lies in the maximal ideal (its constant coefficient vanishes), the structure map \mathcal O \to \mathcal O[\![\sigma]\!] is a local homomorphism, and the residue field is reached from \mathcal O, since a power series is a unit modulo the maximal ideal precisely according to its constant term; if moreover \mathcal O is Noetherian with the adic topology and compact, the power series ring is pro-Artinian, all open quotients being finite. Combining these gives IsLocalProartinianAlgebra π“ž (MvPowerSeries Οƒ π“ž).

Finally, for \mathcal O local Noetherian with finite residue field and complete for the \mathfrak m-adic topology, mvPowerSeriesObj π“ž n is the object of ProartinianCat π“ž with carrier \mathcal O[\![X_1,\dots,X_n]\!] (n variables indexed by Fin n), and mvPowerSeriesObjX j denotes its j-th variable, shown to lie in the maximal ideal.

Relation to Mathlib

MvPowerSeries, its product (WithPiTopology) topology and the evaluation condition MvPowerSeries.HasEval are Mathlib's; the predicates IsProartinian, IsResidueAlgebra, IsLocalProartinianAlgebra and the category ProartinianCat are the project's own.

Where it is used

The objects \mathcal O[\![X_1,\dots,X_n]\!] are the free objects of the deformation category \mathcal{C}_{\mathcal O}: every object with finite-dimensional tangent space is a quotient of one of them, and power series rings in this form are the source of the presentations of deformation rings and of the power series ring over which the Taylor–Wiles patching argument is run.

References

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

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_Deformations_ProartinianCat

set_option autoImplicit false

universe u

namespace Deformation

open CategoryTheory IsLocalRing MvPowerSeries

local notation3:max "𝓴" π“ž:max => (IsLocalRing.ResidueField π“ž)

namespace ProartinianCat

section Nilpotence

variable {R : Type u} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable [IsLocalRing R] [IsProartinian R]

lemma isTopologicallyNilpotent_of_mem_maximalIdeal {x : R} (hx : x ∈ maximalIdeal R) :
    IsTopologicallyNilpotent x := by
  rw [IsTopologicallyNilpotent,
    (IsLinearTopology.hasBasis_open_ideal (R := R)).tendsto_right_iff]
  intro I hI
  obtain ⟨N, hN⟩ := exists_maximalIdeal_pow_le_of_isProartinian I hI
  filter_upwards [Filter.eventually_ge_atTop N] with n hn
  exact hN (Ideal.pow_le_pow_right hn (Ideal.pow_mem_pow hx n))

lemma hasEval_of_forall_mem_maximalIdeal {Οƒ : Type*} [Finite Οƒ] {x : Οƒ β†’ R}
    (hx : βˆ€ j, x j ∈ maximalIdeal R) : MvPowerSeries.HasEval x where
  hpow j := isTopologicallyNilpotent_of_mem_maximalIdeal (hx j)
  tendsto_zero := by
    rw [Filter.cofinite_eq_bot]
    exact Filter.tendsto_bot

end Nilpotence

section Object

open MvPowerSeries.WithPiTopology

variable (π“ž : Type u) [CommRing π“ž] (Οƒ : Type)

omit [CommRing π“ž] in

lemma compactSpace_mvPowerSeries [TopologicalSpace π“ž] [CompactSpace π“ž] :
    CompactSpace (MvPowerSeries Οƒ π“ž) :=
  inferInstanceAs (CompactSpace ((Οƒ β†’β‚€ β„•) β†’ π“ž))

lemma X_mem_maximalIdeal [IsLocalRing π“ž] (j : Οƒ) :
    MvPowerSeries.X j ∈ maximalIdeal (MvPowerSeries Οƒ π“ž) := by
  rw [mem_maximalIdeal, mem_nonunits_iff, MvPowerSeries.isUnit_iff_constantCoeff,
    MvPowerSeries.constantCoeff_X]
  exact fun h => h.ne_zero rfl

lemma isProartinian_mvPowerSeries [IsLocalRing π“ž] [IsNoetherianRing π“ž] [TopologicalSpace π“ž]
    [IsTopologicalRing π“ž] [IsAdicTopology π“ž] [CompactSpace π“ž] :
    IsProartinian (MvPowerSeries Οƒ π“ž) := by
  haveI : CompactSpace (MvPowerSeries Οƒ π“ž) := compactSpace_mvPowerSeries π“ž Οƒ
  exact
    { isArtinianRing_quotient := fun I hI => by
        have : Finite (MvPowerSeries Οƒ π“ž β§Έ I) := AddSubgroup.quotient_finite_of_isOpen _ hI
        exact isArtinian_of_finite }

lemma isLocalHom_algebraMap_mvPowerSeries [IsLocalRing π“ž] :
    IsLocalHom (algebraMap π“ž (MvPowerSeries Οƒ π“ž)) := by
  constructor
  intro a ha
  rw [← MvPowerSeries.c_eq_algebraMap, MvPowerSeries.isUnit_iff_constantCoeff,
    MvPowerSeries.constantCoeff_C] at ha
  exact ha

lemma isResidueAlgebra_mvPowerSeries [IsLocalRing π“ž] :
    IsResidueAlgebra π“ž (MvPowerSeries Οƒ π“ž) := by
  constructor
  intro y
  obtain ⟨f, rfl⟩ := Ideal.Quotient.mk_surjective y
  refine ⟨MvPowerSeries.constantCoeff f, ?_⟩
  show residue _ _ = residue _ _
  rw [← sub_eq_zero, ← map_sub, residue_eq_zero_iff, mem_maximalIdeal, mem_nonunits_iff,
    MvPowerSeries.isUnit_iff_constantCoeff]
  simp [← MvPowerSeries.c_eq_algebraMap]

lemma isLocalProartinianAlgebra_mvPowerSeries [IsLocalRing π“ž] [IsNoetherianRing π“ž]
    [TopologicalSpace π“ž] [IsTopologicalRing π“ž] [IsAdicTopology π“ž] [CompactSpace π“ž] :
    IsLocalProartinianAlgebra π“ž (MvPowerSeries Οƒ π“ž) := by
  haveI : IsProartinian (MvPowerSeries Οƒ π“ž) := isProartinian_mvPowerSeries π“ž Οƒ
  haveI : IsLocalHom (algebraMap π“ž (MvPowerSeries Οƒ π“ž)) :=
    isLocalHom_algebraMap_mvPowerSeries π“ž Οƒ
  haveI : IsResidueAlgebra π“ž (MvPowerSeries Οƒ π“ž) := isResidueAlgebra_mvPowerSeries π“ž Οƒ
  exact ⟨⟩

end Object

section Category

variable (π“ž : Type u) [CommRing π“ž] [IsLocalRing π“ž] [IsNoetherianRing π“ž]
variable [Finite (ResidueField π“ž)] [IsAdicComplete (maximalIdeal π“ž) π“ž]

noncomputable def mvPowerSeriesObj (n : β„•) : ProartinianCat π“ž where
  carrier := MvPowerSeries (Fin n) π“ž
  topologicalSpace :=
    letI := (maximalIdeal π“ž).adicTopology
    WithPiTopology.instTopologicalSpace π“ž
  isLocalProartinianAlgebra :=
    letI := (maximalIdeal π“ž).adicTopology
    letI : IsTopologicalRing π“ž := (RingSubgroupsBasis.toRingFilterBasis _).isTopologicalRing
    letI : IsAdicTopology π“ž := ⟨rfl⟩
    letI : CompactSpace π“ž := compactSpace_of_finite_residueField
    isLocalProartinianAlgebra_mvPowerSeries π“ž (Fin n)

variable {π“ž}

noncomputable def mvPowerSeriesObjX {n : β„•} (j : Fin n) : (mvPowerSeriesObj π“ž n).carrier :=
  MvPowerSeries.X j

lemma mvPowerSeriesObjX_mem_maximalIdeal {n : β„•} (j : Fin n) :
    mvPowerSeriesObjX (π“ž := π“ž) j ∈ maximalIdeal (mvPowerSeriesObj π“ž n).carrier :=
  X_mem_maximalIdeal π“ž (Fin n) j

end Category

end ProartinianCat

end Deformation

Statements phrased using this module (1)