Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_AlgebraicGeometry_RegularLocalRingRegularSequenceAscent.lean

definition module

Ascent of regular local rings along regular sequences

The module establishes, for a Noetherian local ring A, that regularity descends from a quotient by a regular sequence back to A, the quotient being taken by Ideal.ofList rs, the ideal generated by the entries of a list rs.

Two preliminary facts are recorded for a commutative ring A: an element acting regularly on A by scalar multiplication lies in nonZeroDivisors A; and if rs satisfies Sequence.IsRegular A rs then Ideal.ofList rs is not the unit ideal, whence, over a local ring, every entry of rs lies in maximalIdeal A. Next, the minimal number of generators spanFinrank of Ideal.ofList rs is bounded by rs.length, and consequently, for Noetherian local A with A/\mathrm{ofList}(rs) local, \mu(\mathfrak m_A) \le \mu(\mathfrak m_{A/\mathrm{ofList}(rs)}) + |rs|.

The main theorem isRegularLocalRing_of_isRegularLocalRing_quotient_ofList combines this generator count with the dimension identity \dim(A/\mathrm{ofList}(rs)) + |rs| = \dim A for a regular sequence, and with the characterisation of regularity by \mu(\mathfrak m) = \dim, to conclude IsRegularLocalRing A. Variants assume instead that rs is weakly regular with all entries in the maximal ideal, or transfer the conclusion along a surjection f : A \to B with RingHom.ker f = Ideal.ofList rs. A second, independent route proves the same implication by induction on |rs|, at each step passing to A/(x), identifying A/(x) with QuotSMulTop x A so that the image sequence is again regular, and invoking the one-element ascent.

Two families of concrete checks follow: [p] is a regular sequence in \mathbb Z_p with \mathbb Z_p/\mathrm{ofList}[p] \cong \mathbb Z/p regular, giving IsRegularLocalRing ℤ_[p] by either route together with the dimension jump; and over the dual numbers \mathbb Q[\varepsilon] the singleton [\varepsilon] fails to be regular, so that the analogous implication with regularity of the sequence weakened to mere membership in the maximal ideal is false.

Relation to Mathlib

The notions used are Mathlib's: RingTheory.Sequence.IsRegular and IsWeaklyRegular, Ideal.ofList, Submodule.spanFinrank and IsRegularLocalRing. What is added here is the list-indexed ascent statement, built on the one-element case proved in the imported module AlgebraicGeometry_RegularLocalRingQuotientNonZeroDivisorAscent.

Where it is used

Recognising local rings as regular — in particular \mathbb Z_p, and quotients of power series rings by regular sequences — is the standard commutative-algebra input when deformation and Hecke rings are compared, as in the patching argument.

References

  1. R. Hartshorne, Algebraic Geometry, Graduate Texts in Mathematics 52, Springer, 1977, Theorem II.8.24
  2. H. Matsumura, Commutative Ring Theory, Cambridge Studies in Advanced Mathematics 8, Cambridge University Press, 1986
  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_AlgebraicGeometry_RegularLocalRingRegularSequenceAscent.lean

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_AlgebraicGeometry_RegularLocalRingQuotientNonZeroDivisorAscent

set_option autoImplicit false
set_option maxHeartbeats 800000
set_option synthInstance.maxHeartbeats 400000

noncomputable section

open IsLocalRing RingTheory Pointwise

namespace RegularLocalRingQuotientAscent

universe u

section Preliminaries

variable {A : Type*} [CommRing A]

theorem mem_nonZeroDivisors_of_isSMulRegular {x : A} (h : IsSMulRegular A x) :
    x ∈ nonZeroDivisors A := by
  rw [mem_nonZeroDivisors_iff]
  constructor
  · intro a ha
    apply h
    simp only [smul_eq_mul, mul_zero]
    exact ha
  · intro a ha
    apply h
    simp only [smul_eq_mul, mul_zero]
    rw [mul_comm]
    exact ha

theorem ofList_ne_top_of_isRegular {rs : List A} (h : Sequence.IsRegular A rs) :
    Ideal.ofList rs ≠ ⊤ := by
  intro htop
  apply h.top_ne_smul
  rw [htop]
  simp

theorem mem_maximalIdeal_of_isRegular [IsLocalRing A] {rs : List A}
    (h : Sequence.IsRegular A rs) :
    ∀ r ∈ rs, r ∈ maximalIdeal A := fun _ hr =>
  IsLocalRing.le_maximalIdeal (ofList_ne_top_of_isRegular h) (Ideal.subset_span hr)

