Priestley spaces

Stream: condensed mathematics

[Yaël Dillies]

I'm reading about Priestley spaces from Priestley's book and thought it would be moderately easy to formalize Birkhoff's representation theorem and fun to try Priestley's generalization to her spaces. But then I read there was a isomorphism of category between Priestley spaces and pairwise Stone spaces, and spectral spaces?!? So I went down a wikipedia rabbit hole and I found myself reading about profinite sets and condensed mathematics.
So two questions:

• Have you people taken over all of mathematics? :scream:
• How much can I reuse from LTE for my above purpose?

[Yaël Dillies]

My goal was to give @Sara Rousta a nice and easy first project. I think I'm failing :sweat_smile:

[Kevin Buzzard]

There's always the low-hanging fruit in the undergraduate list. IIRC I recently noticed that we'd proved schemes were sober. Do we know yet that they're spectral?

[Yaël Dillies]

Oh no, are you telling me I just mudded a foot into scheme theory?

[Riccardo Brasca]

Spectral space are morally unrelated to schemes.. (well, I know...)

[Johan Commelin]

What's in a name?

[Junyan Xu]

Not all schemes are spectral, since not all are (quasi-)compact. Interestingly, every open subspace of a spectral space is the underlying space of a scheme. Sobriety of schemes was PR'd into mathlib last month by @Andrew Yang and I don't find any follow-up PRs, and it seems the definition of spectral spaces and equivalent characterizations aren't yet in mathlib; we should show that prime spectra are spectral once it's defined. And IMO the proof that schemes are quasi-sober and T0 should be split into proofs that prime spectra are quasi-sober and T0, and that quasi-sobriety and T0-ness are local properties. We currently lack a definition of "local predicates" on topological spaces, though we have theorems like quasi_sober_of_open_cover; locally (path) connectedness (are they defined in mathlib?) and semi-locally-simply-connectedness (setup for covering space theory) are also examples but spectrality is not.

[Adam Topaz]

There is a nice example in Liu's book of a scheme with no closed point (hence is not spectral). (Of course it is not quasi compact.)

[Andrew Yang]

The sobriety and T0-ness of the prime spectrum are indeed proved separately and used in the proofs of schemes.

I’m not planning to add results about spectral spaces though. If someone wants to add them, feel free to go for them.

We should have most the ingredients to show that prime spectrums are spectral. The only thing missing is probably open quasicompact iff ideal f.g. (or do we have it already?)

[Yaël Dillies]

Where is the definition of spectral spaces?

[Adam Topaz]

Homeo to spec of a ring

[Andrew Yang]

If you are asking about mathlib, then there is not one AFAIR

[Adam Topaz]

This is the canonical reference

https://stacks.math.columbia.edu/bibliography/Hochster-thesis

[Junyan Xu]

https://en.wikipedia.org/wiki/Spectral_space
Well any infinite disjoint union of nonempty schemes wouldn't be quasi compact ...
By the way, if anyone is into Zariski topology of prime spectrum, this thread should be fun to formalize: https://twitter.com/plain_simon/status/1470335009525485568

There is even a formula for T, suggested by 6): T(R)=R[X_r,r\in R]/(r^2*X_r-r,X_r^2*r-X_r) The canonical map R-->T(R) identifies Spec(R) and Spec(T(R)) as sets but turns the Zariski topology into the constructible topology and residue fields into local rings.

- Simon Pepin Lehalleur (@plain_simon)

[Yaël Dillies]

Andrew Yang said:

If you are asking about mathlib, then there is not one AFAIR

Ah okay! I assumed "spectral" meant it already was there somewhere.

[Adam Topaz]

I like the example in Liu, because it's an open subset of an affine scheme ;)

[Adam Topaz]

And it involves valuation rings

[Junyan Xu]

mathlib has a directory for counterexamples but there are currently only 6 files in it.
By the MO answer, every scheme is homeomorphic to an open subspace of an affine scheme, but indeed may not be isomorphic to an open subscheme.

