Dear Peter, Thanks for your very thought-provoking example. I'm having difficulty coming up with a direct description of the Booleanization of H. Is it the finite unions of principal filters no two of which are siblings? And which Boolean algebra is it? The free countably generated one? Vaughan Prof. Peter Johnstone wrote:
On Sat, 8 Jan 2005, Vaughan Pratt wrote:
Is there a coordinated pair of names for the Boolean algebra arising as the double-negation retract of a Heyting algebra H, and that arising as the completion of H to a Boolean algebra?
I see no harm in calling the Ba of \neg\neg-stable elements the Booleanization of H, since it is entirely analogous to the Abelianization of a group. However, I'm not sure what Vaughan means by "the completion of H to a Boolean algebra", since there are several possible candidates for that title, and they don't agree in general.
If Vaughan is thinking of some construction that returns H itself when H is already Boolean (for example, the Boolean algebra freely generated by H qua lattice), then "completion" is a bad word to use since such algebras won't in general be complete, even if H is. For example, if H is a profinite distributive lattice, represented as the poset of upper subsets of some poset P (Stone Spaces, VII 3.4), then the corresponding Boolean algebra B consists of all subsets of P which are (finite) lattice-theoretic combinations of upper and lower sets, and this is in general not complete (though it is atomic, since all singletons are in B). For example, if P is the real line with its usual ordering, then B consists of all subsets which are finite unions of intervals (using the word "interval" in its broadest sense, to include singletons), and the set of all singletons {q} with q rational has no least upper bound.
Vaughan's comments suggest that he is thinking of a construction which, when H = upper sets of P, returns the full power-set of P. I'm not sure whether there is any such construction on arbitrary (not necessarily complete) Heyting algebras, but for complete Heyting algebras (frames) H one could take the Booleanization of the assembly of H. Is that what Vaughan was thinking of?
Actually I only care about complete Heyting algebras, in fact profinite distributive lattices, in case that makes any difference. The Boolean algebra completing a profinite distributive lattice is clearly a CABA; unless I'm overlooking something it looks like the double-negation retract should be the powerset of the set of maximal filters of H and so a CABA too.
No, it isn't: take H = upper sets of P, where P is the poset of finite sequences of 0's and 1's, ordered by p \leq q iff p is an initial segment of q. For this H, each principal upper set \uparrow(p) is \neg\neg-stable, and there are no atoms in the Booleanization of H.
While I'm on the question of names, here's a really elementary question I don't know the answer to. How acceptable is it to write \sum_J:C^J\to C instead of Colim:C^J\to C when J is not discrete? Is \sum always understood to connote discrete sum or is the usage \sum_J excusable? Seems like context should make the meaning clear when J is a category.
I wouldn't do it myself (any more than I'd use the product sign for limits of non-discrete diagrams), but I don't have strong objections.
Peter Johnstone
11-Jan-2005 13:05:22 -0400,8440;000000000001-00000000