Closed tirix closed 3 months ago
PS: ZRing
is already existing, maybe 0Ring
then...
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)
This adds proofs in 4 independent, but related directions:
~zarcmp
)~rhmpreimaprmidl
)~isrprm
)~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.