Theorems · Theorem · commutative algebra

IsLocalization.isPrime_iff_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] (J : Ideal S),
  J.IsPrime ↔ (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J)

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 comap, see le_rel_iso_of_prime for the more general relation isomorphism

Defined in

Mathlib.RingTheory.Localization.Ideal

Cited by

6 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebraIsLocalization