Defining Category of Adjunctions

adjoint-functorscategory-theorydefinitionhigher-category-theory

$\newcommand{A}{\mathcal{A}}
\newcommand{B}{\mathcal{B}}
\newcommand{C}{\mathcal{C}}
\newcommand{ADJ}{\mathsf{ADJ}}
\newcommand{id}{\mathrm{Id}}$Morphism between a pair of adjunctions $(F : \A \leftrightarrows \B : G)$ and
$(F' : \A' \leftrightarrows \B' : G')$ is a pair of functors $H : \A \to \A'$ and $F : \B \to \B'$ such that $FK = HF'$ and $GH = KG'$, and either

(I) $H(\eta_{(\cdot)}) = \eta_{H(\cdot)}' $, where $\eta$ and $\eta'$ are unit natural transforms corresponding to the adjunctions.

(II) $K(\epsilon_{(\cdot)}) = \epsilon'_{K(\cdot)}$, where $\epsilon$ and $\epsilon'$ are coint natural transforms corresponding to the adjunctions.

(III) for all $A \in \A, B \in \B,f : F(A) \to B$, it holds that $H(f^\top) = (Kf)^\top$, where by $(\cdot)^\top$ I denote transposition associated with both adjunctions.

Conditions (I),(II),(III) are equivalent as I proved in the exercise recently.

However it seems to me that, as adjunctions have morphisms, they should have their own category:

Consider category $\mathsf{ADJ}$ with objects being pairs of categories supplied each with an appropriate adjunction i. e. $(F : \A \leftrightarrows \B : G) \in \mathsf{ADJ}$ and morphism defined as above. Then, composition is defined by a pairwise functor composition, and identity is a pair of identity functors. Associativity of composition is easily seen from version (III) of definition.

So It seems that $\ADJ$ is a category. But in fact it is not as it contains itself in form $(\id : \ADJ \rightleftarrows \ADJ : \id) \in \ADJ$. Moreover every category $\C$ has a canonical representative $(\id : \C \rightleftarrows \C : \id) \in \ADJ$, which means that $\ADJ$ contains all categories in certain sense. Both of these are bas things for a set theoretical reasons, thus $\ADJ$ should not be defined as a category.

This situation is simillar to the idea of category of categories here so I see two pathways:

1) Restrict $\ADJ$ to small categories or locally small ones.
2) Define $\ADJ$ as a 2-category by introducing 'nutaral transfoms' as morphisms of morphims.

I personally prefer the latter solution.

Are categories of adjunctons used somewhere? If so, how are these categories defined?

P.S.

While writing this question I took liberty to define command \A -> $\mathcal{A}$, \B -> $\mathcal{B}$, \C -> $\mathcal{C}$, \ADJ -> $\mathsf{ADJ}$; \id ->$\mathrm{Id}$. You can use them in your answers and comments.

Best Answer

(note: I had misread the construction in the OP when writing this)

You can't get away from the size issues; an easy way to see definition 2 doesn't help is that you can extract from it the paradoxical 1-category simply by taking its 0 and 1-cells.

It is standard to define Adj on the same 'level' as Cat; e.g. given a cardinal $\kappa$, if you are working with the 2-category $\mathbf{Cat}_\kappa$ of $\kappa$-small categories, functors, and natural transformations, then you would normally take $\mathbf{Adj}_\kappa$ to be the 2-category of $\kappa$-small categories, adjunctions, and natural transformations. Or if you are working with Cat as a 1-category, then you do the same with Adj.

As Derek Elkins points out in comments, Cat isn't special here; given any 2-category $\mathcal{C}$ you can construct the 2-category of adjunctions in $\mathcal{C}$.

Related Question