# Honest application of category theory

I believe that category theory is one of the most fundamental theories of mathematics, and is becoming a fundamental theory for other sciences as well. It allows us to understand many concepts on a higher, unified level. Categorical methods are general, but of course they can be applied to specific categories and thereby help us to solve specific problems. I am not asking for canonical applications in which category theory is used. I have read all answers to similar math.SE questions on applications of category theory, but they don't fit to my question below. I would like to ask for applications of the notions of "category", "functor", and "natural transformation" (perhaps also "limit" and "adjunction") , which go beyond descriptions, but really solve specific problems in an elegant way. I am aware of many, many proofs of theorems which have category-theoretic enhancements, in particular by means of the Yoneda Lemma, but I'm not looking for these kind of applications either. So my question is (even though I know that this is not the task of category theory):

Can you name a specific and rather easy to understand theorem, whose statement naturally does not contain any categorical notions, but whose proof introduces a suitable category / functor / natural transformation in a crucial way and uses some basic category theory? The proof should not just depend on a large theory (such as arithmetic geometry) whose development has used category theory over decades. The proof should not just be a categorical version of a proof which was already known.

So here is an example of this kind, taken from Hartig's wonderful paper "The Riesz Representation Theorem Revisited", and hopefully there are more of them: Let $X$ be a compact Hausdorff space, $M(X)$ the Banach space of Borel measures on $X$ and $C(X)^*$ the dual of the Banach space of continuous functions on $X$. Integration provides a linear isometry $$\alpha(X) : M(X) \to C(X)^*, ~ \mu \mapsto \bigl(f \mapsto \int f \, d\mu\bigr).$$ The Riesz Representation Theorem asserts that this is an isomorphism. For the "categorical" proof, observe first that the maps $\alpha(X)$ are actually natural, i.e. provide a natural transformation $\alpha : M \to C^*$. Using naturality and facts from functional analysis such as the Hahn-Banach Theorem, one shows that if $X$ satisfies the claim and admits a surjective map to $Y$, then $Y$ satisfies the claim. Since every compact Hausdorff space is the quotient of an extremally disconnected space, namely the Stone-Cech-compactification of its underlying set, we may therefore assume that $X$ is extremally disconnected. Now here comes the actual mathematics, and I will just say that there are enough clopen subsets which allow you to construct enough continuous functions. The general case has been reduced to a very easy one, using the concept of natural transformation.

• I would be surprised if in that example, the difficulty of the special case is not exacty the same as the general one. Isn't the «sufficiently many continuous functions» provided by the normality property of compact spaces? (Notice that to even hav a sensible S-C compactification you already need to have many functions!) Commented Mar 27, 2015 at 2:06
• @MarianoSuárez-Alvarez: Well, you will be surprised if you read Hartig's paper :). Universal examples have the advantage of being simpler. For example, $\mathbb{Z}[x]$ is the universal example of a ring containing an element, and this ring happens to be a $2$-dimensional factorial integral domain, which is very nice as compared to other rings. Similarly: In algebraic geometry, working in moduli spaces is often simpler than working with all special points. Commented Mar 27, 2015 at 2:15
• @JoeJohnson126: In fact, the main theorem of Galois theory is really a statement about an adjunction ("Galois connection" in the case of poset categories) and its fixed objects. Category theory is quite useful to organize this, but it's not really an application of the notion of an adjunction between categories, because we would be fine with Galois connection, right? Grothendieck's generalization of Galois theory, in turn, is an equivalence of categories (not just poset categories), so here categories already appear in the statement of the theorem. Commented Mar 27, 2015 at 2:24
• @Martin: yes, i read that, but i thought that proof was more like a categorical version of four proofs which were already known. Nevermind, you're setting the limits here :) Commented Mar 30, 2015 at 8:48
• This kind of unification is quite typical for category theory. Even trivial facts like $X \times (Y \times Z) \cong (X \times Y) \times Z$ for products in a category imply facts about groups, topological spaces, partial orders, simplicial sets, sheaves, etc. at once which are not really trivial when you stick to the set-theoretical instead of the categorical structure. Commented Mar 30, 2015 at 9:01

