Metamath Proof Explorer


Table of Contents - 21.3.14.9. Spectrum of a ring

The prime ideals of a ring can be endowed with the Zariski topology. This is done by defining a function which maps ideals of to closed sets (see for example zarcls0 for the definition of ).

The closed sets of the topology are in the range of (see zartopon).

The correspondence with the open sets is made in zarcls.

As proved in zart0, the Zariski topology is T0 , but generally not T1 .

  1. crspec
  2. df-rspec
  3. rspecval
  4. rspecbas
  5. rspectset
  6. rspectopn
  7. zarcls0
  8. zarcls1
  9. zarclsun
  10. zarclsiin
  11. zarclsint
  12. zarclssn
  13. zarcls
  14. zartopn
  15. zartop
  16. zartopon
  17. zar0ring
  18. zart0
  19. zarmxt1
  20. zarcmplem
  21. zarcmp
  22. rspectps
  23. rhmpreimacnlem
  24. rhmpreimacn