Localizing a prime that survives in a localization

Let S be a localization of R at a submonoid M, and let q be a prime of R disjoint from M. Then q S is a prime of S lying over q, and the localization of R at q is the localization of S at q S. Mathlib records the converse direction, starting from a prime of S, as IsLocalization.isLocalization_isLocalization_atPrime_isLocalization and IsLocalization.localizationLocalizationAtPrimeIsoLocalization.

Main results

• IsLocalization.exists_ringEquiv_localization_atPrime: for a prime q of R disjoint from M, there is a prime P of S lying over q with R_q ≃+* S_P.

theorem IsLocalization.exists_ringEquiv_localization_atPrime {R : Type u_1} [CommSemiring R] (M : Submonoid R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization M S] (q : Ideal R) [q.IsPrime] (hq : Disjoint ↑M ↑q) : ∃ (P : Ideal S) (x : P.IsPrime), Ideal.under R P = q ∧ Nonempty (Localization.AtPrime q ≃+* Localization.AtPrime P)

If S is a localization of R at M and q is a prime of R disjoint from M, then there is a prime P of S lying over q (namely q S) such that R_q is isomorphic to S_P.