Category Theory Basics, Part I
otherPublished on September 18, 2016, last updated June 1, 2017
- What is a category?
- Category of finite sets, internal and external diagrams
- Endomaps and identity maps
- Composition
- Isomorphisms
- Sections and retractions
- Monomorphism and epimorphism
- Composing sections and retractions
- Theorem of uniqueness of inverses
- Another definition of isomorphism, automorphism
When you do Haskell on daily basis (simply put, earn a living writing Haskell code), sooner or later you start to regret you don’t have background in advanced math (unless you have such background, of course, and in that case the post will be probably uninteresting for you). I think it’s a situation in which people who use Haskell as engineers (not researchers) find themselves at some point.
The most important and relevant math area for a Haskeller is probably
category theory, which does look scary at first and Wikipedia
articles/videos of lectures seem to be only partially understandable, always
leaving you with a bunch of new notions unexplained. There is no problem to
understand what Monad
means and how it’s useful in functional programming
(although the abstraction may take some time to sink in), but the feeling of
missing “bigger picture”, full of wonderful ideas may not leave you once you
started to use abstractions from category theory.
So, having intuitive understanding of what the word “injective” means and more-or-less proper understanding of what some things like “isomorphism” mean, I decided to read a book that describes all the concepts in order and using simple language.
The book I found is called “Conceptual Mathematics—A First Introduction to Categories” by F. William Lawvere and Stephen H. Schanuel. The book does not assume math background of any sort and anyone can understand concepts described in it. You can give it a try, but the books in not short—376 pages, and it does not even get you to monads (probably will need something else after it if I decide that I haven’t got enough). So this post is the first in a series of blog posts1 that I want to write as a sort of overgrown cheat sheets that highlight important ideas from category theory in a concise form.
I hope that working on the blog posts will help me better organize the ideas from the book in my head, and may be useful for others who may not necessarily have the time to read the book.
Note: here is a somewhat similar post here, but it tries to make the concepts more programmer-friendly by providing examples from “programming world” using pipes, compilers, and circuits. I have no such intention, and in fact I tested this descriptions on people who are neither programmers nor mathematicians, and it worked!
What is a category?
As everything in math, we need some starting points and definitions to build on. The main definition is of course category itself. Category is defined by objects and maps (synonyms: arrows, morphisms, functions, transformations). There are also a few laws that should hold for the objects and maps in order to form a category, but we will get to them a bit later.
Objects can be pretty much everything. The simplest and most intuitive object is probably finite set (just a collection of things), and it will be discussed in the next section.
Maps have domain (an object), codomain (an object again), and a
rule assigning to each element2
An important thing here is that if we say that object
At this point it should be clear that category theory is a very abstract thing. If we study abstract transformations of abstract objects, then certainly we study something that takes place in every area of science and human knowledge, because human knowledge in general has to do with objects, their relations, and mappings.
There are a couple more things that a category should have, and I’ll describe them in a moment, but first it’s good to introduce category of finite sets and some notation that will be helpful for visualization.
Category of finite sets, internal and external diagrams
In the category of finite sets objects are finite sets and maps are rules how to go from a value in one set to a value in another set. Due to how our brain works, it’s much easier to reason about collections of values and their mappings, than about abstract categories. We will be using the category of finite sets to explain most concepts here, and to visualize them, we will draw pictures of the sets and maps between them.
The set
where a dot represents each element. We can also leave off the labels if they are irrelevant to discussion. Such picture, labelled or not, is called internal diagram of the set.
We can picture a map as collection of arrows that go from elements of one set to element of another set:
There are also external diagrams for the cases when we do not care about concrete elements of objects:
Endomaps and identity maps
A map in which the domain and codomain are the same object is called an endomap (“endo”, a prefix from Greek ἔνδον endon meaning “within, inner, absorbing, or containing” Wikipedia says). For endomaps we have a special form of internal diagram:
It turns out that in every category, for each object, we have a map that
maps elements of an object
The
Definition: An endomap
Composition
The final, fourth (after objects, maps, and identity maps) thing that a category should have (or support) is the ability to compose maps. That’s where all the fun begins.
Composition of two maps
In a more familiar notation:
That equation also explains why composition “works” from right to left (with
respect to the
Once we have the
Not only the composition of maps should be possible, but it should satisfy these laws so objects and maps “fit together nicely”:
-
The identity laws:
and
-
The associative law:
These rules make composition of maps work similarly to multiplication of numbers. The identity laws ensure that identity maps work indeed like number 1, so we can easily remove (or add) them without changing anything. We will use that trick a lot. The associative law allows us to move parenthesis. The analogy between multiplication and composition does not extend too far though, because we cannot generally swap order of maps in composition, since their inputs and outputs are sort of “typed” by domain and codomain objects.
Isomorphisms
One of simplest and ubiquitous things in category theory is isomorphism.
A map
What does
Isomorphisms are cool. They allow to move freely from one representation of object to another. For example, Cartesian system of coordinates is based on the idea that a pair of numbers is isomorphic to a point on plane, then you work from that.
There are a few properties of isomophisms that come directly from the associative and identity laws of maps:
-
Reflexive:
is isomorphic to (follows from the existence of identity maps). -
Symmetric: if
is isomorphic to , then is isomorphic to . This simply follows from the definition of isomorphism. -
Transitive if
is isomorphic to , and is isomorphic to , then is isomorphic to (see the proof below).
Notation: if
Let’s prove the transitive property now as an exercise. We are given that:
In order to show that
To go back from
This makes use of identity laws and associative law we discussed previously. The second equation can be proved the same way.
If
-
If
, then . -
If
, then .
Let prove the first one. We assume that
Sections and retractions
Let’s give names to some special relations of maps that will be very useful
to us later. If
-
a retraction for
is a map for which ; -
a section for
is a map for which .
The first thing to note is that we cannot say that some map
Useful mnemonics for retraction is that it retracts values “back from where they come”. While the name “section” is a little trickier.
We can think of a section
This picture also shows the important idea that in order for
On the other hand, for
Monomorphism and epimorphism
Suppose a map
Proof: Looking at the definition, we see that the assumption means that
we have a map
Definitions: A map
If
What does all this stuff mean anyway? Simply put, if you can “cancel”
For example, when GHC gets into a situation when it has only result of type-level function application, but it needs to figure out what argument of that function was, it complains that the type-level function may be not injective. Fair enough! (In GHC 8.0, there is a way to annotate type-level functions telling that they are injective.)
Remember that if
-
If
, then .
And if
-
If
, then .
(We talked about
Suppose a map
Definition: A map
What happens here? Now we apply
Composing sections and retractions
Now we are going to consider two really simple propositions.
Proposition: If
Proof: Let
Using the familiar tricks:
This proves that
Proving that the composite of two maps each having sections, has itself a section is left as an exercise for the reader.
Theorem of uniqueness of inverses
Theorem (uniqueness of inverses): If
Proof: From the definition we have, if
Then by identity and associative law
Another definition of isomorphism, automorphism
Using the notions of “section” and “retraction” we can rephrase the definition of “isomorphism”.
Definitions: A map
Such a map
Definition: A map that is an endomap and at the same time an isomorphism is usually called by the one word automorphism.