An Empty Product of Nonempty Sets
04 Jun 2025 - Tags: topos-theory
A few days ago I saw a cute question on mse asking about a particularly non-intuitive failing of the axiom of choice. I remember when I was an undergrad talking to a friend of mine about various statements equivalent to choice, and being particularly hung up on the same statement that OP asks about – The product of nonempty sets is nonempty. I understood that there were models where the axiom of choice fails, and so in those models we must have some family of nonempty sets whose product is, somehow, empty! Now that I’m older and I’ve spent much more time thinking about these things, this is less surprising to me, but reading that question reminded me how badly I once wanted a concrete example, and so I’ll share one here!
This should be a pretty quick post, since I’ll basically just be fleshing out my answer to that mse question. But I think it’ll also be nice to have here, since these things can be hard to find when you’re first getting into logic and topos theory! Let’s get to it!
First, let’s remember that for any group
The basic idea of
In particular, we can recover the “
But
which gives us a comonad
As a cute exercise, check that
Now doing computations in this topos is pretty easy! Finite limits and
arbitrary colimits are computed as in
Now with this in mind, we can prove the main claim of this post:
In
So this topos shows explicitly how, in the absence of choice, you can have a family of nonempty sets3 whose product is somehow empty!
The computation is actually quite friendly! To compute
But it’s easy to see that every orbit is infinite! Any element of the
product will contain an element from every
Ok, this one was actually quite quick, which I’m happy about! My parents are visiting soon, and I’m excited to take a few days to see them ^_^. I have another shorter post planned which another grad student asked me to write, and I’ve finally actually started the process of turning my posts on the topological topos into a paper. I’m starting to understand TQFTs better, and it’s been exciting to learn a bit more physics. Hopefully I’ll find time to talk about all that soon too, once I take some time to really organize my thoughts about it.
Thanks for hanging out, all! Stay safe, and we’ll talk soon.
-
In case
then it’s a kind of cute fact that this topos is equivalent to the topos of continuous (discrete) -sets, where is the profinite completion of . See, for instance, Example A2.1.7 on page 72 of the elephant. This gives another computationally effective way to work with this topos!I’m pretty sure I convinced myself that more generally the category of
-sets all of whose orbits are finite should be equivalent to the category of continuous discrete -sets, but I haven’t thought hard enough about it to say for sure in a blog post. ↩ -
Of course, there’s no global points for
, since maps correspond to fixed points. But existential quantification is local, so that the topos models if there’s some surjection and a map .We can takeEdit, June 5: Thanks to Kevin Carlson for pointing out that with its left multiplication action on itself, and there is a map from . with its left multiplication action isn’t in this topos, since its orbit is infinite! We instead need, for each , to look at the surjection from and then you can use the identity map from to witness inhabited-ness.If you’re more used to type theory, we don’t have
, since that would imply a global element. But despite this, we do have the propositional truncation , so that an element of merely exists. ↩ -
Since this topos is boolean, nonempty and inhabited are actually synonyms here. Moreover, this “nonempty” is closer to how a lot of working mathematicians speak, so it felt right to use this wording here. ↩