# Documentation

Mathlib.RingTheory.Ideal.AssociatedPrime

# 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 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.

## Todo #

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

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

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

Instances For
def associatedPrimes (R : Type u_1) [] (M : Type u_2) [] [Module R M] :
Set ()

The set of associated primes of a module.

Instances For
theorem AssociatePrimes.mem_iff {R : Type u_1} [] {I : } {M : Type u_2} [] [Module R M] :
I
theorem IsAssociatedPrime.isPrime {R : Type u_1} [] {I : } {M : Type u_2} [] [Module R M] (h : ) :
theorem IsAssociatedPrime.map_of_injective {R : Type u_1} [] {I : } {M : Type u_2} [] [Module R M] {M' : Type u_3} [] [Module R M'] (f : M →ₗ[R] M') (h : ) (hf : ) :
theorem LinearEquiv.isAssociatedPrime_iff {R : Type u_1} [] {I : } {M : Type u_2} [] [Module R M] {M' : Type u_3} [] [Module R M'] (l : M ≃ₗ[R] M') :
theorem not_isAssociatedPrime_of_subsingleton {R : Type u_1} [] {I : } {M : Type u_2} [] [Module R M] [] :
theorem exists_le_isAssociatedPrime_of_isNoetherianRing (R : Type u_1) [] {M : Type u_2} [] [Module R M] [H : ] (x : M) (hx : x 0) :
P, P
theorem associatedPrimes.subset_of_injective {R : Type u_1} [] {M : Type u_2} [] [Module R M] {M' : Type u_3} [] [Module R M'] (f : M →ₗ[R] M') (hf : ) :
theorem LinearEquiv.AssociatedPrimes.eq {R : Type u_1} [] {M : Type u_2} [] [Module R M] {M' : Type u_3} [] [Module R M'] (l : M ≃ₗ[R] M') :
=
theorem associatedPrimes.eq_empty_of_subsingleton {R : Type u_1} [] {M : Type u_2} [] [Module R M] [] :
theorem associatedPrimes.nonempty (R : Type u_1) [] (M : Type u_2) [] [Module R M] [] [] :
theorem IsAssociatedPrime.annihilator_le {R : Type u_1} [] {I : } {M : Type u_2} [] [Module R M] (h : ) :
theorem IsAssociatedPrime.eq_radical {R : Type u_1} [] {I : } {J : } (hI : ) (h : IsAssociatedPrime J (R I)) :
theorem associatedPrimes.eq_singleton_of_isPrimary {R : Type u_1} [] {I : } [] (hI : ) :