The Zariski Topology is compact

[tirix]

This adds proofs in 4 independent, but related directions:

• the Zariski topology is compact (~zarcmp)
• the preimage of a prime ideal by a ring homomorphism is a prime ideal (~rhmpreimaprmidl)
• the property of being a prime element in a ring (~isrprm)
• the zero ideal is a prime ideal if and only in an integral domain (~prmidl0)

I'm also adding some references to Grothendieck's Éléments de Géométrie Algébrique where relevant.
The next step would be to prove that the induced map on prime spectra is continuous.

[avekens]

Very interesting results!
Would it be useful to have a definition for zero/trivial rings (maybe ZRing = { r e. Ring | ( # ` ( Base ` r ) ) = 1 })?

[avekens]

PS: ZRing is already existing, maybe 0Ring then...

[tirix]

Would it be useful to have a definition for zero/trivial rings (maybe 0Ring = { r e. Ring | ( # ` ( Base ` r ) ) = 1 })?

That would be a useful discussion to launch!

For zero rings, I've followed theorems in the main part: ~0ring, ~0ring01eq, ~0ringnnzr, which are all in the form ( ( R e. Ring /\ ( # ` B ) = 1 ) -> ...

If I were to choose a "class of zero rings", I'd say ( Ring \ NzRing ) is the best, because it is concise and does not need introducing a new definition. You actually have a few theorems with this form in your mathbox (~0ringdif and following)