[FOM] Re: Mirror versus opposite in categories
cxm7 at po.cwru.edu
Tue Nov 25 14:00:12 EST 2003
I am glad to see Florian Lengyel apply such vigorous thought to the
presentation of category theory, and perhaps he has the right idea for
strictly typed presentations. His main points, though, seem to me to rest
on specific conventions which are not the only ones possible.
He claims that the categorial idea of a dual can only be explained by
>an infinite egress of ever larger
This is true for one pattern of explanation: that is if you take
dualization as a functor defined on a meta-category of categories (taking
each one of them to its dual), and so as an arrow in the next higher
meta-category. Since the next higher also has duals, we need a functor
defined on it, and so on.
To my mind, that is a good pattern of explanation, and we should feel free
to posit those meta-categories as far as we like. But it is not the only
possible pattern. The weakest one would merely take dualization as a
operator on the category of categories, and not a functor, and thus would
take not one step to any higher meta-cat. Of course we would all know this
operator is functorial, just like we all know there is a class of all
ordinals, but our theory could refuse to formalize that, just as ZF refuses
to name proper classes.
Also Florian Lengyel believes there is a type error in several books on
category theory. He writes:
>given functors F:A->B and U:B->A,
>F -| U (F is left-adjoint to U) if there is a natural isomorphism
>This has a type error: the domain of B(-,-) is B^op x B, but F has codomain
>B, not B^op
But the books are strictly correct on one natural convention: We say each
term (name of an object or arrow) has a category as type, and when a term
of type B occurs as the first argument in a hom term it is construed as
having type B^op. So the term F(-) has type B and when it occurs in
B(F(-),-) it is construed as having type B^op. This is just like any
computer language that construes integer terms as real terms when they
occur in arithmetic expressions along with real terms.
This typing convention relies on the fact that the objects and arrows of
B^op are by definition the objects and arrows of B. So there is no
ambiguity about the referent of a term---just as there is no ambiguity
about how to construe an integer as a real number.
Yet Florian Lengyel's way of typing has advantages for some purposes.
More information about the FOM