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!