Prologue.

This(These) note(s) mainly work(s) as a dairy on my own study of Category Theory, 2nd Edition (by Steve Awodey). As a CS student who is only familiar with Coq and $1^{st}$ and $2^{nd}$ year university Math, it can be very hard, in a very surprising way. Hope this note can help those who are also struggling with the abstract nonesense.

I will suggest three books, Awodey, Category theory for computing science [Barr and Well] and Basic Category Theory for Computer Scientist [BCP]. The last one is a good quick introduction; the first two are both good as references.

Category, homomorphism, Functor

The formal definition of a category, which you can find almost anywhere, is about objects and arrows. Awodey means, a category is a formalization (in graph-favour) with underlying meaning. When he says Set category, those objects stand for sets and those arrows stands for functions.

Note, I will use bold font like Set to stands for the category.

(recall def of a function: for each element in the domain, there exists an element in the codomain to correspond, thus codomain cannot be empty)

Trivially, this means every category always has a meaning with it, which will bring challenges for me in the understanding of the section Construction in Category (also the hardest part in Chp.1).

Where in a category, the objects are always refering to the mathematical objects with a certain fixed mathematical structure, the arrows are refering to the mapping between some two objects and thusly preserve the structure. (Since the two objects in the category has a certain fixed structure ). This “structure-preserving mapping” is called homomorphism, which justifies the notation $Hom(X,Y)$ which means the collection of the arrows between objects $X,Y$, since in the most cases the arrows are always a kind of homomorphism.$^?$

With the definition, we can easily have the concept of the category of category: the objects of ${C}$ are categories, then what are the ‘structure-preserving’ mapping? Functor ! Then it is clear why Functor is defined in that way, it is just structure preserving.

Isomorphism

Let’s first see the definition of isomorphism inside Category Theory. An isomorphism of two object $A,B$ is just an arrow $f:A \rightarrow B$ (not necessary function, we are talking about category theory), where there is another arrow $f’ : B \rightarrow A$ s.t. $f \circ f’ = id_B, f’ \circ f = id_A$. This definition is quite simple, familiar (because it directly correspond the bijection in Set) but powerful. This stands for the “equality” in the language of category theory. It is claimed$^?$ with only the language of the category theory (arrows and objects), you cannot detect the distinction between two isomorphic objects.

As a side note, the only definition of equality I know is “Lebnize Equality” (two things are equal if one of the two satisfies any property the other satisfies). This is so strong and universal because this definition ranges through all possible theories that existed and will exist.

Now we have the idea of “equality”, we can start to define things! What I actually mean is it is possible to define things unique up to isomorphism. The things we refer to will be “unique”.

Before proceeding to the first example (that makes a definition) , (denoted as UMP in Awodey), I have to reiterate the idea of “underlying” things.

Underlying Structure, 1

Underlying structure is just underlying structure. For example, a monoid’s underlying structure is just a set that containing all the elements of the monoid. (Though I think it is only one of the possible underlying structure.)$^?$ We usually use $\vert X \vert$ or $U(X)$ to denote the underlying structure of $X$. If you see closely, $U(\cdot)$ is a functor.

The set forgets about the property (the structure) that the monoid has: the associativity of the binary operation and the unit for the operation. However, this “forget” is very ambiguious… Because you will see that, even when a monoid forgets about the property (the structure), the elements in the set still have the above two properties. Because the property is about the binary operation (not the elements). The operation is phrased (like a constraint) in the language out of category theory. So why the concept of “underlying structure” makes a difference? I can give you an example. In the Monoid category, take any two objects $M, N$, $Hom(M,N)$ is a bunch of homomorphism while $Hom( \vert M \vert , \vert N \vert )$ is a bunch of functions! where that collection of function include a lot of functions that don’t have to be a homomorphism. Here you can see a implicit ‘context-switching’ that is important while not even emphasized in Awodey.

It still seems like it is not a big deal. Now we can see an example where this context-switching becomes important.

Epis, Monos

Epis and Monos (in category theory) seem like just the corresponding concept of surjection and injection (in set theory). Just evverything is pharsed in the arrow language. It makes these two concepts easy to remember.

$f: A \rightarrow B$ is a monomorphism iff for arbitrary $x, y : C \rightarrow A$, $f\circ x = f\circ y \Rightarrow x = y$.

Now in Awodey, he wants to prove that monoid monomorphism are just injective monoid homomorphism. Injection is the concept of set theory, that means this proposition is going between Set category and Monoid category. Non-trivially, you cannot directly prove this by the definition of Monos.

From right to left, you can. Since any injective monoid homomorphism, say $f:A \rightarrow B$, $\vert f \vert$is a mono in Set, and then we take arbitrary $C \in$ Monoid and $x,y : C \rightarrow A$, thus $\vert x \vert, \vert y \vert : \vert C \vert \rightarrow \vert A \vert$ are also arrows in Set, thus

$f \circ x = f \circ y$

$\Leftrightarrow_\text{they are all just functions} \vert f \vert \circ \vert x \vert = \vert f \vert \circ \vert y \vert$

$\Rightarrow_\text{assumption of mono in category Set} \vert x \vert = \vert y \vert \Leftrightarrow x = y$.

But this cannot work from left to right, because in the definition we “quantify” through the arrows and there is the implict context switching (since this proposition goes between two categories). More concretely, if you only know an arrow $f :A \rightarrow B$ is a monoid monomorphism, you cannot prove $\vert f \vert$ is mono in Set since there will be tones of arrows in Set that are not even monoid homomorphism and will not be an arrow in Monoid and even mentioned in the definition of monos of $f$. Even more concretely, if you want to prove directly, let $x_s, y_s : \vert C\vert \rightarrow \vert A \vert$ be arbitrary, then you need to find the corresponding arrows of $x_s, y_s$ in $Hom(C,A)$, which may not even exist.

I will not show how to actually prove it since repeating a proof from the textbook Awodey is a waste of time. But I will go through the uniqueness of UMP to get familar with informal reasoning via commutative diagrams.