The Zariski topology is a topology

metamath / set.mm

Metamath source file for logic and set theory

Creative Commons Zero v1.0 Universal

238 stars 87 forks source link

The Zariski topology is a topology #4049

Closed tirix closed 1 month ago

tirix commented 1 month ago

Includes proofs for:

the Zariski topology is a topology (~zartop)
the Zariski topology is T0 (~zart0)
the Zariski topology is T1 (~zarmxt1) when restricted to the maximal ideals. Pending:
the Zariski topology is compact.

The whole "spectrum of a ring" section has been moved inside of the "topology" section of my mathbox. I found it to be very interesting and instructive to develop.

avekens commented 1 month ago

Very interesting results, but I am missing some explanations (see inline comments).

tirix commented 1 month ago

Note: this PR is a follow-up to this remark from @savask.