English
If I is a prime ideal of R disjoint from M, then its image under localization is a prime ideal of S.
Русский
Если I — простой идеал R и Disjoint(M,I), то его образ при локализации есть простой идеал S.
LaTeX
$$$I.IsPrime \\rightarrow Disjoint(M:\\mathrm{Set}R)(I) \\rightarrow (\\operatorname{Ideal.map}(\\mathrm{algebraMap}\\;R\\;S)I).IsPrime$$$
Lean4
/-- If `R` is a ring, then prime ideals in the localization at `M`
correspond to prime ideals in the original ring `R` that are disjoint from `M`.
This lemma gives the particular case for an ideal and its map,
see `le_rel_iso_of_prime` for the more general relation isomorphism, and the reverse implication -/
theorem isPrime_of_isPrime_disjoint (I : Ideal R) (hp : I.IsPrime) (hd : Disjoint (M : Set R) ↑I) :
(Ideal.map (algebraMap R S) I).IsPrime :=
by
rw [isPrime_iff_isPrime_disjoint M S, comap_map_of_isPrime_disjoint M S I hp hd]
exact ⟨hp, hd⟩
