Theorems · Theorem · commutative algebra

IsLocalization.isPrime_of_isPrime_disjoint

∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] (I : Ideal R),
  I.IsPrime → Disjoint ↑M ↑I → (Ideal.map (algebraMap R S) I).IsPrime

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

Defined in

Mathlib.RingTheory.Localization.Ideal

Cited by

13 results in Mathlib

Foundations

Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringCommSemiringAlgebraIsLocalization