Café Math : Basic Definitions in Category Theory

Hi, some times ago, I wrote a concise description of the very basic concepts in category theory. I was very satisfied of it. Unfortunately, the text was lost and remained so until very recently. As is often the case in such a situation, memory is not as accurate as one may wish and the text is not as good as I thought I remembered. As I'm very happy to have it again I chose to give here a transcript of it so that interested people can take a look. In order to take a positive attitude towards the relative deception, I decided to improve it as much as I can, in an attempt to recover some of the satisfaction I thought it deserved.

As always, don't hesitate to send an e-mail if you want to make suggestions, or add something at the end as a comment.

There are many points of view that lead to the important idea of a category. The one presented here is : categories as graph monoids. I really love this point of view because it gives a glimpse of the unity of sacred Algebra.

There is at least two levels of reading.

First level. : The text gives concise definitions of the basic concepts of category theory. Using the graphs to introduce categories has the charming merit of giving a down to earth picture of them. Seeing them as plain algebraic structures, despite of their *meta* character, is nice too.

Second level. : Once one knows about *symmetric monoidal categories* and the way one can define a generalized monoid over such a category, one can see that categories are just monoids in the symmetric monoidal category of graphs over a given set of vertices, the tensor product being the fibered cartesian product above that set of vertices.

The subsequent point of view is more conventional. It's that of functors as morphisms of category, and natural transformations as morphisms of functors.

Note to the purists. : In order to remove a lot of technicality, we'll ignore the important distinctions between *small categories*, *categories* and *meta categories*.

Definition 1.
A *graph* $G$ is given by two sets $G_0$ and $G_1$ and two mappings $s,t: G_1 \rightarrow G_0$. $G_0$ is the set of its *vertices*, $G_1$ is the set of its oriented *edges*. The vertices $s(a)$ and $t(a)$ are the *source* and *target* of $a$ respectively.

Definition 2.
A *morphism* $F$ between two graphs $G$ and $G'$ is a pair of mappings $F_0 : G_0 \rightarrow G_0'$ and $F_1 : G_1 \rightarrow G_1'$ compatible to the structure in the sense that the two following relations hold:
\begin{align*}
s(F_1(a)) &= F_0(s(a)), &
t(F_1(a)) &= F_0(t(a)).
\end{align*}

We denote by $G_1 \times_{G_0} G_1 = \{ (a,b) \in G_1 \times G_1 \,|\,s(a) = t(b)\}$ the *fibered product* of $G_1$ with itself over $G_0$.

Definition 3.
A *category* $C$ is a graph equipped with two operations,
\begin{align*}
\mathrm{id} &: C_0 \rightarrow C_1 &
\circ &: C_1 \times_{C_0} C_1 \rightarrow C_1
\end{align*}
called identity and composition and satisfying the following axioms,
\begin{align*}
f \circ \mathrm{id}_a &= f, &
\mathrm{id}_b \circ f &= f, &
h \circ (g \circ f) &= (h \circ g) \circ f,
\end{align*}
whenever the composition makes sense.

In a category, oriented edges are called *morphisms* or *arrows* and vertices are called *objects* or *points*. We denote by $f : a \rightarrow b$ an arrow $f$ having *source* $a$ and *target* $b$, and by $\mathrm{Hom}(a,b)$ the set of such arrows.

Definition 4.
A *functor* $F$ between two categories $C$ and $C'$ is a morphism of the underlying graphs satisfying the following relations,
\begin{align*}
F(\mathrm{id}_a) &= \mathrm{id}_{F(a)}, &
F(f \circ g) &= F(f) \circ F(g).
\end{align*}

We say that functors preserve the *identity* and *composition*. They can be seen as morphisms between categories as any category $C$ is equipped with an *identity functor* denoted by $\mathrm{Id}_C$ (it sends both objects $a$ and morphisms $f: a \rightarrow b$ of $C$ to themselves) and composition of functors is associative (composition of morphisms of graphs is associative). The class of graphs forms a category and so does the class of categories.

Definition 5.
A *natural transformation* $\eta : F \Rightarrow G$ between two functors $F, G : C \rightarrow C'$ associates to any object $a$ of $C$ a morphism $\eta_a : F(a) \rightarrow G(a)$ of $C'$ such that every morphism $f : a \rightarrow b$ in $C$ we have the following relation in $C'$,
\begin{align*}
\eta_b \circ F(f) = G(f) \circ \eta_a.
\end{align*}

Definition 6.
The *identity* associated to any functor $F : C \rightarrow D$ between two categories $C$ and $D$ is the natural transformation $\mathrm{id}_F : F \Rightarrow F$ defined component-wise by $(\mathrm{id}_F)_a = \mathrm{id}_{F(a)}$.

Definition 7.
The *vertical composition* $\eta \circ \rho$ of two natural transformations $\rho : F \Rightarrow G$
and $\eta : G \Rightarrow H$ between three functors $F,G,H : C \rightarrow D$ is defined component-wise:
$$
(\eta \circ \rho)_a = \eta_a \circ \rho_a
$$

With this notions of *identity* and *composition*, natural transformations can be seen as morphisms of functors. More precisely, one has a the following definition.

Definition 8.
The *functor category* $D^C$, where $C$ and $D$ are two categories, is the category which objects are functors $F : C \rightarrow D$ and morphisms between two such functors $F$ and $G$ are natural transformations $\eta : F \Rightarrow G$.

