[FOM] dual of a category

[Vladimir Komendantsky]

> What is the relation between the dual  Cat^op  of the
> category of small categories  Cat, and the dual of a
> small category?

For the sake of what generality do you need Cat^op?!

The category Cat can be defined by purely axiomatic means, that is without set
theory. Therefore, the required relation can be demonstrated using elementary
theory of an abstract category (ETAC). ETAC consists of statements built from
atomic statements like "a in the domain of f", "b is the codomain of g", "i is
the identity arrow of a", "h is the composite of g with f", "a=b", and "f=g".
The non-atomic statements are built by means of ordinary logical connectives
(and, or, implies, iff) and the usual quantifiers ("for all a", "there exists
f", etc.).

The axioms of ETAC are certain sentences (i.e., statements with all variables
quantified).

To form the dual S^* of any statement S of ETAC replace throughout in S:
 - "domain" by "codomain"
 - "codomain" by "domain"
 - "h is the composite of g with f" by "h is the composite of f with g"
(hence, arrows and composites become reversed). Logic (connectives and
quantifiers) is unchanged.

We have the fairly common duality principle: If a statement S of the ETAC in
the consequence of the axioms, so is the dual statement S^*.

To define Cat^op in the axiomatic way, take the usual axioms of Cat (domain,
codomain, identity, associativity, and commutativity) and form their dual
statements. These dual statements axiomatize Cat^op.


> In fact, I'd like to know if it is possible to define
> the dual C^op of a small category C, using the dual of
> the category of small categories.

If T: C -> B is a functor, its object function "c |-> Tc" and its mapping
function f |-> Tf, rewritten as f^op |-> (Tf)^op, together define a functor
T^op: C^op -> B^op. The assignments C |-> C^op and T |-> T^op define a
*covariant* functor F: Cat -> Cat.

So, one doesn't really Cat^op to find C^op, since F above is covariant.


For more details:
 - Chapter II of Mac Lane's book,
 - an online book The Joy of Cats by Adamek et al.

Regards,
Vladimir