Theorems · Theorem · commutative algebra

ModuleCat.exists_isRegular_of_exists_subsingleton_ext

∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] [IsNoetherianRing R] (I : Ideal R) (n : ℕ)
  (M : ModuleCat R) [Module.Finite R ↑M],
  I • ⊤ < ⊤ →
    ∀ (N : ModuleCat R) [Module.Finite R ↑N],
      Module.support R ↑N = PrimeSpectrum.zeroLocus ↑I →
        (∀ i < n, Subsingleton (CategoryTheory.Abelian.Ext N M i)) →
          ∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs

The implication (3) → (4) of exists_isRegular_tfae: for M N finitely generated module over Noetherian ring R and ideal I satisfying IM < M and Supp N = V(I), if Ext N M i = 0 for all i < n, then there exists an M-regular sequence of length n contained in I.

Defined in

Mathlib.RingTheory.Depth.Rees

Cited by

1 results in Mathlib

Foundations

Depth 121 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingSmallIsNoetherianRingModule.FiniteModule.Finite