primeSpectrumOrderIso — Mathlib

English

The prime spectrum of the localization S is order-isomorphic to the interval (-∞, I] in the prime spectrum of R.

Русский

Спектр простых идеалов локализации S упорядоченно изоморфен интервалу (-∞, I] в спектре простых идеалов R.

LaTeX

$$$$ \text{primeSpectrumOrderIso} : \text{PrimeSpectrum}(S) \simeq_o \mathbf{Set.Iic}(\langle I, hI\rangle) $$$$

Lean4

/-- The prime spectrum of the localization of a commutative ring R at a prime ideal I are in
order-preserving bijection with the interval (-∞, I] in the prime spectrum of R. -/
@[simps!]
def primeSpectrumOrderIso : PrimeSpectrum S ≃o Set.Iic (⟨I, hI⟩ : PrimeSpectrum R) :=
  (PrimeSpectrum.equivSubtype S).trans <|
    (orderIsoOfPrime S I).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⟩

Похожие утверждения