[FOM] Mirror versus opposite in categories

[Lengyel, Florian]

Certain apparently overlooked type errors recur in the literature on
categories. Sorting 
this out requires distinct notation for certain notions (even Mac Lane
conflates what I 
claim can be considered a natural transformation and a functor,
respectively: 
the opposite and the mirror functor [CWM, 2nd ed., page 33]). Sorting this
out seems to 
lead to foundational trouble: an infinite egress of ever larger
meta-categories. 
There always seems to be an adjunction, using a functor and (implicitly) a
natural transformation used to express all other adjunctions, which can only
be expressed 
at the next higher level of "meta-categories". I will attempt to be more
specific.


In definitions of adjoint relations between functors (and categories), 
authors such as Higgins, Lambek and Scott, Herrlich and Strecher, and
McLarty 
(in an exercise), write, given functors F:A->B and U:B->A, 
that F -| U (F is left-adjoint to U) if there is a natural isomorphism 
B(F(-),-) ->A(-,U(-)). 

This has a type error: the domain of B(-,-) is B^op x B, but F has codomain
B, 
not B^op [Lambek and Scott refer to an "adjointness" between categories, not

functors, but the same type error is present]. Writing B(F(-), -) by
defining 
what it does to objects and morphisms has the effect of silently introducing

a new notation, since it isn't a valid composition. Perhaps one could be
more explicit.
 
On page 33 of CWM, second edition, Mac Lane defines the opposite category. 
Further along that page, the same notation for the opposite arrow is used
for what 
I will call, in an attempt to be more precise, the mirror functor: 
 
if F:A->B is a functor, then the "mirror" of F, F^op:A^op->B^op, is  given
by  F^op(g^op)=(F(f^op))^op. 

But I claim this conflates what can be considered a natural transformation
and 
a functor, appropriately defined; to sort out what to do with the type
error, 
it will help to keep them separate.
 
Suppose that F is an arrow in Cat, the category of small categories. Then
one would 
think that F^op would denote the arrow F^op:B->A in Cat^op, not an arrow
A^op -> B^op. 
Let's use the notation F* for the mirror functor; further, let's adopt the
convention 
that arrows of opposite categories will always be denoted with an explicit
op. 
So F*(g^op) = (F(g))^op. I've been accused of dyslexia on account of wanting
to be 
explicit about opposite arrows, but I believe there is more going on than an
inability 
to distinguish left from right. A less ad hominem attitude to adopt is that
we want our notation 
to do more of the work.
 
This would mean that the adjunction F -| U above would be properly
written as a natural isomorphism B(F*(-),-) ->A(-,U(-)). There is the
question of whether * and op are "only notation," or whether these refer to
operations on some large ambient category. 

To get rid of the * everywhere, I can introduce what I call the mirror
convention, but 
to do this I will consider what might happen if op and * were admitted as
operations 
with some definite domain. I need a large enough ambient category to do
naive category 
theory on which these operations make sense; I will include * and op as
operations in the "signature" of my naive category theory, rather than just
free-floating syntax that can be freely applied to any category or any
functor. Mac Lane suggests that "op" can be freely 
applied to any category. Are there formalizations of category theory in
which these operations
are formally defined? 
 

Let CAT± denote the meta-category of categories and co- and contra- variant
functors (if 
this is too big, substitute the category Cat± of small categories for CAT±).
Then 
the mirror involution * can be thought of as a "meta-"functor *:CAT±
-> CAT±, and one has a "meta-" natural transformation op:1_CAT± -> * from
the identity on CAT± to the mirror involution *. Its components are
contravariant functors op_A :A ->A^op. This is the 
reason we need to include contravariant functors in CAT±: the components of
op cannot be eliminated following the usual procedure of rewriting a
contravariant functor A ->B as a covariant functor A^op ->B, since this
implicitly uses the component op_A. We need an 
arrow of type A -> A^op, not some other type, despite the often heard
suggestion that 
a contravariant functor A -> B is "the same thing" as a covariant functor
A^op -> B.

So, the meta-category CAT± comes equipped with two operations, * and op,
related 
as follows: 

op is a natural transformation: given a functor F:A->B and an arrow g of A,
op_B(F(g)) = F(op_A(g)). This will motivate a notational convention to get
rid 
of the *'s in the above adjunctions. But it will mean that I have to be
explicit 
about showing opposite arrows as such.
 
Now I can state the mirror convention, by which the same name is used to
denote 
a functor and its mirror.

a) explicitly write arrows of opposite categories. There is a point to
this!  
There seems to be a type error, related to the common error occurring in
some 
statements of adjunctions, in published definitions of the hom functor 
A(-,-):A*xA->Set (for a locally small category A).  Some authors, including
Higgins 
and Lambek and Scott, write an equation related to the type error in the
statement of adjointness relations: A(f,h)(g) = hgf, in which f means both f
and the opposite of f. 
One should write A(op(f),h)(g) = hgf (at least for now). 
 
b) Given categories A and B in CAT± and a functor F:A->B, I abuse notation
by writing F(op(g)) = op(F(g)).
(End of mirror convention)
 
Now, we have operations "*" and "op" on CAT±, which enable one to express
any 
adjunction between functors of CAT± as a natural isomorphism between
hom-classes, 
and a syntactical convention to express this more or less the way category
theorists 
write it, without type errors. 
 
However, there are still apparently "natural" adjunctions that cannot be
expressed: 
it seems "clear" that the mirror functor * is self-adjoint: * -| *. Writing
this seems to require "defining" a meta-meta category meta-CAT±, which
contains CAT± and CAT±^op (we need both!) along with a meta-* and a meta-op.
If we avoid hom-classes, we still need meta-CAT± in which to define the
meta-unit and meta-counit of the meta-adjunction * -| *. 
 
An argument of Steve Simpson shows that there is no category containing an
isomorphic 
copy of every category, so an attempt to express some version of the
adjunction * -| * "internal" to CAT± by such a device cannot work...it seems
as though there is an 
endless egress of meta-categories...

Any comments and criticism would be appreciated.

-FL