English
There is an order isomorphism between the prime spectrum of the localization S and the subtype of prime ideals of R disjoint from M.
Русский
Существуют точное порядковое изоморфизм между спектром примитива локализации S и подтипом простых идеалов R, не пересекающихся с M.
LaTeX
$$$\\text{primeSpectrumOrderIso}: \\text{PrimeSpectrum}(S) \\cong_o \\{ p:\\text{PrimeSpectrum}(R) \\mid \\operatorname{Disjoint}(M:\\mathrm{Set}R)(p.asIdeal)\\}$$$
Lean4
/-- The prime spectrum of the localization of a ring at a submonoid `M` are in
order-preserving bijection with subset of the prime spectrum of the ring consisting of
prime ideals disjoint from `M`. -/
@[simps!]
def primeSpectrumOrderIso : PrimeSpectrum S ≃o { p : PrimeSpectrum R // Disjoint (M : Set R) p.asIdeal } :=
(PrimeSpectrum.equivSubtype S).trans <|
(orderIsoOfPrime M S).trans
⟨⟨fun p ↦ ⟨⟨p, p.2.1⟩, p.2.2⟩, fun p ↦ ⟨p.1.1, p.1.2, p.2⟩, fun _ ↦ rfl, fun _ ↦ rfl⟩, .rfl⟩
