The prime spectrum of a jacobson ring

Main results

• PrimeSpectrum.exists_isClosed_singleton_of_isJacobson: The spectrum of a jacobson ring is a jacobson space.
• PrimeSpectrum.isOpen_singleton_tfae_of_isNoetherian_of_isJacobson: If R is both noetherian and jacobson, then the following are equivalent for x : Spec R:
  1. {x} is open (i.e. x is an isolated point)
  2. {x} is clopen
  3. {x} is both closed and stable under generalization (i.e. x is both a minimal prime and a maximal ideal)

theorem PrimeSpectrum.exists_isClosed_singleton_of_isJacobsonRing {R : Type u_1} [CommRing R] [IsJacobsonRing R] (s : Set (PrimeSpectrum R)) (hs : IsOpen s) (hs' : s.Nonempty) : ∃ x ∈ s, IsClosed {x}

instance PrimeSpectrum.instJacobsonSpaceOfIsJacobsonRing {R : Type u_1} [CommRing R] [IsJacobsonRing R] : JacobsonSpace (PrimeSpectrum R)

theorem PrimeSpectrum.isJacobsonRing_iff_jacobsonSpace {R : Type u_1} [CommRing R] : IsJacobsonRing R ↔ JacobsonSpace (PrimeSpectrum R)

theorem PrimeSpectrum.isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRing {R : Type u_1} [CommRing R] [IsNoetherianRing R] [IsJacobsonRing R] (x : PrimeSpectrum R) : [IsOpen {x}, IsClopen {x}, IsClosed {x} ∧ StableUnderGeneralization {x}].TFAE

If R is both noetherian and jacobson, then the following are equivalent for x : Spec R:

1. {x} is open (i.e. x is an isolated point)
2. {x} is clopen
3. {x} is both closed and stable under generalization (i.e. x is both a minimal prime and a maximal ideal)