Introduction To Category Theory
In this post I am going to explain the fundamentals of category theory in order to explain my favorite theorem in a later post. Category theory is a really pure and fundamental part of mathematics, comparable to set theory. Thus it sometimes is dry since there is no immediate application. But constructions from category theory recently found applications like in programming languages, especially Haskell. In a nutshell, category is the study of things together with its structure. It can be used as a foundation for all of mathematics, like set theory.
Another motivation to learn category theory is that sometimes the same concepts surface in different areas of mathematics. For example a product. There is a product of integers, of vector spaces, of topologies, of groups, … So, why not define a product on a much more general structure? The same is true with isomorphisms, or quotients, …
Category, a definition
We start with the basic thing in category theory: a category. A category is a thing together with structure, as motivated above. More precise, a category consists of
- objects , like , i.e., things
- morphisms (or arrows) , like . One can think of these as functions, but they can also be relations or orders, i.e., structure.
- For all morphisms there are objects and , called domain and codomain. We write this as .
- For morphisms such that , there is a morphism . This amounts to composition of morphisms.
- For all objects there is the identity morphism .
Additionally we require
- Associativity: , for all , such that this expression is defined.
- Unity: for all .
The fun part in category theory is always the examples. The category above looks like a set with functions, but indeed it is more general.
- As mentioned, any set is a category. E.g., take and only the identity morphisms .
- Any ordered set is a category. Let be an ordered set. Then we define if . Function composition in this respect means transitivity, i.e., if and , then . So, categories can be used to express order relations.
- The set of all Haskell types is a category, i.e., Integer, Char, Lists of Chars, … (Well, nearly. There are some exceptions, which have to do with undefinedness.) The morphisms are just the usual functions you can write in Haskell.
- The “set of all sets” is a category. If you take all sets together, this is not a set, due to Russel’s paradox, but in a sufficiently generalized manner, this works. Note that in this case the objects do not form a set. This can be formalized, but I am skipping this part.
- For each category we get a dual category by reversing all the arrows.
After looking at categories, the next thing are functions between categories. These are called functors and preserve the structure of the category. Thus, if we take categories as objects and functors as their morphisms, we even get a category of categories.
We call a function between two categories and , i.e.,
a (covariant) functor, if for all objects we have and , for suitable.
We call a functor contravariant if all of the above is satisfied except we have , for suitable, instead of , i.e., they switch places.
Note that we define the action of the functor on the objects, as well as the morphisms. The requirements to preserve the identity and the compositions are the preservation of the structure i have mentioned above.
- Lists in Haskell are a functor. I.e., the morphisms which maps types to a list of types, also Maybe is a functor in Haskell.
- Let us take another Haskell example. Let us define a tree
data Tree a = Leaf a | Branch (Tree a) (Tree a)This is also a functor mapping types into trees containing these types. The composition is preserved, since if we have a tree of things of type , and a function , then we can apply to all things in the tree (this is called ) and get a tree of things with type .
- Taking a set to its powerset is a functor from the category of sets to the category of sets.
- The identity functor is also a functor which maps any category to itself. Thus, as stated above, if we take categories as objects and functors as the morphisms, we can see that all categories together form a category.
- For each contravariant functor , there is a unique covariant functor . Okay, this is not really an example, but more an exercise. Go ahead, Take a pencil and try to define .
Another fun part of category theory is that one always goes a step further. We have categories. We have functors between categories. We have seen that there is a category of categories. But what are the functors there? Turns out, these are interesting to study on its own. We call then natural transformations. With the natural transformations as functors and the functors as morphisms, we even get the category of morphisms.
A natural transformation between Functors is a family of functors such that the following diagram commutes for all .
And with these definitions I will end my expositions. Next time, we can take a look at my favorite theorem: The Yoneda Lemma.
If you are interested in category theory, there is “Categories for the working mathematicians” which started it all. It is primarily written for a mathematical audience.
Then there is “Catgory Theory” by Awodey which is also a good book. He is a little bit more on the computer science side, since he, e.g., introduces lambda calculus as a category.
For pure programmers there is no real resource except the blog, by Bartosz Milewski. This guy is a genius, despite his habit of sometimes drawing objects as pigs and morphisms as fireworks. (Yeah, you read that right. This is also a category.)