English
If p ∈ Ass_R(M), then the comap of p to R' lies in Ass_{R'}(M'), via a localized map, i.e., localization preserves associated primes through comap.
Русский
Если p ∈ Ass_R(M), через локализацию отображение comap сохраняет ассоциированные праймы в локализованном модуле.
LaTeX
$$$ p \\in \\operatorname{Ass}_R(M) \\Rightarrow \\text{(via localization)} \\ p' \\in \\operatorname{Ass}_{R'}(M'). $$$
Lean4
theorem mem_associatePrimes_localizedModule_atPrime_of_mem_associated_primes {p : Ideal R} [p.IsPrime]
(ass : p ∈ associatedPrimes R M) :
maximalIdeal (Localization.AtPrime p) ∈
associatedPrimes (Localization.AtPrime p) (LocalizedModule p.primeCompl M) :=
by
apply
mem_associatePrimes_of_comap_mem_associatePrimes_isLocalizedModule p.primeCompl (Localization.AtPrime p)
(LocalizedModule.mkLinearMap p.primeCompl M)
simpa [Localization.AtPrime.comap_maximalIdeal] using ass
