Compact opens

Stream: Is there code for X?

[Yaël Dillies]

We have docs#topological_space.opens and docs#topological_space.compacts. Do we have their "intersection", the type of compact opens?

[Kevin Buzzard]

It wouldn't surprise we if we didn't -- I think we only bundled opens because we wanted to think about things more categorically because of schemes etc. People used to real analysis might think compact opens are a strange concept but they come up a lot in the theory of p-adic groups. Do we need to bundle them though? In my mind a lot of the theorems in the theory just say "if K is a compact open subgroup of G then...". We bundled opens so we could talk about sheaves using the category theory language. What would be the benefit here? Do you know why we bundled compacta? Edit: looks like some metric space definition of distance between compacts.

[Yaël Dillies]

I redirect you to the same wikipedia article: The lattice of compact opens is a functor from spectral spaces to distributive lattices, and it can be upgraded to an equivalence of categories.

[Kevin Buzzard]

Oh, that seems like a nice reason! I wonder if the lattices coming from natural locally profinite spaces such as the p-adic numbers have some natural definition on the distributive lattice side.

[Yaël Dillies]

Probably! Maybe we can find it somewhere in this huge article by Olivia Caramello?

[Kevin Buzzard]

I should say that spectral spaces play some role in nonarchimedean geometry so those would be the objects for which an API would find a fan club around here

[Yaël Dillies]

Oh that's nice! I started with Priestley spaces and bitopological spaces because I understand them more, but If you explain me what the definition of spectral spaces should be in mathlib (there are like a lot of equivalent definitions), I could fastforward.

[Kevin Buzzard]

Yes that's an interesting question! My instinct would be to go with the sober definition ie the definition in Wikipedia because we already have sober spaces in mathlib

[Yaël Dillies]

How would you state "$K^\circ(X)$ is closed under finite intersections"?

[Yaël Dillies]

I'm dismissing definitions 1 to 4 already, because they require noncanonical data. However, 5 seems promising too, if I knew what "coherent frame" means.

[Kevin Buzzard]

"intersection of two compact opens is compact open"?

[Kevin Buzzard]

(assuming the background space is compact)

[Yaël Dillies]

Oh okay, I kind of wanted it to be lattice (compact_opens X) but that wouldn't make much sense.

[Reid Barton]

Of the three categories described at https://en.wikipedia.org/wiki/Duality_theory_for_distributive_lattices, the only one I've ever seen anyone use (other than to talk about this duality) is spectral spaces, and they get used a lot.

[Reid Barton]

But that might just be a function of the people I talk to, I suppose.

[Reid Barton]

Yaël Dillies said:

Oh that's nice! I started with Priestley spaces and bitopological spaces because I understand them more, but If you explain me what the definition of spectral spaces should be in mathlib (there are like a lot of equivalent definitions), I could fastforward.

Here is Lurie's definition (https://www.math.ias.edu/~lurie/papers/SAG-rootfile.pdf appendix A.1), which looks the cleanest to me.
image.png

[Reid Barton]

("coherent space" = "spectral space")

[Yaël Dillies]

And do you know what "coherent frame" means?

[Yaël Dillies]

I assume that quasi-compact = compact_space and quasi-separated = separated_space?

[Reid Barton]

http://nlab-pages.s3.us-east-2.amazonaws.com/nlab/show/coherent+space#coherent_locales (substitute "frame" for "locale"), and I assume $a$ is "compact" if whenever $a \le \bigsqcup_{i \in I} b_i$, then already $a \le \bigsqcup_{i \in S} b_i$ for some finite $S \subseteq I$.

[Reid Barton]

Yaël Dillies said:

I assume that quasi-compact = compact_space

Yes

and quasi-separated = separated_space?

No, this separated_space is something about uniform spaces. Quasi-separatedness isn't a property you'd be likely to see in general topology outside this Stone duality/spectral context (because in a "normal" topological space, there are probably very few compact open sets in the first place).

[Reid Barton]

But really it's one condition--the (quasi-)compact opens of $X$ are closed under finite intersections--in the nullary case it says that $X$ is quasi-compact ($X \subset X$ is always open) and then in the binary case it's this quasi-separatedness condition.

[Reid Barton]

IIRC mathlib doesn't currently have a good way to say things like https://github.com/rwbarton/lean-omin/blob/master/src/for_mathlib/closure.lean#L102

[Reid Barton]

(if I'm wrong please let me know!)

[Yaël Dillies]

Do you think it's worth expressing "closed under finitely many operations" as such rather than as the nullary condition + the binary condition? The latter seems simpler to satisfy and more modular (after, compact spaces are a thing!)

[Reid Barton]

You mean in the definition of spectral space I guess

[Reid Barton]

I think in practice, spaces aren't just "accidentally" spectral. You only build spectral spaces in pretty specific ways. So maybe worth thinking about an example like the spectrum of a ring and see what definition fits best to the proof that it is spectral

[Reid Barton]

Ideally something like closed_under_finite_inters in the link above would be in mathlib (hint hint :upside_down:) and then you could check just the 0- and 2-ary cases, and get intersections over finset/fintypes as lemmas for free. Then the definition of spectral space could just include closed_under_finite_inters is_compact_open.

[Damiano Testa]

I had in mind of defining a semiring structure on set α using unions for + and intersections for *. Then if you prove an instance from "compact opens" or whatever definition you want, you have access to the semiring API.

Disclaimer: this may not work, I have not tested it, but is a recurrent thought that I have!

[Kevin Buzzard]

I think this definition has come up before and Mario objected to making it an instance because if you have two subsets A and B of X then people might want A+B to mean something other than the union (eg it could be the sums a+b if X has an addition defined on it)

[Kevin Buzzard]

I guess I talk to different people than Reid and I've only ever seen spectral spaces before out of all of these objects

[Reid Barton]

But instead of the semiring API, you can use the distributive_lattice API which is basically the same thing.

[Reid Barton]

Ideally we would have sub-structures for the order classes (as in https://github.com/rwbarton/lean-omin/blob/master/src/for_mathlib/boolean_subalgebra.lean) but it's a lot of tedium.

[Andrew Yang]

I think it would still be somewhat useful if there is a predicate about quasi-separeted (but not nessecarily quasi-compact)?
At least I'm defining it over at some algebraic geometry branch (to be "intersections of affine opens is quasi-compact"), and it would be nice if I can say that it only depends on the topological structure with a clean iff.

[Yaël Dillies]

We already have quasi-compact: docs#compact_space.

[Andrew Yang]

Yeah but I don't think there is quasi-separated yet.

[Yaël Dillies]

Indeed not. If you think that's worth having, I'll do it quick.

[Reid Barton]

Yes, good point.