A *naturual isomorphism* between two functors $F$ and $F'$ is a natural transformation $\eta : F \Rightarrow F'$ such that there exists another natural transformation $\rho : F' \Rightarrow F$ and such that $\rho \eta = \mathrm{id}_F$ and $\eta \rho = \mathrm{id}_{F'}$. By an obvious symmetry in the definition, $\rho$ is also a natural isomorphism. In that case we often write $F \underset{nat.}{\simeq} F'$ removing any reference to $\eta$ and $\rho$ from the notation.

Sometimes in mathematics, one has the chance to witness a situation that is so rare and so explosively fruitful that it deserves to be called a *miracle*. One such situation arises when two apparently remote notions finally reveal a deep connection and a profound similarity. The most unrelated at first, the most powerful and brilliant the connection proves to be.

The following important notion formalizes *an aspect* of this intuitive picture.

Definition 9.
An *equivalence* between two categories $C$ and $C'$ is a pair of functors $F: C \rightarrow C'$ and $G : C' \rightarrow C$ such that we have two natural isomorphisms,
\begin{align*}
GF &\underset{nat.}{\simeq} \mathrm{Id}_C, & FG \underset{nat.}{\simeq} \mathrm{Id}_{C'}.
\end{align*}

It is not that often that one can discover such a deep connection between two theories, but when it happens, it means that two different theories materialized by two categories are in fact two different formulations of one and the same notion. Each of those formulation caries a particular intuition, is expressed in a particular language and comes along with its own corpus of theorems, deductions and reasonings. An equivalence of category acts as a prism. It permits to reformulate the results associated with one of those formulations in a language that is hopefully totally different. The beauty of it, is precisely that both sides of the equivalence can mutually benefit from each other. At the end of the day a new picture often emerges almost by itself, and its unity can start to eclipse both of the old ones while absorbing their substance.

The interested reader is encouraged to try to find as many examples of that situation as he possibly can, and each time to spend some time in the exploration of the reflections that each sides of the equivalence casts on each other.

Example 1. Just as *involutionary transformations* are interesting examples of *bijections*,
the various notions of *dualities* are particularly bright examples of *equivalences*. A historical example is the lovely duality that exists in the setting of *projective geometry*. In this particular situation, the two sides of the equivalence are identical but the transformation from one side to the other is quite imaginative. The ancients remarked that if one exchanges in every sentences about projective geometry, the notion of line with that of point, the validity of any such statement (either *true* or *false*) was preserved.

Example 2. Poincaré duality of cell complexes is another example of such a reflexive equivalence.

Example 3.
In 1939, C. A. Petri invented — at the age of 13 — an equivalence of categories between *bipartite graphs* and *systems of chemical reactions*. Those bipartite graphs endowed with the interpretation which this equivalence provides are called *Petri nets* in honor of their inventor and constitute a very useful theory. They are used a lot in real life applications, for example by computer scientists, to model complex systems of concurrent interactions.

An adjunction between two functors is a particular relationship that has been recognized by mathematicians to be a structurally important concept. One of the main reason is that most of the mathematical objects are described by so called *universal properties*, and universal properties in turn, most of the time, reveal an adjunction between two functors.
As advocated by S. Mac Lane, one of the fathers of Category Theory:
*Adjunctions are everywhere*.

Universal properties are important in mathematics because they basically give precise characterizations of objects as being *unique* up to a *unique* isomorphism.
Let's say for instance that you and me constructed two solutions to a universal problem. We are therefore assured that those two solutions are *isomorphic*. That's already interesting in itself as this isomorphism is guaranteed *a priori*, but what makes the situation perfectly neat, is precisely that the isomorphism between our two solutions is itself *unique*. This again is guaranteed *a priori*. We don't have to compare our two solutions, we don't even have to communicate, we can just deduce it from the statement of the problem *itself*.

Mathematical objects are to be given the most precise definitions possible and whenever they can be described by a universal property, nothing remains to be desired. Universality unable us to identify any two candidates in a unique way letting thus no indetermination. From that, we are totally freed from the details of the constructions. An important consequence is that, as soon as existence is proven, each and every subsequent properties of such a universal object can be deduced from its universal property *alone*.

Definition 10.
Two functors $F : C \rightarrow D$ and $G : D \rightarrow C$ are called *adjoint* if there exist a natural bijection between the two Hom-sets,
$$
\mathrm{Hom}_D(F\,X,Y) \underset{nat.}{\simeq} \mathrm{Hom}_C(X,G\,Y)
$$
naturality being requiered with respect to both $X$ and $Y$.

The functor $F$ is said to be *left adjoint* to $G$ whereas the functor $G$ is said to be *right adjoint* to $F$. This particular relationship is called an *adjunction* and is denoted by $F \dashv G$.

Samuel VIDAL posted 2012-05-01 13:44:29

To be honest Arish I currently know close to nothing about co induction. I searched google and I'm now reading on that very interesting subject. Thank you very much for you comment.

I am not sure what you have in mind. Co-induction/recursion is about final co-algebras. The rest is syntax sugar, isn't it? And pephars we don't have optimal syntax sugar in Agda or Coq, do we? (And codata has been removed from Agda in favour of sharp and flat in the style of delay and force in Scheme, within data definitions.) The paper advertised by Steve likewise focuses on initial algebras, rather than on syntax for induction and recursion. In the Agda file mentioned above, there is a co-recursion combinator (X -> 1+X) -> X -> CoN and a co-induction principle for CoN using bisimulations in the standard way.It would be interesting to answer the question whether all the co-inductive types definable in Agda and Coq are or are not already definable in ML type theory (assuming extensionality, as done by Steve et al). For example, streams and non-well founded trees are already definable. This covers quite a lot. Also, the so-called delay monad is definable (generalizing the idea used to define CoN). Can you come up with a co-inductive type that is not definable in ML type theory? I think this is an interesting question (which you asked above!).