[Reid Barton]

There's a recent book on spectral spaces that is pretty good

[Reid Barton]

https://www.cambridge.org/core/books/spectral-spaces/9ACC409F3885FA808C8AF53B0381C9C7

[Adam Topaz]

Oh looks nice! I'll have to check it out.

[Junyan Xu]

Andrew Yang said:

The sobriety and T0-ness of the prime spectrum are indeed proved separately and used in the proofs of schemes.

Oh yes indeed they are in docs#prime_spectrum.t0_space, I read the proofs too carelessly; I didn't see prime_spectrum.t0_space in the proof but that's probably because it's an inferred instance.

[Junyan Xu]

The two proofs in algebraic_geometry.properties look too dissimilar and introducing local predicates will definitely help to unify them.

[Peter Scholze]

I love spectral spaces! Writing etale cohomology of diamonds was to a large extent an exercise in the point-set topology of spectral spaces ;-). (Also the referee noted that they were struggling the hardest with the proofs in point-set topology...)

If you really want to go down a rabbit hole, read up about Lurie's take on Makkai's conceptual completeness theorem https://www.math.ias.edu/~lurie/278x.html . Makkai's conceptual completeness theorem is a strengthening of Gödel's completeness theorem, and says that in some appropriate sense, a first order theory [the "syntax"] is determined by its models (with enough extra structure) [the "semantics"]. I gather it's in this way also some very souped up version of Birkhoff's representability theorem. In his course, Lurie uses ideas surrounding the pro-etale site etc, and then shows that there's a fully faithful functor from "first order logic" (appropriately made into a category) [the "syntax" side] to condensed categories [the "semantics" side]. (In one direction: To any first order theory $T$, you can look at all the models of $T$, and these are most naturally organized into a condensed category (Lurie uses a slightly different language of ultracategories, but that's just cosmetical). Yes, we are taking over all of mathematics ;-) :octopus: )

[Peter Scholze]

(I should say that Barwick-Glasman-Haine's work on Exodromy https://arxiv.org/abs/1807.03281 is also very much in this spirit; for them, this is really what inspired the pyknotic/condensed formalism.)

[Yaël Dillies]

Well, see you in a month, when I am done digesting the mountain of infos you just buried me under :rofl:

[Yaël Dillies]

I'm defining the categories on the order side of the story in #11677. Hopefully, I can give a stab at the ones on the topological side once they have sunk more in my category newbie brain.

[Yaël Dillies]

@Sara Rousta and I just wrote a first draft of pairwise Stone spaces over at branch#bitopology. Modulo some sorried instances, we have the forgetful functor Profinite ⥤ BiStone. However, I don't really understand the (bi)zero dimensionality condition.
Profinite is compact + Hausdorff + totally disconnected while BiStone is bicompact + bi-Hausdorff + bi-zero dimensional. Why is the last condition different? Or are they actually the same, somehow?

[Johan Commelin]

Never heard of bi-Stone spaces. What is that bi-zero dimensionality condition?

(https://github.com/leanprover-community/mathlib/compare/bitopology#diff-a5e9b829bdd32836ab137bed938198333e917b23d065e0c9fa7e15cdf7beb6c2R65-R66 isn't telling me the answer :stuck_out_tongue_wink:)

[Yaël Dillies]

Yeah I'm sorry! I'm still trying to figure out the correct mathlib-like formulation: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Bicompactness
Here's the Wikipedia definition: https://en.wikipedia.org/wiki/Bitopological_space

[Johan Commelin]

@Yaël Dillies This seems relevant: https://math.stackexchange.com/questions/142070/totally-disconnected-implies-base-of-closed-sets
Tl;dr: they are not equivalent, but if you add compact Hausdorff it should be fine.

[Yaël Dillies]

Oooh, interesting. What about their bi counterparts?

[Johan Commelin]

Je ne sais pas.

[Yaël Dillies]

A month later, as promised: #12228