Unique isomorphism and generalized "the"
Tagged AC, axiom of choice, category, constructive, functor, isomorphism, theory, types, unique
This is part two in a series of posts on avoiding the axiom of choice; you can read part one here.
In category theory, one is typically interested in specifying objects only up to unique isomorphism. In fact, definitions which make use of actual equality on objects are sometimes referred to (half-jokingly) as evil. More positively, the principle of equivalence states that properties of mathematical structures should be invariant under equivalence. This principle leads naturally to speaking of “the” object having some property, when in fact there may be many objects with the given property, but all such objects are uniquely isomorphic; this cannot cause confusion if the principle of equivalence is in effect.
This phenomenon should be familiar to anyone who has seen simple universal constructions such as terminal objects or categorical products. For example, an object \(1 \in \mathbb{C}\) is called if there is a unique morphism \(A \to 1\) from each object \(A \in \mathbb{C}\). In general, there may be many objects satisfying this criterion. For example, in \(\mathbf{Set}\), the category of sets and functions, every singleton set is terminal: there is always a unique function from any set \(A\) to a singleton set \(\{\star\}\), namely, the function that sends each element of \(A\) to \(\star\). However, it is not hard to show that any two terminal objects must be uniquely isomorphic1. Thus it “does not matter” which terminal object we use—they all have the same properties, as long as we don’t do anything “evil”—and one therefore speaks of “the” terminal object of \(\mathbb{C}\). As another example, a product of two objects \(A,B \in \mathbb{C}\) is a diagram \(A \stackrel{\pi_1}{\longleftarrow} C \stackrel{\pi_2}{\longrightarrow} B\) with the universal property that any other \(C'\) with morphisms to \(A\) and \(B\) uniquely factors through \(C\). Again, there may be multiple such products, but they are all uniquely isomorphic, and one speaks of “the” product \(A \times B\).
Note that in some cases, there may be a canonical choice among isomorphic objects. For example, this is the case with products in \(\mathbf{Set}\), where we may always pick the Cartesian product \(\{(a,b) \mid a \in A, b \in B\}\) as a canonical product of \(A\) and \(B\) (even though there are also other products, such as \(\{(b,a) \mid a \in A, b \in B\}\)). In such cases use of “the”, as in “the product of \(A\) and \(B\)”, is even more strongly justified, since we may take it to mean “the canonical product of \(A\) and \(B\)”. However, in many cases (for example, with terminal objects in \(\mathbf{Set}\)), there is no canonical choice, and “the terminal object” simply means something like “some terminal object, it doesn’t matter which”.
Beneath this seemingly innocuous use of “the” (often referred to as generalized “the”), however, lurks the axiom of choice! For example, if a category \(\mathbb{C}\) has all products, we can define a functor \(P : \mathbb{C} \times \mathbb{C} \to \mathbb{C}\)2 which picks out “the” product of any two objects \(A\) and \(B\)—indeed, \(P\) may be taken as the definition of the product of \(A\) and \(B\). But how is \(P\) to be defined? Consider \(\{ \mathrm{Prod}(A,B) \mid A,B \in \mathbb{C} \}\), where \(\mathrm{Prod}(A,B)\) denotes the set of all possible products of \(A\) and \(B\), i.e. all suitable diagrams \(A \stackrel{\pi_1}{\longleftarrow} C \stackrel{\pi_2}{\longrightarrow} B\) in \(\mathbb{C}\). Since \(\mathbb{C}\) has all products, this is a collection of nonempty sets; therefore we may invoke AC to obtain a choice function, which is precisely \(P_0\), the action of \(P\) on objects. The action of \(P\) on morphisms may then be defined straightforwardly.
The axiom of choice really is necessary to construct \(P\): as has already been noted, there is, in general, no way to make some canonical choice of object from each equivalence class. On the other hand, this seems like a fairly “benign” use of AC. If we have a collection of equivalence classes, where the elements in each class are all uniquely isomorphic, then using AC to pick one representative from each really “does not matter”, in the sense that we cannot tell the difference between different choices (as long as we refrain from evil). Unfortunately, even such “benign” use of AC still poses a problem for computation.
-
If you have never seen this proof before, I highly recommend working it out for yourself. Given two terminal objects \(X\) and \(Y\), what morphisms must exist between them? What can you say about their composition? You will need to use both the existence and uniqueness of morphisms to terminal objects.↩︎
-
Note that we have made use here of “the” product category \(\mathbb{C} \times \mathbb{C}\)—fortunately \(\mathbf{Cat}\), like \(\mathbf{Set}\), has a suitably canonical notion of products.↩︎