Reference on overlap algebras

]]>Cross-linked to Stonean and Boolean locales.

]]>Stone duality for complete Boolean algebras.

]]>That's true.

]]>Thanks, Toby. I haven’t expressed my thoughts very well (and anyway they’re in a different direction from the point you’re making): the notion of completely distributive complete Boolean algebra is manifestly expressible via an infinitary Lawvere theory. The axioms of such a theory, since they do not involve essential uses of disjunction, existential quantification, or negation, do not involve any non-trivial reformulations or undergo bifurcations when we move to a constructive setting.

]]>@Todd: Being atomic is not what causes the problems constructively; being Boolean is. It's slightly nontrivial to formulate being atomic in a constructive manner (see discussion at atom), but when you do it, then it is *true* that power sets are atomic. (It's also true that they're completely distributive, of course.)

Thanks!

That argument works generically for (co)complete locally small categories. It feels like something that should have consequences for universe-ambiguity in category theory, but I’ll have to chew on that idea more.

]]>Is it true that every non-degenerate Grothendieck topos satisfies Giraud’s axioms only in the universe in which it is defined?

The notion of “Grothendieck topos” is always relative to a universe. A $U$-Grothendieck-topos is locally $U$-small, has a $U$-small generating set, has $U$-small limits and colimits (including $U$-small disjoint and stable coproducts, which is the non-finitary one of Giraud’s exactness axioms), and is equivalent to the category of $U$-small sheaves on a $U$-small site. If you’re asking whether a nondegenerate $U$-Grothendieck-topos might happen to also be a $U'$-Grothendieck-topos for some other $U'$, then I think the answer is no, not if $U\in U'$, since a $U$-Grothendieck-topos would then be a $U'$-small category, so by Freyd’s theorem if it were also $U'$-cocomplete it would be a poset, and the only topos that’s a poset is the degenerate one.

]]>Nice argument, Zhen!

]]>Obviously, one has to fix some cardinal constraints – otherwise whatever Lawvere theory you pick, you could just go one universe up and note that the theory has a model that is not complete in the bigger universe. (Is it true that every non-degenerate Grothendieck topos satisfies Giraud’s axioms only in the universe in which it is defined? Completeness pushes the size of a Grothendieck topos upwards, while local-smallness pushes the size downwards.)

Anyway, whatever we do, it cannot work, because models of an infinitary Lawvere theory (of whatever cardinality) can be pushed forward along right adjoints. So consider the complete atomic boolean algebra $2$ and the skyscraper sheaf functor $x_* : \mathbf{Set} \to \mathbf{Sh}(X)$ for some point $x$ in a sufficiently non-trivial topological space $X$. Then $x_* 2$ cannot be the power object of anything in $\mathbf{Sh}(X)$: indeed, if $x_* 2 = P A$, then for any non-empty open subset $U$ not containing $x$, we must have $A(U) = \emptyset$, and for any open subset $V$ containing $x$, we must have $A(V) \ne \emptyset$; but then we would have a map $A (X) \to \emptyset$ with $A (X) \ne \emptyset$, because certainly $x \in X$.

]]>It does seem unlikely!

]]>Well, good point. I guess my comment was directed more at replacing the term “atomic” with the term “completely distributive”, whose equationality would seem less prone to raising constructivist concerns than the notion of being atomic.

Is there an infinitary Lawvere theory whose models in any Grothendieck topos $E$ are given by the monadic functor $P: E^{op} \to E$? As you point out, the theory of completely distributive complete Boolean algebras won’t work. But it doesn’t seem very likely to me now that there is any Lawvere theory description that would work uniformly – or if there is, how would one describe it?

]]>I don't know if it's constructively true that $Set^op$ is equivalent to the category of completely distributive complete Boolean algebras, but if so, it's not through the power set functor, which essentially never lands in Boolean algebras at all.

]]>I added a few words on algebraicity aspects of complete Boolean algebras (they form a variety of infinitary algebras, which however is not monadic over $Set$).

Incidentally, looking over the constructive-mathematics remarks of CABA’s – do I recall correctly that they can also be described (classically) as completely distributive complete Boolean algebras, and that this gives an alternative constructively acceptable definition?

]]>at *complete Boolean algebra* I fixed the missing ${}^{op}$ and then added a pointer to *Set – Properties – Opposite category and Boolean algebras*.