Stone duality

Stream: Is there code for X?

[Sam van G]

Hi all, in preparation for a talk that I'm giving here in Paris (Orsay, to be precise) in a couple of days, I am trying to find out how much of Stone duality has been formalized in Mathlib.
In particular, does anyone know if the correspondence between sober spaces and spatial frames has been formalized/attempted? Even just the up-to-iso bijection on objects would be interesting to see, of course the full dual equivalence including morphisms would be even better.
Searching Zulip, I found some old threads, in particular this one, but looking at the mathlib docs there are mostly definitions, not yet the accompanying theorems.

[Sam van G]

There are well-known links between these dualities and the profinite, since profinite sets = Boolean-Stone spaces and profinite posets = Priestley spaces, so this could also fit well with the questions recently asked in this thread.

[Adam Topaz]

I think @Yaël Dillies was working on this at some point?

[Yaël Dillies]

There hasn't been any progress since we last talked, @Sam van G

[Yaël Dillies]

We're still missing some boring API

[Sam van G]

A little update. Since LFTCM2024 and a bit before, @Filippo A. E. Nuccio, @Dagur Asgeirsson, @Tomáš Jakl and I have been working on a formalization of Stone duality for Boolean algebras. Just now, I pushed a commit to that repository that makes

def Equiv : Profinite ≌ BoolAlgᵒᵖ

sorry-free. The file is way too long and I have not yet made an effort to clean it up and get it ready for Mathlib.
One crucial bit for this theorem, namely the prime ideal theorem for distributive lattices, recently made it into Mathlib, see #12705 .
It should now be possible to also formalize Stone's and Priestley's dualities for distributive lattices.

[Dagur Asgeirsson]

It should also be easy now to deduce the equivalence between LightProfinite and the opposite category of countable boolean algebras. Although this project will not need to use that equivalence (it's easier to use the characterisation of light profinite sets as second countable profinite sets which follows from #12986)

[Andrej Bauer]

And the prime ideal theorem was used already to prove Joyal's representation theorem, see https://github.com/awodey/joyal (@Sam van G already knows about it). Joyal's theorem generalizes the Stone representation theorem.

[Dean Young]

It seems like a good idea to group Stone Duality with Gelfand Duality because of the similarities.

[Junyan Xu]

It is known that an infinite profinite group must have the cardinality of a power set. Must an infinite profinite set / Stone space also? I asked on https://lmarena.ai/ and Claude said for an infinite Stone space X, one has |X| = 2 ^ |B| where B is the Boolean algebra of X and called it Tarski's theorem, but maybe it's just hallucination as Google returned no relevant results.

[Dagur Asgeirsson]

$\mathbb{N} \cup \{\infty\}$ is a counterexample

[Junyan Xu]

Thanks! I can see it's compact and totally separated, but don't yet see how it's an inverse limit of finite sets.

[Dagur Asgeirsson]

Like any compact and totally separated space, it is the inverse limit of its discrete quotients (docs#Profinite.asLimit).

More concretely, in this case you can show that it is the limit of the tower $\cdots \to \{0,\dots,n+1\} \to \{0,\dots,n\} \to \cdots$

[Vasilii Nesterov]

Are we still missing Stone duality in Mathlib? If so, I can start working on it. I'd like to prove the representation theorems for Boolean algebras and distributive lattices.

[Yaël Dillies]

No, it's not in mathlib yet

[Sam van G]

Hi @Vasily Nesterov (and anyone else reading!), I would be very happy if someone took this up. Just in case you're not aware, last spring we managed to get to a sorry-free proof of Stone duality for BA, based on a blueprint.

[Sam van G]

The problem with our Lean code is that it is, to put it euphemistically, of rather variable quality, and certainly not mathlib-ready. Since last spring, as far as I know all the contributors (myself included) were too busy with other projects to get it into mathlib-ready shape (some small parts that we obtained while working on this did make it into mathlib, see #12705 and #12651).

[Sam van G]

Extending to bounded distributive lattices would of course be great too. (There are at least two sub-projects there: Stone's duality with compact-open sets, or Priestley duality with clopen up/down-sets.)

[Sam van G]

The representation theorem for BA is an easy corollary of the duality -- it's essentially immediate from Proposition 20 in my blueprint.

[Sam van G]

I would also expect that the code from #12705 lets you get to the representation theorem for DL fairly easily (to be confirmed).

[Sam van G]

Finally, the link to the slides of my talk at CIRM, where we did a good chunk of this work, in case that's useful, and pinging @Tomáš Jakl @Dagur Asgeirsson and @Filippo A. E. Nuccio in case they have anything to add -- there may have been more developments since ~June 2024 that I am not aware of.

[Vasilii Nesterov]

Thank you, Sam! I'll take a look