Theorems · Theorem · commutative algebra

ModuleCat.exists_isRegular_tfae

∀ {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),
          Nontrivial ↑N →
            Module.Finite R ↑N →
              Module.support R ↑N ⊆ PrimeSpectrum.zeroLocus ↑I →
                ∀ i < n, Subsingleton (CategoryTheory.Abelian.Ext N M i),
        ∀ i < n, Subsingleton (CategoryTheory.Abelian.Ext (ModuleCat.of R (Shrink.{v, u} (R ⧸ I))) M i),
        ∃ N,
          Nontrivial ↑N ∧
            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].TFAE

The Rees theorem For any n : ℕ, Noetherian ring R, I : Ideal R, and finitely generated and nontrivial R-module M satisfying IM < M, the following are equivalent: * for any N : ModuleCat R finitely generated and nontrivial with support contained in the zero locus of I, ∀ i < n, Ext N M i = 0 * ∀ i < n, Ext (R ⧸ I) M i = 0 * there exists a N : ModuleCat R finitely generated and nontrivial with support equal to the zero locus of I, ∀ i < n, Ext N M i = 0 * there exists a M-regular sequence of length n with every element in I

Defined in

Mathlib.RingTheory.Depth.Rees

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingSmallIsNoetherianRingModule.Finite