The n-Category Café

For example, in the axioms, we only asked for the existence of preimages (inverse images) of one-element subsets of the codomain of a function. But we didn’t ask for the existence of preimages of arbitrary subsets. Nor did we ask for any kind of images at all. Nevertheless, we prove here that all preimages and images exist.

We also prove that $\mathbf{2}$ has two elements! One of the axioms (loosely stated) is that there exists a set $\mathbf{2}$ such that for all sets $X$, functions $X \to \mathbf{2}$ correspond to injections into $X$ (taken up to isomorphism over $X$). We didn’t assume that $\mathbf{2}$ has two elements. But we prove here that this does in fact follow from the axioms. In other words, it’s a consequence of the axioms that we’re in a world with exactly two truth values.

Then we build up familiar constructions like unions and intersections of subsets, and prove that obey the usual algebraic laws. As we go further down this road, the arguments look more and more like the elementary set theory that everyone’s used to. Put another way, the ETCS approach starts to converge about here with other axiomatizations of sets.

One of the more subtle points in this chapter is that there are two kinds of elementhood (if that’s a word) or membership:

• The first is a type declaration, like when someone begins a conversation with “Let $z \in \mathbb{C}$”. That’s not a true/false statement; you can’t very well reply “No it’s not!”

• The second kind of membership is about whether an element of a set belongs to a particular subset, and that is a true/false statement, like if you’ve got your element $z \in \mathbb{C}$ and you ask whether $z \in \mathbb{R}$. (It either is or isn’t.) In this course, we’d write it as “$z \in_{\mathbb{C}} \mathbb{R}$”.

And in much the same way, there are two notions of subset (Example 4.1.13). But I won’t write more here, as I’ve already explained everything as well as I can in the notes!