Timeline for Stone duality for the algebra of Boolean functions such that $f(\top,\dots,\top) = \top$, or: What does the presheaf topos on $FinSet_\ast$ classify?
Current License: CC BY-SA 4.0
23 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 26, 2021 at 21:37 | vote | accept | Tim Campion | ||
| Jan 26, 2021 at 16:12 | answer | added | Simon Henry | timeline score: 8 | |
| Jan 26, 2021 at 16:06 | comment | added | Tim Campion | @AndreasBlass Fixed, thanks! მამუკა ჯიბლაძე: Thanks, that's very enlightening. A quick look at the axioms for a Boolean algebra confirms that indeed, your axiom is necessary and sufficient for upper-intervals to be Boolean. Since every finitely-generated lattice is finite so bounded, it follows that the finitely-generated models of the theory with your axiom included are precisely the finite Boolean algebras. So contrary to my assertion, every finitely-generated model is projective; there is no difference between the equational and universal theories. If you post an answer, I'll gladly accept! | |
| Jan 26, 2021 at 15:52 | history | edited | Tim Campion | CC BY-SA 4.0 |
added 354 characters in body
|
| Jan 26, 2021 at 15:45 | comment | added | Andreas Blass | In the third of your axioms borrowed from Heyting algebras, $x\land(x\to y)$ should not be equal to $y$ but to $x\land y$. | |
| Jan 26, 2021 at 14:37 | comment | added | მამუკა ჯიბლაძე | I believe I've seen a duality for these somewhere. Duals are locally compact zero-dimensional locales, and from this point of view it is more convenient to consider Boolean algebras without top rather than without bottom (clopens of a locally compact form such a thing). Passing from $M$ to $M\times M^\circ$ corresponds to the one-point compactification. Conversely, from pointed Stone spaces to locally compact zero-dimensionals one passes just by removing the basepoint. | |
| Jan 26, 2021 at 14:31 | comment | added | მამუკა ჯიბლაძე | Accordingly, for your axioms you need to add that for any $b$ the interval $[b,\top]$ is a Boolean algebra. This amounts to $a\lor a\to b=\top$. Note that any filter in any Boolean algebra is a model. Conversely, for any model $M$ one gets a Boolean algebra $M\times M^\circ$ in which $M$ is an ultrafilter. | |
| Jan 26, 2021 at 14:22 | comment | added | greg | @Tim Campion, it would be great if we could talk. Please call me. | |
| Jan 26, 2021 at 14:20 | comment | added | მამუკა ჯიბლაძე | I also do not see it. What might help is that actually $\mathrm{FinSet}_*$ is monadic over $\mathrm{FinSet}$. Also, the fact is that $\mathrm{FinSet}_*$ does contain a Boolean lattice $B:=\{\text{basepoint},\text{nonbasepoint}\}$ such that any Cartesian functor is uniquely determined by its value on it. This is not a Boolean algebra since negation is not ours, but nevertheless it is a distributive lattice with every element complemented, so the same will hold for any model of the corresponding Cartesian theory. | |
| Jan 26, 2021 at 14:07 | history | edited | LSpice | CC BY-SA 4.0 |
\mathit etc.
|
| Jan 26, 2021 at 14:03 | history | edited | Tim Campion | CC BY-SA 4.0 |
added 758 characters in body
|
| Jan 26, 2021 at 13:38 | comment | added | Tim Campion | @მამუკაჯიბლაძე Edits made. Hopefully the information in the question is now accurate. I can see how the theory of Boolean algebras equipped with an ultrafilter is a natural guess, but I don't see how to complete the argument. For instance, there is an identity $Psh(C/c) = Psh(C)/c$, but I don't think there's a similar identity for $Psh((C/c)^{op})$ in terms of $Psh(C^{op})$. | |
| Jan 26, 2021 at 13:33 | history | edited | Tim Campion | CC BY-SA 4.0 |
added 339 characters in body
|
| Jan 26, 2021 at 8:03 | comment | added | მამუკა ჯიბლაძე | I believe it classifies what I said: either Boolean algebras equipped with a homomorphism to the 2-element Boolean algebra, or, dually, pointed Stone locales. | |
| Jan 26, 2021 at 7:01 | comment | added | Tim Campion | I will edit this question in the morning, but again -- what I really want to know is what the presheaf topos $Psh(FinSet_\ast)$ classifies. | |
| Jan 26, 2021 at 6:40 | comment | added | Tim Campion | @მამუკაჯიბლაძე Ah, thanks! So the free Boolean algebra on $m$ generators has $2^{2^m}$ elements. The powerset lattice on a set with $n$ elements is a Boolean algebra with $2^n$ elements, which is not free in general, but which is projective... In order to translate into classical Lawvere theory language I should restrict to the free ones, so the move to $Set_{2^\bullet}$ sort of makes sense in that light. Now I will have to think through whether my description in terms of "connectives" is accurate. The "real" question -- the one I care about -- is what $Psh(FinSet_\ast)$ classifies. | |
| Jan 26, 2021 at 6:31 | comment | added | მამუკა ჯიბლაძე | Maybe you actually had in mind the category of free finite Boolean algebras. Its idempotent completion is the category of all nontrivial finite Boolean algebras (since all of them are projective) | |
| Jan 26, 2021 at 6:06 | comment | added | Tim Campion | @მამუკაჯიბლაძე It appears that I must be confused -- it does seem to follow from what I've said both that $FinBool$ is closed under finite colimits and that it's not idempotent complete -- a clear contradiction! | |
| Jan 26, 2021 at 5:58 | comment | added | მამუკა ჯიბლაძე | For models in a general topos one must be more careful, presumably these are pointed compact zero-dimensional locales, but here I am not so sure. | |
| Jan 26, 2021 at 5:57 | comment | added | მამუკა ჯიბლაძე | I would have an answer ready but became confused by your $\mathrm{FinSet}_{2^\bullet}$. Conventional duality goes between just $\mathrm{FinSet}$ and $\mathrm{FinBool}$, through the powerset functor and the atoms functor. Through this duality $\mathrm{FinSet}_*$ is dual to the slice $\mathrm{FinBool}/2$, so I would guess the theory classifies Boolean-algebras-with-an-ultrafilter, or dually pointed Stone spaces. More precisely, this would be the category of points of the classifying topos. | |
| Jan 26, 2021 at 5:38 | history | edited | Tim Campion | CC BY-SA 4.0 |
added 17 characters in body
|
| Jan 26, 2021 at 5:16 | history | edited | Tim Campion | CC BY-SA 4.0 |
added 666 characters in body
|
| Jan 26, 2021 at 4:09 | history | asked | Tim Campion | CC BY-SA 4.0 |