The Rees theorem

In this file we prove the Rees theorem for depth, which relates the vanishing of certain Ext groups and the length of a maximal regular sequence in a certain ideal.

Main results

• ModuleCat.exists_isRegular_tfae (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 (A⧸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

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

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

theorem ModuleCat.exists_isRegular_tfae {R : Type u} [CommRing R] [Small.{v, u} R] [IsNoetherianRing R] (I : Ideal R) (n : ℕ) (M : ModuleCat R) [Module.Finite R ↑M] (smul_lt : 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 (of R (Shrink.{v, u} (R ⧸ I))) 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), ∃ (rs : List R), 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 (A⧸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