theorem spanFinrank_ofList_le_length (rs : List A) :
    (Ideal.ofList rs).spanFinrank ≤ rs.length := by
  classical

  have hset : {r : A | r ∈ rs} = (↑rs.toFinset : Set A) := by
    ext r
    simp
  have hfin : Set.Finite {r : A | r ∈ rs} := by
    rw [hset]
    exact rs.toFinset.finite_toSet
  have hcard : ({r : A | r ∈ rs}).ncard ≤ rs.length := by
    rw [hset, Set.ncard_coe_finset]
    exact rs.toFinset_card_le

  have hspan : (Submodule.span A {r : A | r ∈ rs}).spanFinrank ≤ ({r : A | r ∈ rs}).ncard :=
    Submodule.spanFinrank_span_le_ncard_of_finite hfin
  rw [Ideal.submodule_span_eq] at hspan
  exact hspan.trans hcard

end Preliminaries

section Ascent

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

theorem spanFinrank_maximalIdeal_le_quotient_ofList_add_length (rs : List A)
    [IsLocalRing (A ⧸ Ideal.ofList rs)] :
    (maximalIdeal A).spanFinrank
      ≤ (maximalIdeal (A ⧸ Ideal.ofList rs)).spanFinrank + rs.length := by

  have hker_eq : RingHom.ker (Ideal.Quotient.mk (Ideal.ofList rs)) = Ideal.ofList rs :=
    Ideal.mk_ker
  have hkerfg : Submodule.FG (RingHom.ker (Ideal.Quotient.mk (Ideal.ofList rs))) := by
    rw [hker_eq]
    exact IsNoetherian.noetherian _
  have hker_le : (RingHom.ker (Ideal.Quotient.mk (Ideal.ofList rs))).spanFinrank
      ≤ rs.length := by
    rw [hker_eq]
    exact spanFinrank_ofList_le_length rs

  have h1 := spanFinrank_maximalIdeal_le_of_surjective (Ideal.Quotient.mk (Ideal.ofList rs))
    Ideal.Quotient.mk_surjective hkerfg
  omega

theorem isRegularLocalRing_of_isRegularLocalRing_quotient_ofList (rs : List A)
    (hreg : Sequence.IsRegular A rs)
    (hquot : IsRegularLocalRing (A ⧸ Ideal.ofList rs)) :
    IsRegularLocalRing A := by
  haveI := hquot

  have hkey : (maximalIdeal A).spanFinrank
      ≤ (maximalIdeal (A ⧸ Ideal.ofList rs)).spanFinrank + rs.length :=
    spanFinrank_maximalIdeal_le_quotient_ofList_add_length rs

  have hq : ((maximalIdeal (A ⧸ Ideal.ofList rs)).spanFinrank : WithBot ℕ∞)
      = ringKrullDim (A ⧸ Ideal.ofList rs) := hquot.spanFinrank_maximalIdeal

  have hdim : ringKrullDim (A ⧸ Ideal.ofList rs) + rs.length = ringKrullDim A :=
    ringKrullDim_add_length_eq_ringKrullDim_of_isRegular rs hreg

  refine IsRegularLocalRing.of_spanFinrank_maximalIdeal_le A ?_
  rw [← hdim, ← hq]
  exact_mod_cast hkey

theorem isRegularLocalRing_of_isRegularLocalRing_quotient_isWeaklyRegular (rs : List A)
    (hmem : ∀ r ∈ rs, r ∈ maximalIdeal A)
    (hreg : Sequence.IsWeaklyRegular A rs)
    (hquot : IsRegularLocalRing (A ⧸ Ideal.ofList rs)) :
    IsRegularLocalRing A :=
  isRegularLocalRing_of_isRegularLocalRing_quotient_ofList rs
    (Sequence.IsRegular.of_isWeaklyRegular_of_mem_maximalIdeal A hmem hreg) hquot

theorem isRegularLocalRing_of_isRegularLocalRing_quotient_regularSequence (rs : List A)
    (hmem : ∀ r ∈ rs, r ∈ maximalIdeal A)
    (hreg : Sequence.IsRegular A rs)
    (hquot : IsRegularLocalRing (A ⧸ Ideal.ofList rs)) :
    IsRegularLocalRing A :=
  isRegularLocalRing_of_isRegularLocalRing_quotient_isWeaklyRegular rs hmem
    hreg.toIsWeaklyRegular hquot

