Assocaited primes of localized module

This file mainly proof the relation between Ass(S⁻¹M) and Ass(M)

Main Results

• associatedPrimes.mem_associatePrimes_of_comap_mem_associatePrimes_isLocalizedModule : for an R module M, if p is a prime ideal of S⁻¹R and p ∩ R ∈ Ass(M) then p ∈ Ass (S⁻¹M).

TODO: prove the reverse when p is finitely generated and get Ass (S⁻¹M) = Ass(M) ∩ Spec(S⁻¹R) when R noetherian.

TODO: deduce from the above that every minimal element in support is in Ass(M).

theorem Module.associatedPrimes.mem_associatePrimes_of_comap_mem_associatePrimes_isLocalizedModule {R : Type u_1} [CommRing R] (S : Submonoid R) (R' : Type u_2) [CommRing R'] [Algebra R R'] [IsLocalization S R'] {M : Type u_3} {M' : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] [Module R' M'] [IsScalarTower R R' M'] (p : Ideal R') [p.IsPrime] (ass : Ideal.comap (algebraMap R R') p ∈ associatedPrimes R M) : p ∈ associatedPrimes R' M'

theorem Module.associatedPrimes.mem_associatePrimes_localizedModule_atPrime_of_mem_associated_primes {R : Type u_1} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] {p : Ideal R} [p.IsPrime] (ass : p ∈ associatedPrimes R M) : IsLocalRing.maximalIdeal (Localization.AtPrime p) ∈ associatedPrimes (Localization.AtPrime p) (LocalizedModule p.primeCompl M)