When I was young and dumb and first learning category theory, I got it into my head that arguments involving sets were not “categorical”. This is not completely crazy as the idea of category theory being an alternate “foundation” and categorical critiques of set theoretic reasoning are easy to find. As such, I tended to neglect techniques that significantly leveraged , and, in particular, representability. Instead, I’d prefer arguments using universal arrows as those translate naturally and directly to 2-categories.
This was a mistake. I have long since completely reversed my position on this for both practical and theoretical reasons. Practically, representability and related techniques provide very concise definitions which lead to concise proofs which I find relatively easy to formulate and easy to verify. This is especially true when combined with the (co)end calculus. It’s also the case that for a lot of math you simply don’t need any potential generality you might gain by, e.g. being able to use an arbitrary 2-category. Theoretically, I’ve gained a better understanding of where and how category theory is (or is not) “foundational”, and a better understanding of what about set theory categorists were critiquing. Category theory as a whole does not provide an alternate foundation for mathematics as that term is usually understood by mathematicians. A branch of category theory, topos theory, does, but a topos is fairly intentionally designed to give a somewhat -like experience. Similarly, many approaches to higher category theory still include a -like level.
This is, of course, not to suggest ideas like universal arrows aren’t important or can’t lead to elegant proofs.
Below is a particular example of attacking a problem from the perspective of representability. I use this example more because it is a neat proof that I hadn’t seen before. There are plenty of simpler compelling examples, such as proving that right(/left) adjoints are (co)continuous, and I regularly use representability in proofs I presented on, e.g. the Math StackExchange.
An elementary topos, , can be described as a category with finite limits and power objects. Having power objects means having a functor such that natural in and where is the (contravariant) functor that takes an object to its set of subobjects. The action of for an arrow is a function where is a (representative) monomorphism and is the pullback of along which is a monomorphism by basic facts about pullbacks. In diagrammatic form:
This is a characterization of via representability. We are saying that represents the functor parameterized in .
A well-known and basic fact about elementary toposes is that they are
cartesian closed.
(Indeed, finite limits + cartesian closure + a subobject classifier
is a common alternative definition.) Cartesian closure can be characterized
as
All the proofs I reference rely on the following basic facts about an elementary topos.
We have the monomorphism
We need the lemma that
Since the arrow
is a pullback.
To restate the problem: given the above setup, we want to show that the elementary
topos
Toposes, Triples, and Theories
by Barr and Wells actually provides two proofs of this statement: Theorem 4.1 of
Chapter 5. The first proof is in exactly the representability-style approach
I’m advocating, but it relies on earlier results about how a topos relates to
its slice categories. The second proof is more concrete and direct, but it also
involves
Sheaves in Geometry and Logic by Mac Lane and Moerdijk also has this result as Theorem 1 of section IV.2 “The Construction of Exponentials”. The proof starts on page 167 and finishes on 169. The idea is to take the set theoretic construction of functions via their graphs and interpret that into topos concepts. This proof involves a decent amount of equational reasoning (either via diagrams or via generalized elements).
Todd Trimble’s argument is very similar to the following argument.
Contrast these to Dan Doel’s proof1 using representability, which proceeds as follows. (Any mistakes are mine.)
Start with the pullback induced by the singleton map.
Apply the functor
Note:
This means that the above pullback is also the pullback of
Since
where the bottom and right arrows are induced by the corresponding arrows of the previous diagram
by Yoneda. Applying
which is to say
Sent to me almost exactly three years ago.↩︎