English
Let r be an element of R and J an ideal of R. If for every maximal ideal P ∈ R the image of r in the localization at P lies in the localized image of J, then r ∈ J.
Русский
Пусть r ∈ R и J — идеал R. Если при локализации в каждом максимальном идеале P образ r принадлежит локализованному образу J, то r ∈ J.
LaTeX
$$$\\forall r\\in R\\,\\forall J\\subseteq R\\Big(\\forall P\\ (P\\text{ maximal}),\\; \\mathrm{algebraMap}_{R}^{\\mathrm{Localization.AtPrime}(P)}(r) \\in \\mathrm{Ideal.map}(\\mathrm{algebraMap}_{R}^{\\mathrm{Localization.AtPrime}(P)})\,J\\Big) \\Rightarrow r \\in J$$
Lean4
theorem mem_of_localization_maximal {r : R} {J : Ideal R}
(h : ∀ (P : Ideal R) (_ : P.IsMaximal), algebraMap R _ r ∈ Ideal.map (algebraMap R (Localization.AtPrime P)) J) :
r ∈ J :=
Submodule.mem_of_localization_maximal _ _ _ _ fun P hP ↦ by
apply (localized'_eq_map (Localization.AtPrime P) P.primeCompl J).symm ▸ h P hP
