Associated primes of a module

We provide the definition and related lemmas about associated primes of modules.

Main definition

• IsAssociatedPrime: IsAssociatedPrime I M if the prime ideal I is the radical of the annihilator of some x : M.
• associatedPrimes: The set of associated primes of a module.

Main results

• exists_le_isAssociatedPrime_of_isNoetherianRing: In a Noetherian ring, any ann(x) is contained in an associated prime for x ≠ 0.
• associatedPrimes.eq_singleton_of_isPrimary: In a Noetherian ring, I.radical is the only associated prime of R ⧸ I when I is primary.

Implementation details

The presence of the radical in the definition of IsAssociatedPrime is slightly nonstandard but gives the correct characterization of the prime ideals of any minimal primary decomposition in the non-Noetherian setting (see Theorem 4.5 in Atiyah-Macdonald). If the ring R is assumed to be Noetherian, then the radical can be dropped from the definition (see isAssociatedPrime_iff).

See also Stacks: Lemma 0566 which states that a prime p is minimal among primes containing an annihilator an element of M if and only if p R_p is an associated prime of M_p (including the radical).

TODO

Generalize this to a non-commutative setting once there are annihilator for non-commutative rings.

References

• M. F. Atiyah and I. G. Macdonald, Introduction to commutative algebra

structure Submodule.IsAssociatedPrime {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (N : Submodule R M) (I : Ideal R) extends I.IsPrime : Prop

I : Ideal R is an associated prime of a submodule N : Submodule R M if I is prime and I = (colon N {x}).radical for some x : M.

• ne_top' : I ≠ ⊤
• mem_or_mem' {x y : R} : x * y ∈ I → x ∈ I ∨ y ∈ I
• eq_radical_colon : ∃ (x : M), I = (N.colon {x}).radical

def Submodule.associatedPrimes {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (N : Submodule R M) : Set (Ideal R)

The set of associated primes of a submodule.

Equations

• N.associatedPrimes = {I : Ideal R | N.IsAssociatedPrime I}

theorem Submodule.isAssociatedPrime_def {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} {I : Ideal R} : N.IsAssociatedPrime I ↔ I.IsPrime ∧ ∃ (x : M), I = (N.colon {x}).radical

theorem Submodule.isAssociatedPrime_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} {I : Ideal R} [IsNoetherianRing R] : N.IsAssociatedPrime I ↔ I.IsPrime ∧ ∃ (x : M), I = N.colon {x}

instance Submodule.instIsPrimeValIdealMemSetAssociatedPrimes {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} (I : ↑N.associatedPrimes) : (↑I).IsPrime

theorem Submodule.AssociatePrimes.mem_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} {I : Ideal R} : I ∈ N.associatedPrimes ↔ N.IsAssociatedPrime I

def IsAssociatedPrime {R : Type u_1} [CommSemiring R] (I : Ideal R) (M : Type u_2) [AddCommMonoid M] [Module R M] : Prop

IsAssociatedPrime I M if the prime ideal I is the radical of the annihilator of some x : M.

Equations

• IsAssociatedPrime I M = ⊥.IsAssociatedPrime I

def associatedPrimes (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] : Set (Ideal R)

The set of associated primes of a module.

Equations

• associatedPrimes R M = {I : Ideal R | IsAssociatedPrime I M}

theorem AssociatedPrimes.mem_iff {R : Type u_1} [CommSemiring R] {I : Ideal R} {M : Type u_2} [AddCommMonoid M] [Module R M] : I ∈ associatedPrimes R M ↔ IsAssociatedPrime I M

@[deprecated AssociatedPrimes.mem_iff (since := "2025-11-24")]

theorem AssociatePrimes.mem_iff {R : Type u_1} [CommSemiring R] {I : Ideal R} {M : Type u_2} [AddCommMonoid M] [Module R M] : I ∈ associatedPrimes R M ↔ IsAssociatedPrime I M

Alias of AssociatedPrimes.mem_iff.

theorem IsAssociatedPrime.isPrime {R : Type u_1} [CommSemiring R] {I : Ideal R} {M : Type u_2} [AddCommMonoid M] [Module R M] (h : IsAssociatedPrime I M) : I.IsPrime

instance instIsPrimeValIdealMemSetAssociatedPrimes {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] (I : ↑(associatedPrimes R M)) : (↑I).IsPrime

theorem isAssociatedPrime_iff {R : Type u_1} [CommSemiring R] {I : Ideal R} {M : Type u_2} [AddCommMonoid M] [Module R M] [IsNoetherianRing R] : IsAssociatedPrime I M ↔ I.IsPrime ∧ ∃ (x : M), I = ⊥.colon {x}

