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:23 -0400,1339;000000000001-00000000