What is the formal definition of a dual category?

Solution 1:

The point is that source and target of morphisms aren't an intrinsic property of the morphisms themselves, but are more like a property of the category.

In general you can see the same element of a set as a morphism for two different categories and this morphism can have different source and target in these categories. When you say that $\hom_{\mathbf A^\text{op}}(A,B)=\hom_\mathbf{A}(B,A)$, you're building up a new category in which the morphisms are the same elements/morphisms of $\mathbf C$ but in this new category you see these morphisms with reversed direction.

If you prefer you can think of the opposite category of category $\mathbf C$ as a new category such that for each morphism $f \colon A \to B$ in $\mathbf C$ there exists a unique $f^\text{op} \colon B \to A$ in $\mathbf C$ and such that the composition is such that $g^\text{op} \circ f^\text{op}=(f \circ g)^\text{op}$, where the composition on the left is the one in the opposite category, while the one on the right is that of the category $\mathbf C$. In this way you have defined the opposite category $\mathbf C^\text{op}$ up to isomorphism, thus you can think of the definition that you gave as a model, i.e. a concrete representation, of the opposite category.

Hope this can help.

Solution 2:

I think MacLane's "Categories for the working mathematician" says it better than your book:

"To each category $\cal{C}$ we also associate the opposite category $\cal{C}^{op}$. The objects of $\cal{C}^{op}$ are the objects of $\cal{C}$, the arrows of $\cal{C}^{op}$ are arrows $f^{op}$ in one-one correspondence $f \mapsto f^{op}$ with the arrows $f$ of $\cal{C}$. For each arrow $f: a \longrightarrow b$ of $\cal{C}$, the domain and codomain of the corresponding arrow $f^{op}$ are as in $f^{op}: b \longrightarrow a$ (the direction reversed). The composite $f^{op}g^{op} = (gf)^{op}$ is defined in $\cal{C}^{op}$ exactly when the composite $gf$ is defined in $\cal{C}$.