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