Zulip Chat Archive

Stream: maths

Topic: Refactoring ring spectra


David Ang (Oct 12 2022 at 10:14):

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 (Oct 12 2022 at 10:18):

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

Andrew Yang (Oct 12 2022 at 11:28):

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

David Ang (Oct 12 2022 at 14:09):

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 (Oct 12 2022 at 14:14):

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


Last updated: Dec 20 2023 at 11:08 UTC