Unique isomorphism and generalized “the”

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 isomorphic¹. 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}$ ² 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.↩

About Brent

Associate Professor of Computer Science at Hendrix College. Functional programmer, mathematician, teacher, pianist, follower of Jesus.

View all posts by Brent →

8 Responses to Unique isomorphism and generalized “the”

Tom says:

May 13, 2014 at 2:15 pm

(Slight nitpick: { ∅ } seems like a pretty canonical choice of terminal object, and the cartesian product is not really canonical unless it is part of the definition of the set theory.)

- Brent says:
  
  May 13, 2014 at 2:52 pm
  
  Thanks for the nitpicks!
  
sclv says:

May 13, 2014 at 2:46 pm

Coincidentally, I was _just_ looking at anafunctors and the question of avoiding the AoC in category theory, prompted by some discussion on reddit. There’s an interesting historical connection that you may or may not be aware of in this regard — Makkai introduced anafunctors as you well know in order to formulate a category theory where we need not use AoC. This work later on inspired his work in FOLDS (although that had somewhat different aims). In FOLDS Makkai introduced a concept of an Invariant Foundations, which it seems to me is sort of a vast generalization of the notion of anafunctor (nb I have skimmed the anafunctors work but have not yet really tackled FOLDS in any detail, nor do I know when I will :-P).

Now it turns out that Voevodsky in some recent talks has attributed FOLDS as the greatest inspiration for Univalent Foundations, and said that Invariant Foundations, under a shift from infinity-categories to infinity-groupoids, basically _is_ univalent foundations.

Hence now, it should not surprise us that categories as formulated in the HoTT book do not require the AoC, since it was precisely a program of categories-sans-AoC that kicked off one element of this whole project, way back in the 70s!

- Brent says:
  
  May 13, 2014 at 2:53 pm
  
  Ah, fascinating, I was not aware of the connection between FOLDS and Univalent Foundations/HoTT! Thanks!
  
shebang23 says:

May 14, 2014 at 2:32 am

Hmm, I’m not convinced.

Let’s first consider another example: semigroups. Integers form a semigroup in many (non-isomorphic) ways, so when we say abut an integral semigroup, we must specify what the operation should be. We don’t just “search” for all possible associative operations and then pick one.

In the same way, when we talk about a category that has all products, it seems reasonable to supply a proof, a witness of that property in the form of an operaotion that maps objects to their product.

And when we are defining a category, we’re well positioned to supply such a witness — indeed, if our proof that it has products is constructive, we should already have it.

It seems like this eliminates the need for AoC here.

- Brent says:
  
  May 15, 2014 at 2:50 pm
  
  Hmm, you’re right, these are not the greatest examples. I was trying to pick some simple examples that nonetheless exhibit the problem, but maybe I made them too simple.
  
  Maybe the right way to look at these examples is to say that sometimes we don’t *want* to make canonical choices, even though we *could*. That is, which choice we make does not matter, so it’s annoying to be forced to make one. The question is whether we can retain this “it doesn’t matter” flavor in our reasoning and constructions, avoiding the need to commit to any particular choice, while still avoiding the axiom of choice and remaining firmly constructive.
  
Pingback: AC and equivalence of categories | blog :: Brent -> [String]
Pingback: Anafunctors | blog :: Brent -> [String]