isOpen_of_stableUnderGeneralization_of_isConstructible

English

The spectrum of a ring is order-isomorphic to the set of prime ideals. More precisely, there is an order isomorphism between PrimeSpectrum R and { I ⟂ I.IsPrime } given by p ↦ (p.asIdeal, p.isPrime).

Русский

Спектр кольца упорядочен эквивариантно с множеством простых идеалов; существует отображение, сохраняющее порядок, между PrimeSpectrum R и подпростым{I | I.IsPrime}.

LaTeX

$$$\text{PrimeSpectrum}(R) \cong_o { I : \mathrm{Ideal}(R) \mid I. IsPrime }$$$

Lean4

@[stacks 00I0 "(1)"]
theorem isOpen_of_stableUnderGeneralization_of_isConstructible {R : Type*} [CommRing R] {s : Set (PrimeSpectrum R)}
    (hs : StableUnderGeneralization s) (hs' : IsConstructible s) : IsOpen s :=
  by
  rw [← isClosed_compl_iff]
  exact isClosed_of_stableUnderSpecialization_of_isConstructible hs.compl hs'.compl

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