Documentation

Mathlib.AlgebraicGeometry.PrimeSpectrum.Jacobson

The prime spectrum of a jacobson ring #

Main results #

theorem PrimeSpectrum.exists_isClosed_singleton_of_isJacobson {R : Type u_1} [CommRing R] [Ideal.IsJacobson R] (s : Set (PrimeSpectrum R)) (hs : IsOpen s) (hs' : s.Nonempty) :
xs, IsClosed {x}

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)