structure theorem for finite boolean algebras

Stream: Is there code for X?

[Kevin Buzzard]

I want that if I have finitely many clopen sets in a topological space then I can come up with a new finite set of clopens with the same union, such that every set in the second clopen is a subset of the set in the first clopen (so the second cover refines the first) and furthermore the sets in the second cover are pairwise disjoint.

My instinct is that the "proper" way to do this would be to define sub_boolean_algebra, prove it's closed under arbitrary disjoint unions, define a span or closure operator (are we consistent on which one to use?) from set (set X) to sub_boolean_algebra (set X), prove that the boolean algebra generated by a finite set is finite, pull back the subalgebra to an algebra and then invoke some classification theorem of finite boolean algebras saying that each element is a finite union of atoms (i.e. atoms generate even if you're not allowed to use compl).

Do we have any of this, and how crazy is this strategy?

[Kevin Buzzard]

PS @Ashvni Narayanan

[Bryan Gin-ge Chen]

We don't have any of this yet. I'm actually working on a refactor of Boolean algebras at the moment to insert "generalized Boolean algebras" (structures which only have \ and aren't guaranteed to have a ⊤ or compl) but afterwards I can take on some parts of this.

[Bhavik Mehta]

Do you have a mwe for this? I'd like to try playing with it

[Bryan Gin-ge Chen]

@Bhavik Mehta The code is currently at branch#symm_diff_generalized_boolean_algebra, but I anticipate making a PR either later today or tomorrow.

[Bhavik Mehta]

@Bryan Gin-ge Chen oops sorry - I meant to reply to Kevin's original question

[Ashvni Narayanan]

Bhavik Mehta said:

Do you have a mwe for this? I'd like to try playing with it

From my side, it is under construction :sweat_smile: I need it for a specific case of profinite spaces, but turns out to be more general than that.