`Definitions/Def_Mathlib_RingTheory_RegularLocalRingFlatLocalAscent.lean`

definition module

Regular systems of parameters and flat local ascent of regularity

The module records two facts about regular local rings, in Mathlib's vocabulary: IsRegularLocalRing, Submodule.spanFinrank (the minimal number of generators), Ideal.ofList (the ideal generated by the entries of a list), and Sequence.IsWeaklyRegular/Sequence.IsRegular for lists.

First, existence of a regular system of parameters that is a regular sequence. exists_isWeaklyRegular_ofList_eq_maximalIdeal asserts that for a regular local ring R there is a list rs of elements of R whose entries generate \mathfrak m_R, whose length equals \operatorname{spanFinrank}(\mathfrak m_R), and which is weakly regular; exists_isRegular_ofList_eq_maximalIdeal upgrades weak regularity to Sequence.IsRegular, using that the entries lie in the maximal ideal. The auxiliary form exists_isWeaklyRegular_ofList_eq_maximalIdeal_aux states the same assertion as a claim quantified over a natural number n and over all regular local rings whose maximal ideal has spanFinrank equal to n, a shape suited to induction on n; the inductive step picks x \in \mathfrak m_R \setminus \mathfrak m_R^2 and cites the quotient engine for the regularity of R/(x) and for the drop of spanFinrank by one. The helper quotSpanSingletonEquivQuotSMulTop provides, for x in a commutative ring R, the R/(x)-linear equivalence between R/(x) and QuotSMulTop x R, coming from the identity of submodules (x) = x \cdot R with scalars extended along R \to R/(x).

Second, flat local ascent: isRegularLocalRing_of_flat_of_isRegularLocalRing_quotient takes a regular local ring R and an R-algebra S that is a flat R-module, a Noetherian local ring, with R \to S a local homomorphism, and assumes that the closed fibre S/\mathfrak m_R S is a regular local ring; it concludes that S is regular local. The proof maps a weakly regular generating sequence of \mathfrak m_R into S, where flatness keeps it weakly regular, and applies the regular-sequence descent criterion. flatLocalAscent_forall restates this with all arguments universally quantified across two universes.

Two calibration statements accompany these. gate_flat_ascent_runs_at_identity obtains \mathbb Z_p regular local by applying the ascent theorem with R = S = \mathbb Z_p. not_forall_ascent_dropping_flat shows the flatness hypothesis cannot simply be removed: taking R = \mathbb Z_2 and S = \mathbb Z_2/(4), the closed fibre is \mathbb Z_2/(2), hence regular, while S has a non-zero element of square zero and so is not a domain, hence not regular local.

Relation to Mathlib

All notions occurring in the statements are Mathlib's (IsRegularLocalRing, Sequence.IsWeaklyRegular, Sequence.IsRegular, Ideal.ofList, QuotSMulTop, Module.Flat, Submodule.spanFinrank); what the module adds are the two theorems — existence of a regular system of parameters forming a regular sequence, and ascent of regularity along a flat local homomorphism with regular closed fibre — together with the scalar-extension equivalence used to pass from R/(x) to QuotSMulTop x R.

Where it is used

Both statements belong to the local commutative algebra used when regularity of Noetherian local rings has to be transferred along flat local maps, as in the verification of regularity for local rings arising in the deformation-theoretic part of the modularity-lifting argument.

References

H. Matsumura, Commutative Ring Theory, Cambridge Studies in Advanced Mathematics 8, Cambridge University Press, 1986, Theorems 14.2 and 23.7
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.

264 lines
8 declarations
used in the statements of 0 theorems and imported by 1 proofs
imports 2 definition modules, and the statements of 1 theorems

Source file: Definitions/Def_Mathlib_RingTheory_RegularLocalRingFlatLocalAscent.lean

Imports

Theorems imported by this definition module

IsRegularLocalRing.isDomain

Imported by

Declarations

defRegularFlatLocalAscent.quotSpanSingletonEquivQuotSMulTop
theoremRegularFlatLocalAscent.exists_isWeaklyRegular_ofList_eq_maximalIdeal_aux
theoremRegularFlatLocalAscent.exists_isWeaklyRegular_ofList_eq_maximalIdeal
theoremRegularFlatLocalAscent.exists_isRegular_ofList_eq_maximalIdeal
theoremRegularFlatLocalAscent.isRegularLocalRing_of_flat_of_isRegularLocalRing_quotient
theoremRegularFlatLocalAscent.flatLocalAscent_forall
theoremRegularFlatLocalAscent.gate_flat_ascent_runs_at_identity
theoremRegularFlatLocalAscent.not_forall_ascent_dropping_flat

