Associated primes of localized module

This file mainly proves 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).

theorem Module.associatedPrimes.mem_associatedPrimes_of_comap_mem_associatedPrimes_of_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') (ass : Ideal.comap (algebraMap R R') p ∈ associatedPrimes R M) : p ∈ associatedPrimes R' M'

Stacks Tag 0310 ((1))

theorem Module.associatedPrimes.mem_associatedPrimes_atPrime_of_mem_associatedPrimes {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.AtPrime p M)

@[deprecated Module.associatedPrimes.mem_associatedPrimes_atPrime_of_mem_associatedPrimes (since := "2025-11-27")]

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.AtPrime p M)

Alias of Module.associatedPrimes.mem_associatedPrimes_atPrime_of_mem_associatedPrimes.

theorem Module.associatedPrimes.comap_mem_associatedPrimes_of_mem_associatedPrimes_of_isLocalizedModule_of_fg {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') (ass : p ∈ associatedPrimes R' M') (fg : (Ideal.comap (algebraMap R R') p).FG) : Ideal.comap (algebraMap R R') p ∈ associatedPrimes R M

Stacks Tag 0310 ((2))

theorem Module.associatedPrimes.preimage_comap_associatedPrimes_eq_associatedPrimes_of_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'] [IsNoetherianRing R] : Ideal.comap (algebraMap R R') ⁻¹' associatedPrimes R M = associatedPrimes R' M'

Stacks Tag 0310 ((3))

theorem Module.associatedPrimes.minimalPrimes_annihilator_subset_associatedPrimes (R : Type u_1) [CommRing R] (M : Type u_3) [AddCommGroup M] [Module R M] [IsNoetherianRing R] [Module.Finite R M] : (annihilator R M).minimalPrimes ⊆ associatedPrimes R M