Theorems · Theorem · commutative algebra

ModuleCat.subsingleton_ext_of_exists_isRegular

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

The implication (4) → (1) 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 there is an M-regular sequence rs contained in I, then Ext N M i = 0 for all i < rs.length.

Defined in

Mathlib.RingTheory.Depth.Rees

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingSmallIsNoetherianRingModule.FiniteModule.Finite