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} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : Prop

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

Equations

• IsAssociatedPrime I M = (I.IsPrime ∧ ∃ (x : M), I = (Submodule.span R {x}).annihilator)

def associatedPrimes (R : Type u_1) [CommRing R] (M : Type u_2) [AddCommGroup 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 AssociatePrimes.mem_iff {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_2} [AddCommGroup M] [Module R M] : I ∈ associatedPrimes R M ↔ IsAssociatedPrime I M

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

theorem IsAssociatedPrime.map_of_injective {R : Type u_1} [CommRing R] {I : Ideal R} {M : Type u_2} [AddCommGroup M] [Module R M] {M' : Type u_3} [AddCommGroup 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} [CommRing R] {I : Ideal R} {M : Type u_2} [AddCommGroup M] [Module R M] {M' : Type u_3} [AddCommGroup M'] [Module R M'] (l : M ≃ₗ[R] M') : IsAssociatedPrime I M ↔ IsAssociatedPrime I M'

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

theorem exists_le_isAssociatedPrime_of_isNoetherianRing (R : Type u_1) [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [H : IsNoetherianRing R] (x : M) (hx : x ≠ 0) : ∃ (P : Ideal R), IsAssociatedPrime P M ∧ (Submodule.span R {x}).annihilator ≤ P

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

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

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

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

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

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

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}