Zulip Chat Archive

Stream: new members

Topic: Stone Duality

Gonzalo Zigaran (Sep 05 2023 at 21:30):

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 (Sep 05 2023 at 21:37):

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

Yaël Dillies (Sep 05 2023 at 21:38):

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 (Sep 06 2023 at 07:04):

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

Last updated: Dec 20 2023 at 11:08 UTC