ProjectiveDimension of quotient by regular element

For M a finitely generated module over Noetherian local ring R and an M-regular element x contained in the unique maximal ideal of R, projdim(M/xM) = projdim(M) + 1. The analogous version for quotient regular sequence is also provided.

Main Results

• ModuleCat.projectiveDimension_quotSMulTop_eq_succ_of_isSMulRegular : For M a finitely generated module over Noetherian local ring R and an M-regular element x contained in the unique maximal ideal of R, projdim(M/xM) = projdim(M) + 1

theorem ModuleCat.hasProjectiveDimensionLT_of_forall_finite {R : Type u} [CommRing R] [Small.{v, u} R] [IsNoetherianRing R] (M : ModuleCat R) [Module.Finite R ↑M] (n : ℕ) (h : ∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (CategoryTheory.Abelian.Ext M L n)) : CategoryTheory.HasProjectiveDimensionLT M n

theorem ModuleCat.projectiveDimension_quotSMulTop_eq_succ_of_isSMulRegular {R : Type u} [CommRing R] [Small.{v, u} R] [IsLocalRing R] [IsNoetherianRing R] (M : ModuleCat R) [Module.Finite R ↑M] (x : R) (reg : IsSMulRegular (↑M) x) (mem : x ∈ IsLocalRing.maximalIdeal R) : CategoryTheory.projectiveDimension ↧(QuotSMulTop x ↑M) = CategoryTheory.projectiveDimension M + 1

theorem ModuleCat.projectiveDimension_quotient_eq_add_length_of_isWeaklyRegular {R : Type u} [CommRing R] [Small.{v, u} R] [IsLocalRing R] [IsNoetherianRing R] (M : ModuleCat R) [Nontrivial ↑M] [Module.Finite R ↑M] (rs : List R) (reg : RingTheory.Sequence.IsWeaklyRegular (↑M) rs) (mem : ∀ r ∈ rs, r ∈ IsLocalRing.maximalIdeal R) : CategoryTheory.projectiveDimension ↧(↑M ⧸ Ideal.ofList rs • ⊤) = CategoryTheory.projectiveDimension M + ↑rs.length

theorem ModuleCat.projectiveDimension_quotient_eq_length {R : Type u} [CommRing R] [Small.{v, u} R] [IsLocalRing R] [IsNoetherianRing R] (rs : List R) (reg : RingTheory.Sequence.IsRegular R rs) : CategoryTheory.projectiveDimension ↧(Shrink.{v, u} (R ⧸ Ideal.ofList rs)) = ↑rs.length