theorem isRegularLocalRing_of_surjective_ker_ofList {B : Type*} [CommRing B]
    (f : A →+* B) (hf : Function.Surjective f) (rs : List A)
    (hker : RingHom.ker f = Ideal.ofList rs)
    (hreg : Sequence.IsRegular A rs)
    (hB : IsRegularLocalRing B) :
    IsRegularLocalRing A := by
  haveI := hB

  have e : (A ⧸ Ideal.ofList rs) ≃+* B :=
    (Ideal.quotEquivOfEq hker.symm).trans (RingHom.quotientKerEquivOfSurjective hf)
  exact isRegularLocalRing_of_isRegularLocalRing_quotient_ofList rs hreg
    (IsRegularLocalRing.of_ringEquiv e.symm)

end Ascent

section IteratedAscent

theorem isRegularLocalRing_of_isRegularLocalRing_quotient_ofList_iterated :
    ∀ (n : ℕ) (A : Type u) [CommRing A] [IsLocalRing A] [IsNoetherianRing A] (rs : List A),
      rs.length = n → Sequence.IsRegular A rs →
      IsRegularLocalRing (A ⧸ Ideal.ofList rs) → IsRegularLocalRing A := by
  intro n
  induction n with
  | zero =>
    intro A _ _ _ rs hlen hreg hquot
    cases rs with
    | nil =>

      rw [Ideal.ofList_nil] at hquot
      haveI := hquot
      exact IsRegularLocalRing.of_ringEquiv (RingEquiv.quotientBot A)
    | cons x rest => exact absurd hlen (by simp)
  | succ n IH =>
    intro A _ _ _ rs hlen hreg hquot
    cases rs with
    | nil => exact absurd hlen (by simp)
    | cons x rest =>
      have hrestlen : rest.length = n := by simpa using hlen

      obtain ⟨hxreg, hrestreg⟩ := (Sequence.isRegular_cons_iff' A x rest).mp hreg

      have hxm : x ∈ maximalIdeal A :=
        mem_maximalIdeal_of_isRegular hreg x (by simp)
      have hxnzd : x ∈ nonZeroDivisors A := mem_nonZeroDivisors_of_isSMulRegular hxreg

      have hxne : Ideal.span {x} ≠ ⊤ := by
        rw [Ne, Ideal.span_singleton_eq_top]
        intro hu
        exact (maximalIdeal.isMaximal A).ne_top (Ideal.eq_top_of_isUnit_mem _ hxm hu)
      haveI : Nontrivial (A ⧸ Ideal.span {x}) := Ideal.Quotient.nontrivial_iff.mpr hxne
      haveI : IsLocalRing (A ⧸ Ideal.span {x}) :=
        IsLocalRing.of_surjective' (Ideal.Quotient.mk (Ideal.span {x}))
          Ideal.Quotient.mk_surjective

      have hsub : (Ideal.span {x} : Submodule A A) = x • (⊤ : Submodule A A) := by
        rw [← Submodule.ideal_span_singleton_smul]
        simp
      have e' : (A ⧸ Ideal.span {x}) ≃ₗ[A ⧸ Ideal.span {x}] QuotSMulTop x A :=
        LinearEquiv.extendScalarsOfSurjective
          (by rw [Ideal.Quotient.algebraMap_eq]; exact Ideal.Quotient.mk_surjective)
          (Submodule.quotEquivOfEq _ _ hsub)
      have hrestreg' : Sequence.IsRegular (A ⧸ Ideal.span {x})
          (rest.map (Ideal.Quotient.mk (Ideal.span {x}))) :=
        (LinearEquiv.isRegular_congr e' _).mpr hrestreg

      have hquot' : IsRegularLocalRing ((A ⧸ Ideal.span {x}) ⧸
          Ideal.ofList (rest.map (Ideal.Quotient.mk (Ideal.span {x})))) := by
        haveI := hquot
        refine IsRegularLocalRing.of_ringEquiv (R := A ⧸ Ideal.ofList (x :: rest)) ?_
        exact (Ideal.quotEquivOfEq (Ideal.ofList_cons x rest)).trans
          (((DoubleQuot.quotQuotEquivQuotSup (Ideal.span {x}) (Ideal.ofList rest)).symm).trans
            (Ideal.quotEquivOfEq (Ideal.map_ofList _ _)))

      have hB : IsRegularLocalRing (A ⧸ Ideal.span {x}) :=
        IH (A ⧸ Ideal.span {x}) (rest.map (Ideal.Quotient.mk (Ideal.span {x})))
          (by rw [List.length_map]; exact hrestlen) hrestreg' hquot'

      exact isRegularLocalRing_of_isRegularLocalRing_quotient hxm hxnzd hB

theorem isRegularLocalRing_of_isRegularLocalRing_quotient_ofList_via_iterated_ascent
    {A : Type u} [CommRing A] [IsLocalRing A] [IsNoetherianRing A] (rs : List A)
    (hreg : Sequence.IsRegular A rs)
    (hquot : IsRegularLocalRing (A ⧸ Ideal.ofList rs)) :
    IsRegularLocalRing A :=
  isRegularLocalRing_of_isRegularLocalRing_quotient_ofList_iterated rs.length A rs rfl
    hreg hquot

end IteratedAscent

section Gates

variable (p : ℕ) [Fact p.Prime]

theorem gate_padicInt_isRegular_singleton_p :
    Sequence.IsRegular ℤ_[p] [(p : ℤ_[p])] := by
  haveI : IsNoetherianRing ℤ_[p] := PrincipalIdealRing.isNoetherianRing
  apply Sequence.IsRegular.of_isWeaklyRegular_of_mem_maximalIdeal
  · intro r hr
    rw [List.mem_singleton] at hr
    subst hr
    rw [PadicInt.maximalIdeal_eq_span_p]
    exact Ideal.mem_span_singleton_self _
  · rw [Sequence.isWeaklyRegular_singleton_iff]
    exact Module.Flat.isSMulRegular_of_nonZeroDivisors
      (mem_nonZeroDivisors_of_ne_zero
        (Nat.cast_ne_zero.mpr (Fact.out (p := p.Prime)).ne_zero))

theorem gate_padicInt_quotient_ofList_isRegularLocalRing :
    IsRegularLocalRing (ℤ_[p] ⧸ Ideal.ofList [(p : ℤ_[p])]) := by
  rw [Ideal.ofList_singleton]
  exact IsRegularLocalRing.of_ringEquiv (padicIntQuotientSpanPEquiv p).symm

theorem gate_isRegularLocalRing_padicInt_via_sequence : IsRegularLocalRing ℤ_[p] := by
  haveI : IsNoetherianRing ℤ_[p] := PrincipalIdealRing.isNoetherianRing
  exact isRegularLocalRing_of_isRegularLocalRing_quotient_ofList _
    (gate_padicInt_isRegular_singleton_p p)
    (gate_padicInt_quotient_ofList_isRegularLocalRing p)

theorem gate_isRegularLocalRing_padicInt_via_iterated_ascent : IsRegularLocalRing ℤ_[p] := by
  haveI : IsNoetherianRing ℤ_[p] := PrincipalIdealRing.isNoetherianRing
  exact isRegularLocalRing_of_isRegularLocalRing_quotient_ofList_via_iterated_ascent _
    (gate_padicInt_isRegular_singleton_p p)
    (gate_padicInt_quotient_ofList_isRegularLocalRing p)

theorem gate_padicInt_dimension_jump_length :
    ringKrullDim (ℤ_[p] ⧸ Ideal.ofList [(p : ℤ_[p])])
      + ([(p : ℤ_[p])].length : WithBot ℕ∞) = ringKrullDim ℤ_[p] := by
  haveI : IsNoetherianRing ℤ_[p] := PrincipalIdealRing.isNoetherianRing
  exact ringKrullDim_add_length_eq_ringKrullDim_of_isRegular _
    (gate_padicInt_isRegular_singleton_p p)

end Gates

section Teeth

theorem not_isRegular_dualNumber_singleton_eps :
    ¬ Sequence.IsRegular (DualNumber ℚ) [(DualNumber.eps : DualNumber ℚ)] := by
  intro h
  obtain ⟨h1, -⟩ := (Sequence.isRegular_cons_iff' (DualNumber ℚ) DualNumber.eps []).mp h
  exact eps_notMem_nonZeroDivisors (mem_nonZeroDivisors_of_isSMulRegular h1)

theorem not_forall_isRegularLocalRing_of_quotient_ofList_dropping_isRegular :
    ¬ (∀ (A : Type) [CommRing A] [IsLocalRing A] [IsNoetherianRing A] (rs : List A),
        (∀ r ∈ rs, r ∈ maximalIdeal A) → IsRegularLocalRing (A ⧸ Ideal.ofList rs) →
        IsRegularLocalRing A) := by
  intro hclaim
  haveI : IsNoetherianRing (DualNumber ℚ) := PrincipalIdealRing.isNoetherianRing
  refine not_isRegularLocalRing_dualNumber
    (hclaim (DualNumber ℚ) [DualNumber.eps] ?_ ?_)
  · intro r hr
    rw [List.mem_singleton] at hr
    subst hr
    exact eps_mem_maximalIdeal
  · rw [Ideal.ofList_singleton]
    exact quotient_span_eps_isRegularLocalRing

end Teeth

end RegularLocalRingQuotientAscent

/--
info: 'RegularLocalRingQuotientAscent.mem_nonZeroDivisors_of_isSMulRegular' depends on axioms: [propext, Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.mem_nonZeroDivisors_of_isSMulRegular

/--
info: 'RegularLocalRingQuotientAscent.ofList_ne_top_of_isRegular' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.ofList_ne_top_of_isRegular

/--
info: 'RegularLocalRingQuotientAscent.mem_maximalIdeal_of_isRegular' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.mem_maximalIdeal_of_isRegular

/--
info: 'RegularLocalRingQuotientAscent.spanFinrank_ofList_le_length' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.spanFinrank_ofList_le_length

/--
info: 'RegularLocalRingQuotientAscent.spanFinrank_maximalIdeal_le_quotient_ofList_add_length' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.spanFinrank_maximalIdeal_le_quotient_ofList_add_length

/--
info: 'RegularLocalRingQuotientAscent.isRegularLocalRing_of_isRegularLocalRing_quotient_ofList' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.isRegularLocalRing_of_isRegularLocalRing_quotient_ofList

/--
info: 'RegularLocalRingQuotientAscent.isRegularLocalRing_of_isRegularLocalRing_quotient_isWeaklyRegular' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.isRegularLocalRing_of_isRegularLocalRing_quotient_isWeaklyRegular

/--
info: 'RegularLocalRingQuotientAscent.isRegularLocalRing_of_isRegularLocalRing_quotient_regularSequence' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.isRegularLocalRing_of_isRegularLocalRing_quotient_regularSequence

/--
info: 'RegularLocalRingQuotientAscent.isRegularLocalRing_of_surjective_ker_ofList' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.isRegularLocalRing_of_surjective_ker_ofList

/--
info: 'RegularLocalRingQuotientAscent.isRegularLocalRing_of_isRegularLocalRing_quotient_ofList_iterated' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.isRegularLocalRing_of_isRegularLocalRing_quotient_ofList_iterated

/--
info: 'RegularLocalRingQuotientAscent.isRegularLocalRing_of_isRegularLocalRing_quotient_ofList_via_iterated_ascent' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.isRegularLocalRing_of_isRegularLocalRing_quotient_ofList_via_iterated_ascent

/--
info: 'RegularLocalRingQuotientAscent.gate_padicInt_isRegular_singleton_p' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.gate_padicInt_isRegular_singleton_p

/--
info: 'RegularLocalRingQuotientAscent.gate_padicInt_quotient_ofList_isRegularLocalRing' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.gate_padicInt_quotient_ofList_isRegularLocalRing

/--
info: 'RegularLocalRingQuotientAscent.gate_isRegularLocalRing_padicInt_via_sequence' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.gate_isRegularLocalRing_padicInt_via_sequence

/--
info: 'RegularLocalRingQuotientAscent.gate_isRegularLocalRing_padicInt_via_iterated_ascent' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.gate_isRegularLocalRing_padicInt_via_iterated_ascent

/--
info: 'RegularLocalRingQuotientAscent.gate_padicInt_dimension_jump_length' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.gate_padicInt_dimension_jump_length

/--
info: 'RegularLocalRingQuotientAscent.not_isRegular_dualNumber_singleton_eps' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.not_isRegular_dualNumber_singleton_eps

/--
info: 'RegularLocalRingQuotientAscent.not_forall_isRegularLocalRing_of_quotient_ofList_dropping_isRegular' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
-/
#guard_msgs in
#print axioms RegularLocalRingQuotientAscent.not_forall_isRegularLocalRing_of_quotient_ofList_dropping_isRegular

end

Statements phrased using this module (0)

No statement module imports it directly (it is used through other definition modules or by proofs).