Ultrafilters on Boolean Algebras

Stream: maths

[Aaron Anderson]

For model theory purposes, I'd like to use the construction of the Stone-Cech space of ultrafilters on a general boolean algebra.

[Aaron Anderson]

I recall that we have pfilter as an alternative to filter for more general lattices, but it seems not to have gone very far.

[Aaron Anderson]

Where can I begin my generalization without messing up too much API?

[Yaël Dillies]

Start by replacing the definition of filter with pfilter then, file by file, duplicate all lemmas that use set-specific operations, generalize the first duplicate to boolean algebras and prove the second one using the first.

[Aaron Anderson]

This would maybe be my instinct, but the main conclusion of the discussion about pfilter was that basically any change to the definition or basic API of filter would be extremely difficult and ill-advised

[Yaël Dillies]

I disagree. The definition translates verbatim, which is the most important part.

[Yaël Dillies]

It'll be a bunch of work, but if you stick to changing one file at a file, it should be pretty straightforward.

[Adam Topaz]

If you don't want to duplicate a bunch of the API, you could use $\mathrm{Spec}$ :)

[Aaron Anderson]

Do we really have Spec in that level of generality? Even if we do, what I'm looking for puts a slightly different topology on Spec.

[Adam Topaz]

It's not the Zariski topology?

[Adam Topaz]

I'm talking about Spec of a commutative ring here... you can view any boolean algebra as a commutative ring.

[Aaron Anderson]

Actually, I'm not sure if it's the Zariski topology, as I haven't thought about boolean rings much. I need varieties to be clopen rather than closed - perhaps this is true in boolean rings.

[Johan Commelin]

I think it is

[Damiano Testa]

I also agree (with a minor doubt) that for boolean rings, the Zariski topology has the property that closed subsets are also open. The minor doubt has to do with the fact that the ring need not be of finite type.

After a lot of words, the key identity is the following:

import algebra.ring.boolean_ring

variables {R : Type*} [boolean_ring R] {a : R}

example : a * (1 - a) = 0 := by simp

The example shows that the vanishing set of a coincides with the non-vanishing set of 1-a.

Thus, the Zariski topology admits a sub-basis of clopen sets.

In fact, there is a (possibly) different topology that you can put on any scheme where you declare the quasi-compact opens and their complements to form a sub-basis for the topology. This is sometimes called the constructible topology. My small concern is exactly about the quasi-compact assumption that floats around.

[Damiano Testa]

EDIT: resolved below by Yaël -- boolean algebras have ⊤ as identity under ⊓ as multiplication.

On a slightly separate note, I found out that the module doc-string for boolean_ring says

A Boolean ring is [...] equivalent to Boolean algebras.

though it seems that there need not be a 1 in a boolean algebra.
(Of course, equivalent can be interpreted in multiple ways: does it make sense to specify that boolean rings are equivalent to boolean algebras with an identity?)

[Yaël Dillies]

In this context, 1 is top, right? In which case, yes, boolean algebras have a top, but not generalized boolean algebras.

[Damiano Testa]

Ah, I think that you are right! I tried writing 1 and boolean algebra complains that there is no has_one instance.

variables {S : Type*} [boolean_algebra S] {b : S}

example : b ⊓ ⊤ = b := by simp

works!

[Yaël Dillies]

Note that having 1 as notation for ⊤ in all boolean algebras will conflict with docs#set.has_one (and docs#finset.has_one over a fintype), which is useful in the context of pointwise operations.

[Damiano Testa]

Ok, thanks for the explanation! I was not going to suggest adding the instance, but I was wondering why it was not there.

[Bryan Gin-ge Chen]

If there's interest in the boolean algebras / boolean rings equivalence, I'll try and come back to #6476 within a few days.

[Adam Topaz]

@Yaël Dillies I never heard of generalized boolean algebras. Is there even a Stone duality for such gadgets?

[Reid Barton]

I don't know what a generalized boolean algebra is either but if it's something like a "boolean algebra without 1", then it probably corresponds to something that looks locally like a Stone space and is still quasiseparated (= intersection of qc opens is qc)

[Reid Barton]

we just don't require the whole space to be qc

[Yaël Dillies]

A generalized boolean algebra is a boolean algebra without a top. We mostly use it in mathlib to have \ on finset (but also to generalize stuff like docs#uv.compress).

[Aaron Anderson]

Ok, I now believe that using Spec could theoretically work.

[Aaron Anderson]

However, is this really the best way to go about things? I feel like I'd at least have to duplicate some of the API, at least when I prove that such a space is actually totally disconnected, and I do feel like Stone duality is important enough to find the right way to do it

[Adam Topaz]

Check out nlab#Stone-duality I think more or less everything there should be doable