Category theory Notes 1

What is category theory all about

Category theory is all about structures and relations.

... category theory is the mathematical study of (abstract) algebras of functions. —— Category Theory by Steve Awodey

For me, learning category theory enables me to understand what on earth is "a monoid in the category of endofunctors", and it helps me to learn HoTT.

Function of Sets

Nothing too much to say here, only some notations here.

Identity function in the books I am using (primary Category Theory by Steve Awodey, but I'm also referring to Beginning Category Theory by Peter Smith) is written as

$$ 1_A : A \rightarrow A $$

Definition of Category

Basically, a category is anything which

• Contains objects and arrows (you can consider arrows as something like functions since it makes it simpler, but they don't have to be functions actually) between them
• The arrows can composite with each other and obey the associativity rule
• For each object, there exists an identity arrow, which is also the "unit" arrow when compositing with other arrows.

In Agda, simplified:

record Category (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where
  field
    Obj : Set o
    _⇒_ : Rel Obj ℓ
    _≈_ : ∀ {A B} → Rel (A ⇒ B) e

    id  : ∀ {A} → (A ⇒ A)
    _∘_ : ∀ {A B C} → (B ⇒ C) → (A ⇒ B) → (A ⇒ C)
    assoc     : ∀ {A B C D} {f : A ⇒ B} {g : B ⇒ C} {h : C ⇒ D} → (h ∘ g) ∘ f ≈ h ∘ (g ∘ f)
    identityˡ : ∀ {A B} {f : A ⇒ B} → id ∘ f ≈ f
    identityʳ : ∀ {A B} {f : A ⇒ B} → f ∘ id ≈ f

Examples

The book gives us some examples of categories, I'll just take some interesting ones here

Rel

Object: Sets

Arrows : Binary Relations ($f : A → B$, $f ⊆ A×B$)

Identity Arrow : $$ 1_A = {(a,a) ∈ A×A | a∈A} ⊆ A×A $$

We need to prove $f ◦ 1_A = f = 1_B ◦ f$, which is easy to do by introducing $(a,b) \in f ◦ 1_A$ so there must exists a $p$, and $(a, p) \in 1_A$ ,$(p, b) \in f$, since $1_A$ is by definition $(a,a)$, so $p$ is $a$, so $(a,b) \in f$. Proof of $f = 1_B ◦ f$ is similar.¹

Composite of Arrows: function composition, obvious We need to prove $f ◦ (g ◦ h) = (f ◦ g) ◦ h$.

This proof is easy, just assume $(a,b)$, $(b,c)$, $(c,d)$ and apply the definition of composite will lead us to the result.

You can find the definition of Rels category in Agda.

Partially ordered set (Poset)

Object: element in the set

Arrows : $\leq$

Identity Arrow : $a \leq a$

Composite of Arrows : $a \leq b\ \ and\ \ b \leq c \Rightarrow a \leq c$

Category can be considered as a kind of generalized poset with more structure than just $p \leq q$. And functor can be regarded as a generalized monotone map.

Poset category in Agda

Monoid

A monoid is a category with only one object, and the arrows are the monoid's elements. The identity arrow is the unit element, and the composite of arrows is the monoid's operation.

For any object $C$ in any category $\textbf{C}$, the set of arrows from $C$ to $C$, written as $Hom_{\textbf{C}}(C,C)$, is a monoid under the composition operation of $\textbf{C}$

Monoids are structured sets, there is a category $\textbf{Mon}$ whose objects are monoids and arrows are functions that preserve the monoid structure.

A homomorphism from $M$ to $N$ is the same thing as a functor from "$M$ as category" to "$N$ as category", so:

Category can be considered as a kind of generalized monoid. And functor can be regarded as a generalized homomorphism.

Free category

The free category on a “set of arrows”, hence on a directed graph, is the category whose morphisms are the tuples of composable arrows, hence the morphisms freely generated from these arrows. These morphisms may also be thought of as the “paths” that one may trace out in the directed graph by traversing in each step along an arrow, and therefore free categories are also called path categories. ——— nLab

With any directed graph, we can make it a category by adding more arrows:

• For each node, add an identity arrow
• For any two composable arrows, add the composite result arrow

Then this category is called the free category generated by the directed graph.

Isomorphism

In a category, an arrow can be called an isomorphism if it has an inverse.

If there exists an isomorphism between object $A$ and $B$ in category $C$, we say $A$ is isomorphic to $B$, and write $A \cong B$.

Intuitively we can think isomorphism is a way to say that two objects are "similar".

Large/Small Category

A category is small if it has a small set of objects and a small set of morphisms. —— nLab

Where a small set is really a set instead of a proper class².

A category is said to be locally small if each of its hom-sets is a small set. —— nLab

And large categories are those which are not small.