Associated primes and localization at a prime

For a module M over a Noetherian ring R and a prime p, this file characterises when the maximal ideal of R_p is an associated prime of M_p.

Main results

• TauCeti.maximalIdeal_mem_associatedPrimes_localizedModule_iff: the maximal ideal of R_p is associated to M_p exactly when p is an associated prime of M.

theorem TauCeti.maximalIdeal_mem_associatedPrimes_localizedModule_iff {R : Type u} [CommRing R] [IsNoetherianRing R] {M : Type v} [AddCommGroup M] [Module R M] {p : Ideal R} [p.IsPrime] : IsLocalRing.maximalIdeal (Localization.AtPrime p) ∈ associatedPrimes (Localization.AtPrime p) (LocalizedModule p.primeCompl M) ↔ p ∈ associatedPrimes R M

For a module M over a Noetherian ring R and a prime p, the maximal ideal of R_p is an associated prime of M_p exactly when p is an associated prime of M. This upgrades Mathlib's Module.associatedPrimes.mem_associatedPrimes_atPrime_of_mem_associatedPrimes to an iff.