[Math] What does functor definition in category theory mean

category-theory

According to Wikipedia:

Let C and D be categories. A functor F from C to D is a mapping that

  • associates to each object $X$ in C an object $F(X)$ in D,
  • associates to each morphism $f : X \rightarrow Y$ in C a morphism $F(f) : F(X) \rightarrow F(Y)$ in D such that the following two conditions hold:
    • $F(id_X) = id_{F(X)}$ for every object $X$ in C
    • $F(g \circ f)$ = $F(g) \circ F(f)$ for all morphisms $f : X \rightarrow Y$ and $g : Y \rightarrow Z$ in C.

That is, functors must preserve identity morphisms and composition of morphisms.

Maybe this is because of my programming background, but it's not clear what is $F$ in this definition. It looks like a function, but it always takes different arguments: $F(X)$ – object, $F(f)$ – morphism.

It looks like a very smart function that accepts all kinds of arguments and knows what to return in each case.

Moreover, in this book there is one more equation that makes thing even more complicated:

$$F(f : X \rightarrow Y) = F(f) : F(X) \rightarrow F(Y)$$

Does it mean that if we pass a function $f : X \rightarrow Y$ to $F$, we will get a function $F(f) : F(X) \rightarrow F(Y)$?

Also, shall $F$ mentioned here: $F(f : X \rightarrow Y)$
and here:
$F(X)$
to be two different functions with different signatures and behavior?

Best Answer

You're right, $F$ really is two functions. If you were being very formal, you might say a functor $F : \mathcal{C} \to \mathcal{D}$ is a pair $F=(F_0, F_1)$, where $F_0 : \mathrm{ob}(\mathcal{C}) \to \mathrm{ob}(\mathcal{D})$ and $F_1 : \mathrm{mor}(\mathcal{C}) \to \mathrm{mor}(\mathcal{D})$ are functions satsifying

  • If $f : X \to Y$ in $\mathcal{C}$, then $F_1(f) : F_0(X) \to F_0(Y)$ in $\mathcal{D}$;
  • $F_1(\mathrm{id}_X) = \mathrm{id}_{F_0(X)}$ for all $X \in \mathrm{ob}(\mathcal{C})$; and
  • $F_1(g \circ f) = F_1(g) \circ F_1(f)$ for all $X \xrightarrow{f} Y \xrightarrow{g} Z$ in $\mathcal{C}$.

There are various encoding tricks you could use to completely remove ambiguity, but in day-to-day life there is no problem with just writing $F$ to denote both $F_0$ and $F_1$. But when using a proof assistant, say, the distinction has to be made.

Related Question