functor (Rev #6)

The concept if *functor* is the evident concept of homomorphisms between categories.

Let $A$ and $B$ be precategories. A **functor** $F : A \to B$ consists of

- A function $F_0 : A_0 \to B_0$
- For each $a,b:A$, a function $F_{a,b}:hom_A(a,b) \to hom_B(F a,F b)$, generally also denoted $F$.
- For each $a:A$, we have $F(1_a)=1_{F a}$.
- For each $a,b,c: A$ and $f:hom_A(a,b)$ amd $g:hom_A(b,c)$, we have

$F(g \circ f) = F g \circ F f$

By induction on identity, a functor also preserves $idtoiso$ (See precategory).

For functors $F:A\to B$ and $G:B \to C$, their composite $G \circ F : A \to C$ is given by

- The composite $(G_0 \circ F_0): A_0 \to C_0$
- For each $a,b:A$, the composite$(G_{F a, F b} \circ F_{a,b}):hom_A(a,b)\to hom_C(G F a, G F b)$

Composition of functors is associative $H(G F)=(H G)F$.

**Proof:** Since composition of functions is associative, this follows immediately for the actions on objects and on homs. And since hom-sets are sets, the rest of the data is automatic. $\square$

Lemma 9.2.9 is coherent, i.e. the following pentagon of equalities commutes:

$\array{
&& (K H)(G F)
\\
& \nearrow
&&
\searrow
\\
((K H) G) F
&& &&
K (H (G F))
\\
\downarrow
&& &&
\uparrow
\\
(K(H G)) F
&& \longrightarrow &&
K( (H G) F)
}$

Category theory natural transformation full functor faithful functor

category: category theory

Revision on September 7, 2018 at 06:45:38 by Urs Schreiber. See the history of this page for a list of all contributions to it.