Prime ideal correspondence for localization (source code)

= Prime ideal correspondence for localization
{wiki=Localization_(commutative_algebra)#Properties}

Extension and contraction give inverse inclusion-preserving bijections between prime ideals of $S^{-1}R$ and prime ideals of $R$ disjoint from $S$:
$$
\mathfrak p\longmapsto S^{-1}\mathfrak p,
\qquad
\mathfrak q\longmapsto\iota^{-1}(\mathfrak q).
$$