Associated primes, dimension, and quotients by a regular element

Facts about the associated primes of a module M over a commutative ring R. The first two are used to bound the depth of M by the dimensions dim (R ⧸ p) of its associated primes p:

• IsAssociatedPrime.ringKrullDim_quotient_le_supportDim: for an associated prime p of M, the dimension of R ⧸ p is at most the dimension of the support of M.
• IsAssociatedPrime.exists_le_isAssociatedPrime_quotSMulTop: if R is Noetherian, M is finite, and x is M-regular and lies in the Jacobson radical of the annihilator of M, then every associated prime of M lies in an associated prime of M ⧸ x M. This comes from Nakayama's lemma applied to the elements of M killed by p.

A separate fact describes the associated primes of a reduced ring:

• IsAssociatedPrime.mem_minimalPrimes_of_isReduced: every associated prime of a reduced ring is a minimal prime.

For an R-algebra S, two facts compare the associated primes of an S-module M over S and over R, using Submodule.comap_colon_singleton from TauCeti.RingTheory.Ideal.Colon:

• IsAssociatedPrime.comap: the contraction of an associated prime over S is an associated prime over R.
• IsAssociatedPrime.exists_isAssociatedPrime_comap_eq: if S is Noetherian, every maximal ideal of R that is an associated prime over R is such a contraction.

Over a Noetherian ring, prime avoidance characterises the ideals containing a regular element:

• Ideal.exists_mem_isSMulRegular_iff_of_finite_associatedPrimes, Ideal.exists_mem_isSMulRegular_iff: an ideal I contains an M-regular element if and only if it lies in no associated prime of M, for M with finitely many associated primes, in particular for M finite (Stacks, Tag 00LL).

References

• H. Matsumura, Commutative Ring Theory, proof of Theorem 17.2.

theorem IsAssociatedPrime.mem_minimalPrimes_of_isReduced {R : Type u_1} [CommSemiring R] {p : Ideal R} [IsReduced R] (hp : IsAssociatedPrime p R) : p ∈ minimalPrimes R

Every associated prime of a reduced ring is a minimal prime: an associated prime is the radical of the annihilator of some x ≠ 0, so it lies in a minimal prime that does not contain x.

theorem IsAssociatedPrime.ringKrullDim_quotient_le_supportDim {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {p : Ideal R} (hp : IsAssociatedPrime p M) : ringKrullDim (R ⧸ p) ≤ Module.supportDim R M

The quotient by an associated prime of M has dimension at most the dimension of the support of M: every prime containing an associated prime lies in the support.

theorem IsAssociatedPrime.exists_le_isAssociatedPrime_quotSMulTop {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {p : Ideal R} [IsNoetherianRing R] [Module.Finite R M] {x : R} (hp : IsAssociatedPrime p M) (reg : IsSMulRegular M x) (hx : x ∈ (Module.annihilator R M).jacobson) : ∃ (q : Ideal R), IsAssociatedPrime q (QuotSMulTop x M) ∧ p ≤ q

Let M be a finite module over a Noetherian ring and x an M-regular element of the Jacobson radical of the annihilator of M. Every associated prime of M is contained in an associated prime of M ⧸ x M.

theorem Ideal.exists_mem_isSMulRegular_iff_of_finite_associatedPrimes {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [IsNoetherianRing R] (hfin : (associatedPrimes R M).Finite) (I : Ideal R) : (∃ a ∈ I, IsSMulRegular M a) ↔ ∀ p ∈ associatedPrimes R M, ¬I ≤ p

Prime avoidance for regular elements. An ideal I of a Noetherian ring contains an element that is regular on a module M with finitely many associated primes if and only if I is contained in no associated prime of M. This generalises the finite-module case (Stacks, Tag 00LL).

theorem Ideal.exists_mem_isSMulRegular_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [IsNoetherianRing R] [Module.Finite R M] (I : Ideal R) : (∃ a ∈ I, IsSMulRegular M a) ↔ ∀ p ∈ associatedPrimes R M, ¬I ≤ p

Prime avoidance for regular elements. An ideal I of a Noetherian ring contains an element that is regular on a finite module M if and only if I is contained in no associated prime of M.

theorem IsAssociatedPrime.comap {R : Type u_3} {S : Type u_4} {M : Type u_5} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] {q : Ideal S} (hq : IsAssociatedPrime q M) : IsAssociatedPrime (Ideal.comap (algebraMap R S) q) M

An associated prime of an S-module M contracts to an associated prime of M as an R-module.

theorem IsAssociatedPrime.exists_isAssociatedPrime_comap_eq {R : Type u_3} {S : Type u_4} {M : Type u_5} [CommSemiring R] [CommSemiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [IsNoetherianRing S] {p : Ideal R} [hmax : p.IsMaximal] (hp : IsAssociatedPrime p M) : ∃ (q : Ideal S), IsAssociatedPrime q M ∧ Ideal.comap (algebraMap R S) q = p

Let S be a Noetherian R-algebra. A maximal ideal of R that is an associated prime of an S-module M, viewed as an R-module, is the contraction of an associated prime of M over S.