English
If p ∈ Ass_R(M), then the maximal ideal of the localization at p belongs to Ass_{R_p}(M_p).
Русский
Если p ∈ Ass_R(M), то максимальная идеал локализации AtPrime p принадлежит Ass_{R_p}(LocalizedModule p).
LaTeX
$$$\\mathfrak{m}_{R_p} \\in \\operatorname{Ass}_{R_p}(M_p)$, where $R_p$ is the localization at $p$ and $M_p$ is the localized module.$$
Lean4
theorem mem_associatePrimes_of_comap_mem_associatePrimes_isLocalizedModule (p : Ideal R') [p.IsPrime]
(ass : p.comap (algebraMap R R') ∈ associatedPrimes R M) : p ∈ associatedPrimes R' M' :=
by
rcases ass with ⟨hp, x, hx⟩
constructor
· /- use the following to remove `p.IsPrime`
exact (IsLocalization.isPrime_iff_isPrime_disjoint S _ _).mpr
⟨hp, (IsLocalization.disjoint_comap_iff S R' p).mpr (p ≠ ⊤)⟩ -/
assumption
· use f x
ext t
rcases IsLocalization.mk'_surjective S t with ⟨r, s, hrs⟩
rw [← IsLocalizedModule.mk'_one S, ← hrs, mem_ker, toSpanSingleton_apply, IsLocalizedModule.mk'_smul_mk', mul_one,
IsLocalizedModule.mk'_eq_zero']
refine ⟨fun h ↦ ?_, fun ⟨t, ht⟩ ↦ ?_⟩
· use 1
simp only [← toSpanSingleton_apply, one_smul, ← mem_ker, ← hx, Ideal.mem_comap]
have : (algebraMap R R') r = IsLocalization.mk' R' r s * IsLocalization.mk' R' s.1 (1 : S) :=
by
rw [← IsLocalization.mk'_one (M := S) R', ← sub_eq_zero, ← IsLocalization.mk'_mul, ← IsLocalization.mk'_sub]
simp
rw [this]
exact Ideal.IsTwoSided.mul_mem_of_left _ h
· have : t • r • x = (t.1 * r) • x := smul_smul t.1 r x
rw [this, ← LinearMap.toSpanSingleton_apply, ← LinearMap.mem_ker, ← hx, Ideal.mem_comap, ←
IsLocalization.mk'_one (M := S) R'] at ht
have : IsLocalization.mk' R' r s = IsLocalization.mk' (M := S) R' (t.1 * r) 1 * IsLocalization.mk' R' 1 (t * s) :=
by
rw [← IsLocalization.mk'_mul, mul_one, one_mul, ← sub_eq_zero, ← IsLocalization.mk'_sub, Submonoid.coe_mul]
simp [← mul_assoc, mul_comm r t.1, IsLocalization.mk'_zero]
simpa [this] using Ideal.IsTwoSided.mul_mem_of_left _ ht
