Maximal spectrum of a ring

Stream: mathlib4

[Michał Staromiejski]

Hi, as my first contribution (:tada:) I'd like to add a definition of the maximal spectrum of a ring. In my local work I defined it just as a set:

def specMax (R : Type*) [Semiring R] : Set (Ideal R) :=
  {I | I.IsMaximal}

but the prime spectrum is already defined in Mathlib4 as a type (https://github.com/leanprover-community/mathlib4/blob/v4.15.0/Mathlib/RingTheory/PrimeSpectrum.lean):

structure PrimeSpectrum [CommSemiring R] where
  asIdeal : Ideal R
  isPrime : asIdeal.IsPrime

Should I follow this for consistency? If so, should I create separate file MaximalSpectrum.lean with the definition under RingTheory/ or maybe better under RingTheory/Ideal/? Or for now just add it to the file RingTheory/Ideal/Maximal.lean?

One negative side of implementing it as the structure is that I use theorems like IsArtinian.equivPi that deals with the set but on the other hand maybe we want to replace occurrences of {I : Ideal R | I.IsMaximal} (the variable R might differ here) by MaximalSpectrum R wherever possible.

Any thoughts?

[Andrew Yang]

docs#MaximalSpectrum already exists I believe. We should probably reduce the imports so that it could be imported into ArtinianRing.lean to refactor that.

[Michał Staromiejski]

Thanks, it seems I need to learn how to search for things :face_palm: I swear I was looking for it but maybe not enough :face_with_peeking_eye:

Do we want to create a subdirectory Spectrum with Maximal.lean, Prime.lean (definitions + simple facts) and somehow organize the rest of the results? I might come up with some suggestions if original authors agree.

Then the next step would be to refactor the rest using the definitions.

[Andrew Yang]

My suggestion would be to create RingTheory/Spectrum/Prime/Defs.lean that contains only the definition of PrimeSpectrum and move file#RingTheory/PrimeSpectrum to /Basic.lean and everything AlgebraicGeometry/PrimeSpectrum/* inside (with Basic renamed to Topology or ZariskiTopology). The same for MaximalSpectrum (to Maximal/Defs and Maximal/Basic).

[Andrew Yang]

Sidenote: I have previously discussed with @Johan Commelin privately on moving PrimeSpectrum out of AG entirely and IIRC our conclusion is to make the line between AG and CA to be the use of sheaf theory or not. Happy to hear other suggestions though.

[Michał Staromiejski]

This sounds reasonable. I can refactor and we can discuss once PR is there.

[Michał Staromiejski]

PR opened: #20772 and new topic started: #PR reviews > #20772 split off definition of ring spectra
the PR contains only splitting off definitions. Moving results from AlgebraicGeometry will follow in a separate PR to keep changes reasonably small.