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 = (Ideal.IsPrime I ∧ ∃ (x : M), I = Submodule.annihilator (Submodule.span R {x}))

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) : Ideal.IsPrime I

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.annihilator (Submodule.span R {x}) ≤ 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] : Set.Nonempty (associatedPrimes R M)

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) : Submodule.annihilator ⊤ ≤ I

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

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