Source

import Mathlib
import Definitions.Def_Mathlib_RingTheory_RegularLocalRingQuotientRegular
import Theorems.Thm_IsRegularLocalRing_isDomain
import Definitions.Def_AlgebraicGeometry_RegularLocalRingRegularSequenceAscent

set_option autoImplicit false
set_option maxHeartbeats 800000
set_option synthInstance.maxHeartbeats 400000

noncomputable section

open IsLocalRing RingTheory
open scoped Pointwise

namespace RegularFlatLocalAscent

universe u v

def quotSpanSingletonEquivQuotSMulTop {R : Type u} [CommRing R] (x : R) :
    (R ⧸ Ideal.span {x}) ≃ₗ[R ⧸ Ideal.span {x}] QuotSMulTop x R :=
  (Submodule.quotEquivOfEq (Ideal.span {x}) (x • (⊤ : Submodule R R))
    (by rw [← Submodule.ideal_span_singleton_smul, Ideal.smul_eq_mul,
      Ideal.mul_top])).extendScalarsOfSurjective Ideal.Quotient.mk_surjective

theorem exists_isWeaklyRegular_ofList_eq_maximalIdeal_aux :
    ∀ (n : ℕ) (R : Type u) [CommRing R] [IsRegularLocalRing R],
      (maximalIdeal R).spanFinrank = n →
      ∃ rs : List R, Ideal.ofList rs = maximalIdeal R ∧ rs.length = n ∧
        Sequence.IsWeaklyRegular R rs := by
  intro n
  induction n with
  | zero =>
    intro R _ _ hn
    refine ⟨[], ?_, rfl, Sequence.IsWeaklyRegular.nil R R⟩
    rw [Ideal.ofList_nil]
    exact ((Submodule.spanFinrank_eq_zero_iff_eq_bot
      ((maximalIdeal R).fg_of_isNoetherianRing)).mp hn).symm
  | succ n ih =>
    intro R _ _ hn

    have hbot : maximalIdeal R ≠ ⊥ := by
      intro h
      have h0 : (maximalIdeal R).spanFinrank = 0 :=
        (Submodule.spanFinrank_eq_zero_iff_eq_bot
          ((maximalIdeal R).fg_of_isNoetherianRing)).mpr h
      omega

    have hne : maximalIdeal R ^ 2 ≠ maximalIdeal R := by
      intro h
      refine hbot (Submodule.eq_bot_of_le_smul_of_le_jacobson_bot (maximalIdeal R)
        (maximalIdeal R) (IsNoetherian.noetherian _) ?_
        (IsLocalRing.maximalIdeal_le_jacobson _))
      rw [Ideal.smul_eq_mul, ← pow_two]
      exact le_of_eq h.symm
    obtain ⟨x, hx, hx2⟩ := SetLike.exists_of_lt
      (lt_of_le_of_ne (Ideal.pow_le_self two_ne_zero) hne)

    haveI hQ : IsRegularLocalRing (R ⧸ Ideal.span {x}) :=
      RegularQuotientEngine.isRegularLocalRing_quotient_span_singleton R hx hx2
    have hdrop : (maximalIdeal (R ⧸ Ideal.span {x})).spanFinrank + 1
        = (maximalIdeal R).spanFinrank :=
      RegularQuotientEngine.spanFinrank_maximalIdeal_quotient_succ_eq R hx hx2
    obtain ⟨rs', hof', hlen', hreg'⟩ := ih (R ⧸ Ideal.span {x}) (by omega)

    have hsurj : Function.Surjective (Ideal.Quotient.mk (Ideal.span {x})) :=
      Ideal.Quotient.mk_surjective
    obtain ⟨lifts, hliftmap, hliftlen⟩ :
        ∃ lifts : List R,
          lifts.map (Ideal.Quotient.mk (Ideal.span {x})) = rs' ∧
            lifts.length = rs'.length := by
      refine ⟨rs'.map (Function.surjInv hsurj), ?_, by rw [List.length_map]⟩
      rw [List.map_map,
        show (⇑(Ideal.Quotient.mk (Ideal.span {x})) ∘ Function.surjInv hsurj) = id from
          funext fun b => Function.surjInv_eq hsurj b,
        List.map_id]
    haveI : IsLocalHom (Ideal.Quotient.mk (Ideal.span {x})) :=
      IsLocalHom.of_surjective _ hsurj

    have hofeq : Ideal.ofList (x :: lifts) = maximalIdeal R := by
      apply le_antisymm
      · rw [Ideal.ofList_cons, sup_le_iff]
        constructor
        · rwa [Ideal.span_le, Set.singleton_subset_iff]
        · refine Ideal.span_le.mpr fun r hr => ?_
          show r ∈ maximalIdeal R
          have hmkmem : Ideal.Quotient.mk (Ideal.span {x}) r
              ∈ maximalIdeal (R ⧸ Ideal.span {x}) := by
            rw [← hof']
            exact Ideal.subset_span (by
              rw [← hliftmap]
              exact List.mem_map.mpr ⟨r, hr, rfl⟩)
          rw [IsLocalRing.mem_maximalIdeal, mem_nonunits_iff] at hmkmem ⊢
          exact fun hu => hmkmem (RingHom.isUnit_map _ hu)
      · intro a ha
        have hanu : ¬IsUnit a := by
          rwa [IsLocalRing.mem_maximalIdeal, mem_nonunits_iff] at ha
        have hmka : Ideal.Quotient.mk (Ideal.span {x}) a
            ∈ Ideal.map (Ideal.Quotient.mk (Ideal.span {x})) (Ideal.ofList lifts) := by
          rw [Ideal.map_ofList, hliftmap, hof', IsLocalRing.mem_maximalIdeal,
            mem_nonunits_iff]
          exact fun hu => hanu (IsUnit.of_map _ a hu)
        have hcomap : a ∈ Ideal.comap (Ideal.Quotient.mk (Ideal.span {x}))
            (Ideal.map (Ideal.Quotient.mk (Ideal.span {x})) (Ideal.ofList lifts)) :=
          Ideal.mem_comap.mpr hmka
        rw [Ideal.comap_map_of_surjective _ hsurj, ← RingHom.ker_eq_comap_bot,
          Ideal.mk_ker, sup_comm (Ideal.ofList lifts) (Ideal.span {x})] at hcomap
        rw [Ideal.ofList_cons]
        exact hcomap

    haveI : IsDomain R := IsRegularLocalRing.isDomain R
    have hx0 : x ≠ 0 := fun h => hx2 (h ▸ Submodule.zero_mem _)
    have hxreg : IsSMulRegular R x :=
      Module.Flat.isSMulRegular_of_nonZeroDivisors (mem_nonZeroDivisors_of_ne_zero hx0)

    have hwR : Sequence.IsWeaklyRegular R (x :: lifts) := by
      rw [Sequence.isWeaklyRegular_cons_iff']
      refine ⟨hxreg, ?_⟩
      rw [hliftmap]
      exact ((quotSpanSingletonEquivQuotSMulTop x).isWeaklyRegular_congr rs').mp hreg'
    refine ⟨x :: lifts, hofeq, ?_, hwR⟩
    rw [List.length_cons, hliftlen, hlen']

theorem exists_isWeaklyRegular_ofList_eq_maximalIdeal (R : Type u) [CommRing R]
    [IsRegularLocalRing R] :
    ∃ rs : List R, Ideal.ofList rs = maximalIdeal R ∧
      rs.length = (maximalIdeal R).spanFinrank ∧ Sequence.IsWeaklyRegular R rs :=
  exists_isWeaklyRegular_ofList_eq_maximalIdeal_aux ((maximalIdeal R).spanFinrank) R rfl

theorem exists_isRegular_ofList_eq_maximalIdeal (R : Type u) [CommRing R]
    [IsRegularLocalRing R] :
    ∃ rs : List R, Ideal.ofList rs = maximalIdeal R ∧
      rs.length = (maximalIdeal R).spanFinrank ∧ Sequence.IsRegular R rs := by
  obtain ⟨rs, hof, hlen, hw⟩ := exists_isWeaklyRegular_ofList_eq_maximalIdeal R
  refine ⟨rs, hof, hlen,
    Sequence.IsRegular.of_isWeaklyRegular_of_mem_maximalIdeal R (fun r hr => ?_) hw⟩
  rw [← hof]
  exact Ideal.subset_span hr

open RegularLocalRingQuotientAscent in

theorem isRegularLocalRing_of_flat_of_isRegularLocalRing_quotient
    (R : Type u) (S : Type v) [CommRing R] [IsRegularLocalRing R] [CommRing S] [Algebra R S]
    [Module.Flat R S] [IsLocalRing S] [IsLocalHom (algebraMap R S)] [IsNoetherianRing S]
    (hfiber : IsRegularLocalRing (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))) :
    IsRegularLocalRing S := by
  obtain ⟨rs, hof, -, hreg⟩ := exists_isWeaklyRegular_ofList_eq_maximalIdeal R
  have hwS : Sequence.IsWeaklyRegular S (rs.map (algebraMap R S)) := hreg.of_flat
  have hmem : ∀ s ∈ rs.map (algebraMap R S), s ∈ maximalIdeal S := by
    intro s hs
    obtain ⟨r, hr, rfl⟩ := List.mem_map.mp hs
    have hrm : r ∈ maximalIdeal R := by
      rw [← hof]
      exact Ideal.subset_span hr
    rw [IsLocalRing.mem_maximalIdeal, mem_nonunits_iff] at hrm ⊢
    exact fun hu => hrm (IsUnit.of_map (algebraMap R S) r hu)
  have hid : Ideal.ofList (rs.map (algebraMap R S))
      = Ideal.map (algebraMap R S) (maximalIdeal R) := by
    rw [← Ideal.map_ofList, hof]
  have hquot : IsRegularLocalRing (S ⧸ Ideal.ofList (rs.map (algebraMap R S))) := by
    rw [hid]
    exact hfiber
  exact isRegularLocalRing_of_isRegularLocalRing_quotient_isWeaklyRegular
    (rs.map (algebraMap R S)) hmem hwS hquot

theorem flatLocalAscent_forall :
    ∀ (R : Type u) (S : Type v) [CommRing R] [CommRing S] [IsRegularLocalRing R]
      [Algebra R S] [Module.Flat R S] [IsLocalRing S] [IsLocalHom (algebraMap R S)]
      [IsNoetherianRing S],
      IsRegularLocalRing (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)) →
      IsRegularLocalRing S :=
  fun R S _ _ _ _ _ _ _ _ hfiber =>
    isRegularLocalRing_of_flat_of_isRegularLocalRing_quotient R S hfiber

theorem gate_flat_ascent_runs_at_identity (p : ℕ) [Fact p.Prime] :
    IsRegularLocalRing ℤ_[p] := by
  haveI : IsRegularLocalRing ℤ_[p] :=
    RegularLocalRingQuotientAscent.gate_isRegularLocalRing_padicInt_via_sequence p
  haveI : IsNoetherianRing ℤ_[p] := PrincipalIdealRing.isNoetherianRing
  haveI : IsLocalHom (algebraMap ℤ_[p] ℤ_[p]) := by
    rw [Algebra.algebraMap_self]
    exact ⟨fun a h => h⟩
  have hfib : IsRegularLocalRing
      (ℤ_[p] ⧸ Ideal.map (algebraMap ℤ_[p] ℤ_[p]) (maximalIdeal ℤ_[p])) := by
    rw [Algebra.algebraMap_self, Ideal.map_id, PadicInt.maximalIdeal_eq_span_p,
      ← Ideal.ofList_singleton]
    exact RegularLocalRingQuotientAscent.gate_padicInt_quotient_ofList_isRegularLocalRing p
  exact isRegularLocalRing_of_flat_of_isRegularLocalRing_quotient ℤ_[p] ℤ_[p] hfib

theorem not_forall_ascent_dropping_flat :
    ¬ ∀ (R S : Type) [CommRing R] [CommRing S] [IsRegularLocalRing R] [Algebra R S]
        [IsLocalRing S] [IsLocalHom (algebraMap R S)] [IsNoetherianRing S],
        IsRegularLocalRing (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)) →
        IsRegularLocalRing S := by
  intro hforall
  haveI : Fact (Nat.Prime 2) := ⟨Nat.prime_two⟩
  haveI : IsRegularLocalRing ℤ_[2] :=
    RegularLocalRingQuotientAscent.gate_isRegularLocalRing_padicInt_via_sequence 2
  haveI : IsNoetherianRing ℤ_[2] := PrincipalIdealRing.isNoetherianRing

  have hspan : maximalIdeal ℤ_[2] = Ideal.span {((2 : ℕ) : ℤ_[2])} :=
    PadicInt.maximalIdeal_eq_span_p
  have h2m : ((2 : ℕ) : ℤ_[2]) ∈ maximalIdeal ℤ_[2] := by
    rw [hspan]
    exact Ideal.mem_span_singleton_self _
  have h4m : ((2 : ℕ) : ℤ_[2]) ^ 2 ∈ maximalIdeal ℤ_[2] :=
    Ideal.pow_mem_of_mem _ h2m 2 two_pos

  haveI : IsLocalRing (ℤ_[2] ⧸ Ideal.span {((2 : ℕ) : ℤ_[2]) ^ 2}) :=
    RegularQuotientEngine.isLocalRing_quotient_span_singleton ℤ_[2] h4m
  haveI : IsLocalHom (algebraMap ℤ_[2] (ℤ_[2] ⧸ Ideal.span {((2 : ℕ) : ℤ_[2]) ^ 2})) := by
    rw [Ideal.Quotient.algebraMap_eq]
    exact IsLocalHom.of_surjective _ Ideal.Quotient.mk_surjective

  have hsup : Ideal.span {((2 : ℕ) : ℤ_[2]) ^ 2} ⊔ maximalIdeal ℤ_[2]
      = Ideal.span {((2 : ℕ) : ℤ_[2])} := by
    rw [hspan]
    refine sup_eq_right.mpr ?_
    rw [Ideal.span_le, Set.singleton_subset_iff]
    exact Ideal.mem_span_singleton.mpr (dvd_pow_self _ two_ne_zero)
  haveI : IsRegularLocalRing (ℤ_[2] ⧸ Ideal.ofList [((2 : ℕ) : ℤ_[2])]) :=
    RegularLocalRingQuotientAscent.gate_padicInt_quotient_ofList_isRegularLocalRing 2
  have hofeq2 : Ideal.ofList [((2 : ℕ) : ℤ_[2])]
      = Ideal.span {((2 : ℕ) : ℤ_[2]) ^ 2} ⊔ maximalIdeal ℤ_[2] := by
    rw [Ideal.ofList_singleton]
    exact hsup.symm
  have hfib : IsRegularLocalRing
      ((ℤ_[2] ⧸ Ideal.span {((2 : ℕ) : ℤ_[2]) ^ 2}) ⧸
        Ideal.map (algebraMap ℤ_[2] (ℤ_[2] ⧸ Ideal.span {((2 : ℕ) : ℤ_[2]) ^ 2}))
          (maximalIdeal ℤ_[2])) := by
    rw [Ideal.Quotient.algebraMap_eq]
    exact IsRegularLocalRing.of_ringEquiv
      ((Ideal.quotEquivOfEq hofeq2).trans
        (DoubleQuot.quotQuotEquivQuotSup _ _).symm)

  have hSreg : IsRegularLocalRing (ℤ_[2] ⧸ Ideal.span {((2 : ℕ) : ℤ_[2]) ^ 2}) :=
    hforall ℤ_[2] (ℤ_[2] ⧸ Ideal.span {((2 : ℕ) : ℤ_[2]) ^ 2}) hfib

  haveI := hSreg
  haveI : IsDomain (ℤ_[2] ⧸ Ideal.span {((2 : ℕ) : ℤ_[2]) ^ 2}) :=
    IsRegularLocalRing.isDomain _
  have hmk0 : (Ideal.Quotient.mk (Ideal.span {((2 : ℕ) : ℤ_[2]) ^ 2}) ((2 : ℕ) : ℤ_[2])) ^ 2
      = 0 := by
    rw [← map_pow, Ideal.Quotient.eq_zero_iff_mem]
    exact Ideal.mem_span_singleton_self _
  have hmkne : Ideal.Quotient.mk (Ideal.span {((2 : ℕ) : ℤ_[2]) ^ 2}) ((2 : ℕ) : ℤ_[2])
      ≠ 0 := by
    rw [ne_eq, Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton]
    intro hdvd
    obtain ⟨c, hc⟩ := hdvd
    have h2ne : ((2 : ℕ) : ℤ_[2]) ≠ 0 := Nat.cast_ne_zero.mpr two_ne_zero
    have hcancel : (1 : ℤ_[2]) = ((2 : ℕ) : ℤ_[2]) * c := by
      refine mul_left_cancel₀ h2ne ?_
      rw [mul_one]
      calc ((2 : ℕ) : ℤ_[2]) = ((2 : ℕ) : ℤ_[2]) ^ 2 * c := hc
        _ = ((2 : ℕ) : ℤ_[2]) * (((2 : ℕ) : ℤ_[2]) * c) := by ring
    have h2nu : ¬IsUnit ((2 : ℕ) : ℤ_[2]) := by
      rwa [IsLocalRing.mem_maximalIdeal, mem_nonunits_iff] at h2m
    exact h2nu (IsUnit.of_mul_eq_one c hcancel.symm)
  exact hmkne (pow_eq_zero_iff two_ne_zero |>.mp hmk0)

end RegularFlatLocalAscent

end

Statements phrased using this module (0)

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