Associated primes of a module #
We provide the definition and related lemmas about associated primes of modules.
Main definition #
IsAssociatedPrime I Mif the prime ideal
Iis 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.radicalis the only associated prime of
R ⧸ Iwhen
Generalize this to a non-commutative setting once there are annihilator for non-commutative rings.