Does the following standard proof of the Brouwer fixed point theorem for the two-dimensional disk $D$ count?

Theorem. Any continuous map $f : D \to D$ has a fixed point.

Proof. If $f$ had no fixed point, the map $g : D \to \partial D$ given by $g(x) = \partial D \cap ($ray from $f(x)$ to $x)$ would be a retraction of $D$ onto $\partial D$, that is, $g \circ i = 1_{\partial D}$ where $i : \partial D \to D$ is the inclusion. This implies, by functoriality of $\pi_1$, that $g_\ast \circ i_\ast = 1_{\pi_1(\partial D)}$ which is impossible since $\pi_1(D) = 0$, $\pi_1(\partial D) = \mathbb{Z}$.

• Yes, I like it! A similar proof works for the $n$-dimensional disk. One might argue that algebraic topology enters here, whose development has used category theory for a long time, but basically it's really just functoriality of $\pi_1$. Therefore your example is a very nice application of the concept of a functor, and also (indirectly) of the concept of a commutative diagram. Commented Mar 27, 2015 at 11:08
• Sure, for the $n$-dimensional disk substitute $H_n$ or $\pi_n$ for $\pi_1$. Commented Mar 27, 2015 at 12:48
• Basically algebraic topology is full of such examples. The theorem $\mathbb{R}^n \cong \mathbb{R}^m \Rightarrow n=m$ can be proven in the following steps: Apply the functor which maps a space to its one-point compactification, which gives $S^n \cong S^m$. Then, apply the $n$th (reduced) singular homology functor $H_n$, which gives $\mathbb{Z} \cong H_n(S^m)$ and therefore $n=m$. Many spaces $X,Y$ can be separated using (co)homology of homotopy. Commented Mar 27, 2015 at 13:26
• Absolutely, @MartinBrandenburg! Algebraic topology really does use that homology and homotopy are functors in a way that would be very tedious to spell out without using the concept of functor. I just picked one example that seemed particularly simple, while also proving something very cool and non-obvious. Commented Mar 27, 2015 at 15:20

Here is one example, very classical probably. I hope it counts for your purposes!

Proposition. The fundamental group of a topological group $(G,\ast,e)$ is abelian.

Proof. The fundamental group $\pi_{1}$ is a functor from topological spaces to groups which preserves products, so that it sends group objects into group objects. A topological group is a group in the category of topological spaces and is thus sent via $\pi_{1}$ to a group object in the category of groups, i.e. to an abelian group.

• Thank you for your answer. The argument is "hidden" in the sentence "a group object in the category of groups, i.e. to an abelian group" (Eckmann-Hilton). Therefore I think that this is just a categorical version of a proof which was already known. Don't get me wrong, I like this proof very much and it is very elegant, but the proof doesn't seem to use categorical notions in an essential way. Of course it is hard to define what that means precisely, and one could in fact argue that the other answers so far also don't need categorical notions in an essential way. So this is just my oppinion. Commented Mar 28, 2015 at 11:19
• @MartinBrandenburg I don't know, I guess it depends on what you mean by "an essential way" (if you can prove something without using CT, then its use in an alternative proof may not be considered essential at all). Anyway, the fact that a group in groups is an abelian group can be checked independently from the specific case and, from some perspectives, I guess it may even be considered a result in category theory (because it can be formulated using category theory) even if it can be proved in elmentary terms (using Eckmann-Hilton's argument for example) [...] Commented Mar 28, 2015 at 11:27
• @MartinBrandenburg [...] However, you are the one who knows what you are interested in, so consider the answer as you wish :) Commented Mar 28, 2015 at 11:27

