Stone Duality

Stream: new members

[Gonzalo Zigaran]

Hi,
I'm Gonzalo Zigarán, and i'm taking the course in formalization in the National University of Cordoba.
For the course project i'm thinking to formalize the Stone Duality (given by the Stone's representation theorem for Boolean algebras). I was checking the mathlib and found some necessary definitions but nothing in the direction to prove the theorem.

I'm a mathematician working on universal algebra and I took a category theory course, so I'm familiar with the result to formalize it.

I was wondering if there is any work or progress to formalize something about categorical dualities and if you have any suggestions.

[Anatole Dedecker]

@Sam van G weren't you working in that direction?

[Yaël Dillies]

Yes, this is well under way. Sorry! I have Birkhoff's duality on a branch and Sam has most of the remaining pieces to go from there.

[Sam van G]

Indeed, we have a PR that I need to return to. I would be interested to participate in a possible continuation.