# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: structure theorem for finite boolean algebras

#### Kevin Buzzard (Mar 19 2021 at 12:35):

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 (Mar 19 2021 at 12:36):

PS @Ashvni Narayanan

#### Bryan Gin-ge Chen (Mar 19 2021 at 15:04):

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 (Mar 19 2021 at 16:05):

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

#### Bryan Gin-ge Chen (Mar 19 2021 at 16:27):

@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 (Mar 19 2021 at 18:42):

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

#### Ashvni Narayanan (Mar 19 2021 at 18:59):

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.

Last updated: May 07 2021 at 22:14 UTC