English
If for every maximal P, the localizations of I and J are equal, then I = J.
Русский
Если для каждого максимального P локализации I и J равны, то I = J.
LaTeX
$$$\\forall P\\; (P\\text{ maximal})\\; \\mathrm{Ideal.map}(\\mathrm{algebraMap}_{R}^{\\mathrm{Localization.AtPrime}(P)})\,I = \\mathrm{Ideal.map}(\\mathrm{algebraMap}_{R}^{\\mathrm{Localization.AtPrime}(P)})\,J \\Rightarrow I = J$$
Lean4
/-- Let `I J : Ideal R`. If the localization of `I` at each maximal ideal `P` is equal to
the localization of `J` at `P`, then `I = J`. -/
theorem eq_of_localization_maximal {I J : Ideal R}
(h :
∀ (P : Ideal R) (_ : P.IsMaximal),
Ideal.map (algebraMap R (Localization.AtPrime P)) I = Ideal.map (algebraMap R (Localization.AtPrime P)) J) :
I = J :=
le_antisymm (le_of_localization_maximal fun P hP ↦ (h P hP).le) (le_of_localization_maximal fun P hP ↦ (h P hP).ge)
