pi-base
Add theorems for spectral spaces and introduce Stone spaces
This PR introduces the notion of a Stone space, which implies that a space is spectral (P75). Along with a theorem that finite Sober spaces are spectral, this establishes the first positive values for the spectral property in the database. Additionally, values for the Stone space property are automatically deduced for every space.
I also changed the name "spectral space" to simply "spectral", as it is used as an adjective independently (e.g. Wikipedia states "X is said to be spectral if it satisfies all of the following conditions"). Stone, by comparison, is a proper name, and doesn't appear to be used as an adjective in the same way.
Coincidentally, this happens to resolve #743.
P193 (Stone space): It is a little hard to see on the web page that there are three properties involved in the definition. Also, the more usual order of properties seems to be "compact Hausdorff totally disconnected" (see for example https://encyclopediaofmath.org/index.php?title=Stone_space or https://ncatlab.org/nlab/show/Stone+space). How about something like: "A space that is {compact}, {T2} and {totally disconnected}".
We should also mention it's equivalent to [compact + totally separated] and to [compact + T0 + zero dimensional].
T532 and T533]? If we can be replaced by the single theorem [Stone ==> totally separated].
T529: even if the equivalent [compact + totally separated ==> Stone] woud be shorter, I think I still prefer the version you have. Can you reorder the properties in the order [compact + T2 + totally disconnected] ?
P75 (Spectral) What good sources would you recommend to study spectral spaces, and the Stone representation theorem for Boolean algebras?
The definition for spectral is phrased in purely topological term. But in T531 the explanation for the space being spectral mentions the spectrum of a Boolean algebra, which a priori seems unrelated. So the page for P75 should mention the equivalent characterization as being homeomorphic to the spectrum of a commutative ring. And should give the definition of what that spectrum and its topology are.
T532 and T533 can be replaced by the single theorem [Stone ==> totally separated].
While working on the PR, I had previously used Stone space ⇒ Zero dimensional, but when I went to type up the reasoning I realized it was equivalent to giving the two separate theorems thanks to T269. I can change it to implying one of zero dimensional or totally separated though.
What good sources would you recommend to study spectral spaces, and the Stone representation theorem for Boolean algebras? The definition for spectral is phrased in purely topological term. But in T531 the explanation for the space being spectral mentions the spectrum of a Boolean algebra, which a priori seems unrelated. So the page for P75 should mention the equivalent characterization as being homeomorphic to the spectrum of a commutative ring. And should give the definition of what that spectrum and its topology are.
I did realize after submitting my PR that that theorem was quite handwavy, but frustratingly Lemma 5.23.8 at the Stacks Project, which I referenced elsewhere, was worded in such a way that it's not clear that Stone/profinite spaces are spectral, and there's no mention of spectral on their page on profinite spaces. It's given in Theorem 4.2 of the book Stone Spaces by Peter Johnstone though. That proof is purely topological, so mentioning spectra of rings isn't strictly necessary, but it would probably be nice to give further justifications/explanations of the properties and a deeper sense of how they relate. (If you do want to read about Stone's representation theorem for Boolean algebras, it's listed as a corollary of Proposition 4.4 a couple pages later. There's okay coverage of the topic on Wikipedia and nLab as well; c.f. nLab's table of contents for the book. The book Spectral Spaces also looks good from the table of contents, but I can't access it through my university.)
T532 and T533 can be replaced by the single theorem [Stone ==> totally separated].
While working on the PR, I had previously used Stone space ⇒ Zero dimensional, but when I went to type up the reasoning I realized it was equivalent to giving the two separate theorems thanks to T269. I can change it to implying one of zero dimensional or totally separated though.
We want to express that a Stone space is both T2 and totally disconnected. And totally separated by itself already implies both T2 and totally disconnected. Zero dimensional by itself does not imply T2, nor does totally disconnected. So it seems simpler to just have [Stone ==> totally separated] for the purpose of having a smaller set of theorems.
(Note: it's true that we could use Stone ==> spectral ==> sober ==> T0. And that in combination with zero dim is good enough to imply everything else. But it seems more straightforward to have [Stone ==> totally separated].)
Thanks for the extra info on spectral spaces. It seems that Johnstone is a good resource. If we could quote a specific result or section from that book giving the formulation of spectral spaces in terms of the spectrum of a commutative ring, that would be very helpful.
Actually, doesn't Theorem 4.2 in Johnstone's book prove exactly your T531 in purely topological terms without referring to the spectrum of a commutative ring?
I did say as much in my comment above, yes.
Right, I thought you meant to also add something about the spectrum of commutative rings in T531. I initially thought there was no need to. But maybe it could be useful after all.
But like you said to give a deeper sense of these properties, the definition page for P75 can also mention something about spectra of commutative rings and how they relate, with references, etc.
After finding a copy of the aforementioned book Spectral Spaces and getting a better idea of how Stone duality works, I did my best to write something brief, comprehensible, and meaningful about Stone duality and spectra of rings. I believe all of your suggestions have been implemented as well.
Nice overview.
For T528 [sober + finite ==> spectral], we already have T513 [finite ==> quasi-sober] So T528 can be be given a stronger and easier form [finite + T0 ==> spectral].
I have some more comments about this PR. But in the mean time, can you review #768? It's related to the current topic.
- For Stone space (P193), I want to suggest to present the equivalent formulation for the definition as a list similar to what's done for example for R0 (https://topology.pi-base.org/properties/P000135): "Any of the following equivalent properties hold: ...", but only for the three formulation involving Compact, not for Spectral+T1. No need for justification, as the equivalences follow from what's already known in pi-base (any interested user can get at it by plugging things in the search box in the usual way).
But we can also note in a separate paragraph after the list (not as part of the formal definition) that a space is Stone space iff it is spectral and T1.
-
For T530 [Spectral + T1 ==> Stone] the proofs in the references are confusingly intertwined with commutative algebra results. A direct topological proof is actually pretty straightforward. The tricky part is to show that spectral T1 spaces are Hausdorff. For that we can refer to the argument for the Corollary at the end of https://math.stackexchange.com/a/109174 (reading $X$ for Spec A). Once we have that, we can give a direct argument, using that fact that in a compact Hausdorff space the compact open subsets are exactly the clopen subsets.
-
Spectral space (P75): "... its prime ideals": the "its" refers to the lattice and not the spectral space, I suppose. Can we phrase it as "... whose points are the prime ideals of the lattice"? Also use the more usual plural "spectra" in this context.
Let me know if you'd like me to give a shot to the above.
I feel satisfied with the pull request as it stands, but if there are any changes you would like to make, feel free to add them.
For T530 [Spectral + T1 ==> Stone space], I realized I overlooked something crucial. We want a purely topological proof, not involving notions of ring theory. I thought the corollary at the end of https://math.stackexchange.com/a/109174 did the job to show the space is T2. Namely, we have a family of compact open sets with the finite intersection property. So by compactness their intersection must be nonempty. But that does not work because we don't know a priori that the compact opens are also closed.
So it seems we cannot avoid making use of the patch topology (= constructible topology). I changed things to just refer to Lemma 5.23.8 of the Stacks project, which requires quite a bit of preliminaries, but at least it's all detailed in there. Maybe you can find a better reference to add?
Two more minor things:
- P75 (spectral): the reference to Arhangel'skii really does not do much. It's just two two small paragraphs without much of an explanation. Since the other sources have better coverage, I think we should remove that one.
- T531: What is the reference to Boolean ring for?
Comments?
Those references were legacies from previous versions that aren't useful anymore, so I just removed them. I can't recall having come across a better source to reference for T530, since a lot of them don't seem to mention that T1 is sufficient and just give the Hausdorff condition. I can take another look, but I wouldn't expect to find another one as good that's also freely accessible on the web.