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

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

def associatedPrimes (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] : Set (Ideal R)

The set of associated primes of a module.

theorem AssociatePrimes.mem_iff {R : Type u_1} [CommSemiring R] {I : Ideal R} {M : Type u_2} [AddCommMonoid M] [Module R M] : I ∈ associatedPrimes R M ↔ IsAssociatedPrime I M

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

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

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

theorem exists_le_isAssociatedPrime_of_isNoetherianRing (R : Type u_1) [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] [H : IsNoetherianRing R] (x : M) (hx : x ≠ 0) : ∃ (P : Ideal R), IsAssociatedPrime P M ∧ ⊥.colon {x} ≤ P

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

If M → M' is injective, then the set of associated primes of M is contained in that of M'.

theorem associatedPrimes.subset_union_of_exact {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {M' : Type u_3} [AddCommMonoid M'] [Module R M'] {f : M →ₗ[R] M'} {M'' : Type u_4} [AddCommMonoid M''] [Module R M''] {g : M' →ₗ[R] M''} (hf : Function.Injective ⇑f) (hfg : Function.Exact ⇑f ⇑g) : associatedPrimes R M' ⊆ associatedPrimes R M ∪ associatedPrimes R M''

If 0 → M → M' → M'' is an exact sequence, then the set of associated primes of M' is contained in the union of those of M and M''.

theorem associatedPrimes.prod (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] (M' : Type u_3) [AddCommMonoid M'] [Module R M'] : associatedPrimes R (M × M') = associatedPrimes R M ∪ associatedPrimes R M'

The set of associated primes of the product of two modules is equal to the union of those of the two modules.

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

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

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

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

theorem biUnion_associatedPrimes_eq_compl_nonZeroDivisors (R : Type u_1) [CommSemiring R] [IsNoetherianRing R] : ⋃ p ∈ associatedPrimes R R, ↑p = (↑(nonZeroDivisors R))ᶜ

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

theorem isAssociatedPrime_iff_exists_injective_linearMap {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] : IsAssociatedPrime I M ↔ I.IsPrime ∧ ∃ (f : R ⧸ I →ₗ[R] M), Function.Injective ⇑f

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}