Here is one way of saying what a pyknotic set is. Fix an inaccessible cardinal $\kappa$, and let $Proj_\kappa$ be the category of $\kappa$-small, extremally disconnected compact Hausdorff spaces. Recall that Stone duality restricts to an equivalence between the opposite category $Proj_\kappa^{op}$ and the category $CBool_\kappa$ of $\kappa$-small, complete Boolean algebras, and all Boolean algebra homomorphisms. Barwick and Haine define a pyknotic set $X$ to be a sheaf on the category $Proj_\kappa$ with respect to the canonical Grothendieck topology. It turns out to be very easy to say what this means explicitly. That is, we have:
Definition: A pyknotic set comprises
- A functor $X: CBool \to Set$;
(i.e. for each complete boolean algebra $B$ we have a set $X(B)$, and for each boolean algebra homomorphism $B \to B'$ we have a function $X(B) \to X(B')$ respecting identities and composition)
- such that $X$ respects finite products.
(i.e. $X(1)$ is a singleton, where $1$ is your favorite 1-element Boolean algebra, and the canonical map $X(B \times B') \to X(B) \times X(B')$ is a bijection for any pair of complete Boolean algebras $B,B'$.)
I've chosen to state the definition of a pyknotic set this way; the condensed sets of Clausen and Scholze are similar, but avoid the requirement of choosing an inaccessible cardinal. This is done by defining $Proj_\kappa$ as above where $\kappa$ is merely a strong limit cardinal, and then taking a direct limit over all $\kappa$'s to arrive at the final notion.
Now, the thing about complete Boolean algebras is that it seems they're more commonly studied by set theorists than by anybody else. My understanding is that in the "Boolean-valued models" approach to forcing, the forcing extension is more-or-less identified with sheaves on the forcing poset, which is a complete Boolean algebra. From this perspective, it sounds like a pyknotic set is somehow a set which "lives in all forcing extensions at once".
Question:
-
Do set theorists have a notion of a "set which lives in all forcing extensions at once"?
-
If so, how similar is such a thing to the data of a pyknotic / condensed set?
-
In any event, do there exist theoretical frameworks in set theory for talking about objects like pyknotic / condensed sets?
My initial guess is that in multiverse-type frameworks, one probably considers morphisms of forcing posets which preserve a little more structure than just an arbitrary boolean algebra homomorphism, so that perhaps the connection is not so tight. But I really have no idea!
Best Answer
Great question — for some reason this tight relation between extremally disconnected profinite sets and forcing had elapsed me!
I've just been trying to read a bit about it. From what I understand, the sheaf-theoretic approach to forcing, as in MacLane-Moerdijk "Sheaves in geometry and logic" Chapter VI, consists of three steps.
Start with any extremally disconnected profinite set $S$. Consider the category of open and closed subsets of $S$, with the following notion of cover: $\{U_i\subset U\}_i$ is a cover of $U$ if $\bigcup_i U_i\subset U$ is dense in $U$. (This is what, I believe, the "double negation topology" amounts to.) In this topology, the subsheaves of $\ast$ are exactly given by the open and closed subsets $U\subset S$, so one has a boolean topos. The first step is thus completed: The construction of the boolean topos of sheaves $\mathrm{Sh}(S)$ on $S$.
The second step is to pick any point $s\in S$, and take the colimit $\varinjlim_{U\ni s} \mathrm{Sh}(U)$. Here, the subsheaves of $\ast$ are just $\emptyset$ and $\ast$, so it's a boolean topos with only two truth values.
The third step is to start with the topos $\varinjlim_{U\ni s} \mathrm{Sh}(U)$ and somehow make it into a model of ZFC. When I've previously tried myself to contemplate forcing from the sheaf-theoretic point of view, this is the point that got me very confused: In a model of ZFC, elements of sets should be sets, but there's no meaningful way to talk about elements of objects in this topos, and certainly they won't be objects of this topos. I have to read more about this step; MacLane-Moerdijk cite work of Fourman. Apparently the idea is to redo the iterative construction of $V_\alpha$'s by iteratively taking the powerset, but now internally in this topos. [Edit: This third step deals with the problem of turning a structural set theory into a material set theory. A very nice discussion of this is in the paper Comparing material and structural set theories of Shulman. In particular, he explains how to very cleanly go back and forth between models of ECTS + a structural form of replacement, which $\varinjlim_{U\ni s} \mathrm{Sh}(U)$ satisfies, and models of ZFC, see Corollary 9.5.] (I might at this point be sold on structural set theory — forcing seems to have an extremely clean formulation in terms of structural set theory, namely just $\varinjlim_{U\ni s} \mathrm{Sh}(U)$. Please correct me if I'm misunderstanding something!)
In any case, the third step seems to be orthogonal to the question at hand. More salient is that the category of sheaves on $S$ is actually incompactible with the category of sheaves on $S$ that we would consider, where covers are just open covers. This is critical! If $S$ is the Stone-Cech compactification of a discrete set $S_0$, then sheaves in our sense are equivalent to functors on subsets of $S_0$, taking finite disjoint unions to products. But in the forcing-sense, they are equivalent to such functors taking all disjoint unions to products; equivalently, they are just sheaves on the discrete $S_0$. Most condensed sets of interest (like $\mathbb Z$ or $\mathbb R$) do not have this property; actually, the condition singles out the compact Hausdorff condensed sets if I'm not mistaken.
So even before analyzing the question of how to put this together for varying $S$, I think there are slightly different things happening even for individual $S$. But I agree that it's definitely worth finding out if there's something more to this!
Addendum in response to Mike Shulman's question in the comments below: I think $\varinjlim_{U\ni s} \mathrm{Sh}(U)$ is well-pointed. The key seems to be the following: If $f: B\to A$ is a map in $\mathrm{Sh}(S)$ that is surjective in the stalk at $s$, then $f|_U$ is surjective for some $U$ containing $s$. (This property does seem surprising to me. Is it a formal consequence of being a boolean topos?) To prove this, we prove that if $f|_U$ is not surjective for all such $U$, then also $f$ is not surjective in the stalk at $s$. Look at pairs $(V\subset S,a\in A(V))$ of an open and closed subset $V\subset S$ and a section $a$ of $A$ over $V$, such that $a\times_{A|_V} B|_V=\emptyset$. There is an obvious partial order on such; by Zorn's lemma and as any section over a union $\bigcup_i V_i$ extends to the closure by the notion of covering, there is some maximal such $(V,a)$. If $s\in V$, then in particular $f$ is not surjective on the stalk at $s$, as desired. Otherwise, let $U=S\setminus V$, which contains $s$. By assumption, $f|_U$ is not surjective, so there is some $U'\subset U$ and $a'\in A(U')$ such that $a'\times_{A|_{U'}} B|_{U'}$ (a subsheaf of $\ast|_{U'}$) is not all of $\ast|_{U'}$, and thus given by $\ast_{U''}$ for some $U''\subsetneq U'$; replacing $U'$ by $U'\setminus U''$, we can assume that $a'\times_{A|_{U'}} B|_{U'}=\emptyset$. But then $(V\sqcup U',a\sqcup a')$ extends $(V,a)$, contradicting maximality of $(V,a)$.