theorem IsAssociatedPrime.map_of_injective {R : Type u_1} [CommSemiring R] {I : Ideal R} {M : Type u_2} [AddCommMonoid M] [Module R M] {M' : Type u_3} [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') (h : IsAssociatedPrime I M) (hf : Function.Injective ⇑f) : IsAssociatedPrime I M'

theorem LinearEquiv.isAssociatedPrime_iff {R : Type u_1} [CommSemiring R] {I : Ideal R} {M : Type u_2} [AddCommMonoid M] [Module R M] {M' : Type u_3} [AddCommMonoid M'] [Module R M'] (l : M ≃ₗ[R] M') : IsAssociatedPrime I M ↔ IsAssociatedPrime I M'

theorem not_isAssociatedPrime_of_subsingleton {R : Type u_1} [CommSemiring R] {I : Ideal R} {M : Type u_2} [AddCommMonoid M] [Module R M] [Subsingleton M] : ¬IsAssociatedPrime I M

theorem exists_le_isAssociatedPrime_of_isNoetherianRing (R : Type u_1) [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] [H : IsNoetherianRing R] (x : M) (hx : x ≠ 0) : ∃ (P : Ideal R), IsAssociatedPrime P M ∧ ⊥.colon {x} ≤ P

theorem associatedPrimes.subset_of_injective {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {M' : Type u_3} [AddCommMonoid M'] [Module R M'] {f : M →ₗ[R] M'} (hf : Function.Injective ⇑f) : associatedPrimes R M ⊆ associatedPrimes R M'

If M → M' is injective, then the set of associated primes of M is contained in that of M'.

theorem associatedPrimes.subset_union_of_exact {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {M' : Type u_3} [AddCommMonoid M'] [Module R M'] {f : M →ₗ[R] M'} {M'' : Type u_4} [AddCommMonoid M''] [Module R M''] {g : M' →ₗ[R] M''} (hf : Function.Injective ⇑f) (hfg : Function.Exact ⇑f ⇑g) : associatedPrimes R M' ⊆ associatedPrimes R M ∪ associatedPrimes R M''

If 0 → M → M' → M'' is an exact sequence, then the set of associated primes of M' is contained in the union of those of M and M''.

theorem associatedPrimes.prod (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] (M' : Type u_3) [AddCommMonoid M'] [Module R M'] : associatedPrimes R (M × M') = associatedPrimes R M ∪ associatedPrimes R M'

The set of associated primes of the product of two modules is equal to the union of those of the two modules.

theorem LinearEquiv.AssociatedPrimes.eq {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {M' : Type u_3} [AddCommMonoid M'] [Module R M'] (l : M ≃ₗ[R] M') : associatedPrimes R M = associatedPrimes R M'

theorem associatedPrimes.eq_empty_of_subsingleton {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] [Subsingleton M] : associatedPrimes R M = ∅

theorem associatedPrimes.nonempty (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] [IsNoetherianRing R] [Nontrivial M] : (associatedPrimes R M).Nonempty

theorem biUnion_associatedPrimes_eq_zero_divisors (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] [IsNoetherianRing R] : ⋃ p ∈ associatedPrimes R M, ↑p = {r : R | ∃ (x : M), x ≠ 0 ∧ r • x = 0}

theorem biUnion_associatedPrimes_eq_compl_nonZeroDivisors (R : Type u_1) [CommSemiring R] [IsNoetherianRing R] : ⋃ p ∈ associatedPrimes R R, ↑p = (↑(nonZeroDivisors R))ᶜ

theorem IsAssociatedPrime.annihilator_le {R : Type u_1} [CommSemiring R] {I : Ideal R} {M : Type u_2} [AddCommMonoid M] [Module R M] (h : IsAssociatedPrime I M) : ⊤.annihilator ≤ I

theorem isAssociatedPrime_iff_exists_injective_linearMap {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] [IsNoetherianRing R] : IsAssociatedPrime I M ↔ I.IsPrime ∧ ∃ (f : R ⧸ I →ₗ[R] M), Function.Injective ⇑f

theorem IsAssociatedPrime.eq_radical {R : Type u_1} [CommRing R] {I J : Ideal R} (hI : I.IsPrimary) (h : IsAssociatedPrime J (R ⧸ I)) : J = I.radical

theorem associatedPrimes.eq_singleton_of_isPrimary {R : Type u_1} [CommRing R] {I : Ideal R} [IsNoetherianRing R] (hI : I.IsPrimary) : associatedPrimes R (R ⧸ I) = {I.radical}