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

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

The set of associated primes of a module.

Equations
• = {I : | }
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 : ) :
I.IsPrime
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 : ), (Submodule.span R {x}).annihilator 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] [] [] :
().Nonempty
theorem biUnion_associatedPrimes_eq_zero_divisors (R : Type u_1) [] (M : Type u_2) [] [Module R M] [] :
p, p = {r : R | ∃ (x : M), x 0 r x = 0}
theorem IsAssociatedPrime.annihilator_le {R : Type u_1} [] {I : } {M : Type u_2} [] [Module R M] (h : ) :
.annihilator I
theorem IsAssociatedPrime.eq_radical {R : Type u_1} [] {I : } {J : } (hI : I.IsPrimary) (h : IsAssociatedPrime J (R I)) :