Refactoring ring spectra

Stream: maths

[David Ang]

Currently we have four flavours of spectra of rings (hopefully I have not missed any):

• prime_spectrum for prime ideals of any commutative ring,
• projective_spectrum for homogeneous prime ideals of a graded ring avoiding the irrelevant ideal,
• height_one_spectrum for height one prime ideals of a Dedekind domain, and
• maximal_spectrum for maximal ideals of any commutative ring in a new PR

The first two are currently defined as a def with information encoded by subtyping, and the last two are currently defined as a structure with information encoded in fields (as suggested by @Eric Wieser). If possible, I would like to refactor them to look the same, but I'm not sure which approach is preferable to people working with these things, so I'm requesting for opinions. I also think the files containing their definitions and e.g. topological properties are currently in awkward locations, so I would also like to relocate them with permission.

[Johan Commelin]

Sounds good! I think working with a structure is probably a good idea.

[Andrew Yang]

Where are you planning to move them? Somewhere under ring_theory I suppose?

[David Ang]

I don't have a plan yet, but I guess they will be under ring_theory. I think everything under the prime_spectrum folder should be in one file called prime_spectrum.lean somewhere in ring_theory, and similarly with maximal_spectrum.lean, while height_one_spectrum should be its own file height_one_spectrum.lean in ring_theory/dedekind_domain. I don't know what to do with projective_spectrum but I'm guessing the topological properties can be in a file projective_spectrum.lean while the structure sheaf and projective schemes can remain in algebraic_geometry. It's hard to separate algebra with algebraic geometry but the definitions should at least be at a unified location.

[David Ang]

Wild idea but maybe we can have a folder ring_theory/spectrum instead, and put all four files in the same place?