(Note that we write compositions from left to right and accordingly apply most maps on the right.)
A functor is called a left adjoint to a functor if there is a bijection between the homsets:
natural in both and . In this case is called a right adjoint to , and we write .
A functor is called a left adjoint to a functor if there are natural transformations and satisfying the zig-zag identities:
So, why are these two definitions equivalent?
We start out from Def.2, as it generalizes to arbitrary bicategory or double category, which enable morphisms (‘transformations‘) between [parallel] arrows, depicted .
We will use the bicategory which has functors as arrows and natural transformations as transformations, and the bicategory which has profunctors as arrows. And we will pass them to Ehresmann’s double category construction.
In this generality one can already prove uniqueness of left/right adjoint for a given arrow and the following interchanging rules, which assert one-to-one correspondences between the below transformations, supposed :
(E.g. if given , we have , now we can use to obtain .)
Note that, both sides of the natural bijection in Def.1 are functors , i.e. are profunctors.
Specifically, they above are denoted by and , that is, for a single functor , we define
(In the terminology of heteromorphisms, we can get if we take a copy from each arrow in of the form and regard them as heteromorphisms .)
Importantly, it turns out that there is an adjunction in the bicategory .
The mappings and extend to two natural embeddings of the bicategory , whose arrows are the functors, into .
Note that is contravariant on arrows (reverses source/target and composition of functors) while is contravariant on the natural transformations.
To express these as covariant mappings, the notations and are introduced, for the bicategory obtained from by reversing arrows / transformations, respectively.
Using the interchange rules, we show below how to arrive to the embedding when starting out from , touching an embedding of double categories, , in the middle of the way:
A diagram of functors with induces and is determined by any of the following profunctor morphisms:
In a double category, transformations are supported by a pair of ‘vertical arrows‘ (regarding the original arrows as horizontal ones), and thus are depicted and also called as squares (or ‘cells’).
Horizontally adjacent squares, as well as horizontal arrows can be associatively composed horizontally, with units.
Vertically adjacent squares, as well as vertical arrows can be associatively composed vertically, with units.
The so called Ehresmann double category can be defined for any bicategory : all the arrows of are considered both vertical and horizontal in , with squares as transformations .
Now we are ready to define our embedding : its source is the double category , and its target is the double category , and flips horizontal arrows and composition.
So that . All objects (the categories) are fixed, a horizontal arrow (a functor ) is mapped to , while a vertical arrow (a functor ) is mapped to and a square is mapped to the corresponding square of . Compositions just work fine.
Adjunction in a double category is interpreted between a vertical and horizontal , in such a way that in for a bicategory translates readily to being left adjoint to in , according to Def.2.
If we flip horizontal arrows in a double category, adjunctions become companions:
A pair of horizontal and vertical arrows , are said to be a companion pair, if there exist squares as below
such that and (vertical composition) .
It is easy to see, that a companion in is just a pair of parallel isomorphic arrows in .
Since flips horizontal arrows, takes adjunctions to companions and companions to adjunctions.
Moreover, is surjective on squares.
Put it all together, we get that
two functors are naturally isomorphic if and only if there is an adjunction of profunctors . (This is basically one of the key observations above that .)
two functors are adjoint according to Def.2 if and only if we have an isomorphism of profunctors , i.e. Def.1 holds.
Remark. Actually, there are issues about formalizing Ehresmann’s construction for general bicategories.
When composition of arrows in a bicategory is strictly associative, we indeed get a (still strictly associative) double category . Otherwise, however, the resulting double category would be only weakly associative both horizontally and vertically, and such animals can only be defined by workarounds, e.g. using higher dimension categories with special collapses.
But don’t panic, we can still make things precise by introducing adequate maps from double categories to bicategories, so that would become such a map , with all its good properties, in particular taking companions to adjunctions and an adjunction to a pair of isomorphic arrows.