A nice example from the area of computer science would be John C. Reynolds "Polymorphism is not set-theoretic" (available here: https://hal.inria.fr/inria-00076261/document). The point is that second-order $\lambda$-calculus does not have set-theoretic models (there is a rather natural definition in the paper of what it means to be "set-theoretic").

The proof is by contradiction: we assume the existence of a set-theoretic model, which allows us to define an initial $T$-algebra $\mu T$, where $T$ is a $\mathbf{Set}$-endofunctor:

$$TX = (X \to \mathbb B) \to \mathbb B$$

for a set $\mathbb B$ with $|\mathbb B| \geq 2$. Lambek's lemma says that the action of this initial algebra is an isomorphism, hence

$$|\mu T| \cong |(\mu T \to \mathbb B) \to \mathbb B|$$

The proof is directed by the categorical "approach" to the concept of initiality, and thus has a very categorical feeling, even though there is nothing categorical in the formulation of the theorem or the definition of what it means to be set-theoretic.

• Thank you for your answer! I'm not experienced enough with computer science, therefore it's hard to follow your answer, which also seems to use another language than the paper. Basically I don't know what you are talking about ;). I know Lambek's Lemma, though. Commented Mar 28, 2015 at 1:35
• In "On Functors Expressible in the Polymorphic Typed Lambda Calculus" by Reynolds and Plotkin (available in Gordon Plotkin's web) a more categorical (generalised) account of this result can be found.
– zxv
Commented Apr 8, 2015 at 21:12

Here are two proofs that both involve recognizing that a big category is the ind- or pro-category of a smaller category, and then proving something about the smaller category to get it for the bigger category.

Theorem: The Pontryagin dual $\text{Hom}(A, S^1)$ of a torsion abelian group $A$ is a profinite abelian group and vice versa; these two maps are inverses to each other on isomorphism classes.

Proof. We will in fact prove a contravariant equivalence of categories. The category of torsion abelian groups is the category $\text{Ind}(\text{FinAb})$ of ind-objects in finite abelian groups, while the category of profinite abelian groups is the category $\text{Pro}(\text{FinAb})$ of pro-objects in finite abelian groups, so it suffices to show that Pontryagin duality is a contravariant equivalence of categories from $\text{FinAb}$ to itself. But this is clear: the Pontryagin dual of the finite cyclic group $C_n$ of order $n$ is (noncaonically) $C_n$ again, and Pontryagin duality respects direct sums. $\Box$

Theorem (Stone's representation theorem): Every Boolean ring $B$ is the Boolean ring $\text{Hom}(X, \mathbb{F}_2)$ of clopen subsets on a profinite space $X$, the Stone space $\text{Hom}(B, \mathbb{F}_2)$ of $B$.

Proof. We will in fact prove a contravariant equivalence of categories. The category of Boolean rings is the ind-category of finite Boolean rings, while the category of profinite spaces is the pro-category of finite sets, so it suffices to show that taking continuous functions to $\mathbb{F}_2$ resp. taking the Stone space is a contravariant equivalence of categories from finite Boolean rings to finite sets. But it's straightforward to prove by induction on the cardinality that every finite Boolean ring is $\mathbb{F}_2^X$ for some finite set $X$ and that it has Stone space $X$. $\Box$

• Great examples. The proofs in the cyclic/finite case might be misleading. The fact that there is some isomorphism $(C_n)^* \cong C_n$ has (almost) nothing to do with the statement that the natural map $C_n \to (C_n)^{**}$ is an isomorphism, which is what we need. Commented Mar 28, 2015 at 4:24
• That observation just makes it really clear that Pontryagin duality is essentially surjective, if that's the way you like proving that a functor is an equivalence of categories. I guess in both proofs above I skipped showing that the relevant functor sends filtered colimits to cofiltered limits, but in both cases it's not hard to show. Commented Mar 28, 2015 at 4:28
• This is not what I wanted to say. For an equivalence of categories $(F,G)$, we need natural isomorphisms $F(G(X)) \cong X$ and $G(F(X)) \cong X$, and proving random isomorphisms $F(X) \cong X$, $G(X) \cong X$ (whatever that should mean, since the types of these objects differ!) is not enough for this. Commented Mar 28, 2015 at 4:29
• @Martin: that's not what I wanted to say! I mean one way to prove that Pontryagin duality is an equivalence of categories is to prove that it's fully faithful and essentially surjective. Both of these essentially follow from the fact that the Pontryagin dual of a finite abelian group is (noncanonically) isomorphic to itself. Commented Mar 28, 2015 at 4:40
• I don't think so. This is not enough. Commented Mar 28, 2015 at 10:22

You can prove the Poincare Lemma by reducing categorically/homotopy-theoretically to the case of a point. Proof: (re-)state the Poincare lemma (every closed form on a contractible subdomain of $\mathbb{R}^n$ is exact) as a statement about De Rham cohomology, and prove that the De Rham cohomology functor sends homotopy equivalences to isomorphisms. I seem to recall learning the Poincare lemma before learning about homotopy invariance, but apparently it's not necessary to go in that order.

• I suppose this only works for smoothly contractible domains (although I don't know any examples of domains which are continuously but not smoothly contractible), but the technical restrictions in the usual statements of the Poincare lemma are even more severe -e.g. restricting to "star-shaped" domains. Commented Mar 27, 2015 at 16:24
• Thank you for sharing this nice example. Regarding your comment: The author seems to use a smooth homotopy, because it is used to pull back differential forms, but this isn't made explicit in the statement of the Lemma. Commented Mar 28, 2015 at 4:35

I don't know if this fits as an answer, but I think that Michael Barr's existence of free groups is a nice application of some basic category theory.

• I assume that you mean the construction $F(S) = \langle \mathrm{im}(f) \rangle$ , where $f : S \to | \prod_{i : S \to |G|} G|$ is the canonical map and the product is taken over some set of $\cong$-representatives of the class of all maps $i : S \to |G|$ which generate $G$? Notice that the proof that such a set(!) of representatives exists is almost the same as constructing the free group directly. I've been a "fan" of this construction and the Adjoint Functor Theorem for a long time, but recently I've gone through the details and the whole approach doesn't convince me anymore. Commented Mar 28, 2015 at 16:36
• Meanwhile I think that the most efficient and useful construction of free structures is not using the Adjoint Functor Theorem (which is merely an existence result), but rather to consider the free structure w.r.t. the underlying signature (i.e. $1^{[0]}$, $\mathrm{inv}^{[1]}$, $*^{[2]}$ in the case of groups), which simply consists of all terms, and only in the end mod out all group axioms. This approach works for arbitrary algebraic structures and can also be internalized into arbitrary cocomplete cartesian categories. Commented Mar 28, 2015 at 16:38
• I'm not sure it can be done in such great generality in arbitrary cocomplete cartesian categories. Besides the obvious condition that the binary product preserve colimits in each variable, which you have no doubt folded into the definition of "cocomplete cartesian", I suspect you also need exactness, or maybe even being a coherent category. Commented Mar 28, 2015 at 19:02
• I mean a cocomplete category with finite products such that $X \times -$ is cocontinuous for all $X$. Why do you think that one needs exactness or coherence? Commented Mar 28, 2015 at 23:31

( This one is from applied mathematics, not theoretical one as all other above!) Take for example a structure where You have a person travelling from New York to San Francisco. CIA is collecting informations about this person, but they are from various sources of information: tickets, credit card records, mobile phone triangulations, wifi access from various places, information form residents in some places etc. All of this informations are in fact functions on different domains ( some of them assigns person to his position - like direct observation, whilst another only in indirect manner - for example plane ticket or wifi data connected with phone imei number). Some of this information may even be lousy related to that person - like not so certain observation of similar car on street camera monitoring.

We put all of this in big data database. What structure data sources ( reflected in data store) must have in order to perform basic tracking of position of such person and perform some basic operations on it?

The answer is: it mus be a (pre) sheaf - which I found very amusing and interesting.