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

• IsSMulRegular.subsingleton_linearMap_iff : for finitely generated R-module M, N, Hom(N, M) = 0 iff there is an M-regular element in Module.annihilator R N. This is the case for n = 0 in the Rees theorem.

• 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 IsSMulRegular.linearMap_subsingleton_of_mem_annihilator {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {r : R} (reg : IsSMulRegular M r) (mem_ann : r ∈ Module.annihilator R N) : Subsingleton (N →ₗ[R] M)

theorem IsSMulRegular.subsingleton_linearMap_iff {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [IsNoetherianRing R] [Module.Finite R M] [Module.Finite R N] : Subsingleton (N →ₗ[R] M) ↔ ∃ r ∈ Module.annihilator R N, IsSMulRegular M r