English
There is an order-preserving bijection between the prime spectrum of S and the subset of the prime spectrum of R consisting of primes disjoint from M.
Русский
Существует биекция, сохраняющая порядок, между спектром простых примеров S и подмножеством спектра простых R, состоящих из простых, дисjoint с M.
LaTeX
$$$\\text{primeSpectrumOrderIso}(M,S):\\ \\text{PrimeSpectrum}(S) \\simeq_o \\{ p:\\text{PrimeSpectrum}(R) \\mid \\operatorname{Disjoint}(M:\\mathrm{Set}R)(p.asIdeal)\\}$$$
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` -/
@[simps]
def orderIsoOfPrime : { p : Ideal S // p.IsPrime } ≃o { p : Ideal R // p.IsPrime ∧ Disjoint (M : Set R) ↑p }
where
toFun p := ⟨Ideal.comap (algebraMap R S) p.1, (isPrime_iff_isPrime_disjoint M S p.1).1 p.2⟩
invFun p := ⟨Ideal.map (algebraMap R S) p.1, isPrime_of_isPrime_disjoint M S p.1 p.2.1 p.2.2⟩
left_inv J := Subtype.eq (map_comap M S J)
right_inv I := Subtype.eq (comap_map_of_isPrime_disjoint M S I.1 I.2.1 I.2.2)
map_rel_iff'
{I I'} := by
constructor
· exact fun h => show I.val ≤ I'.val from map_comap M S I.val ▸ map_comap M S I'.val ▸ Ideal.map_mono h
exact fun h x hx => h hx
