An adjoint equivalence is a more “coherent” or “structured” notion of equivalence, in which the 2-isomorphisms relating composites to identities are required to satisfy coherence laws (the zigzag identities for an adjunction).
We work in any 2-category. First, we observe:
If is an adjoint equivalence, then so is .
Therefore, in an adjoint equivalence, each functor is both the left and the right adjoint of the other (i.e. it is an ambidextrous adjunction).
The definition as given above is also redundant:
If is any equivalence, then it satisfies one zigzag identity iff it satisfies the other.
Using string diagram notation, with strings progressing up the page and 1-morphisms progressing from left to right, we can draw the data of an equivalence (omitting labels for the regions denoting objects) as follows:
If we now suppose that one zigzag identity holds:
then we can verify the other as follows. (The first step uses the inverse of the first zigzag identity.)
Furthermore, although an adjoint equivalence is a “stronger” or “more structured” notion than a mere equivalence, the property of “being adjoint equivalent” is no stronger a condition than “being equivalent,” since every equivalence may be refined to an adjoint equivalence by modifying one of the natural isomorphisms involved. More specifically:
If is a morphism which is an equivalence, then given any morphism and any isomorphism , there exists a unique 2-isomorphism such that is an adjoint equivalence.
Since is an equivalence, there exists a and isomorphisms and . However, we also have , so the isomorphism also induces an isomorphism , which we denote . Now and may not satisfy the zigzag identities, but if we define as follows:
then we can verify, using string diagram notation as above, that satisfies one zigzag identity, and hence (by the previous lemma) also the other:
Finally, if is any other isomorphism satisfying the zigzag identities with , then we have
using the interchange law and two zigzag identities. This shows uniqueness.
In Categories Work, IV.4, there is a different proof of the weaker fact that if a functor is part of an equivalence, then it is part of an adjoint equivalence. This proof is given in Cat, but can be applied representably to any 2-category.
Since adjoints are unique up to unique isomorphism when they exist, it follows that any adjunction involving one functor which is an equivalence must be an adjoint equivalence. Therefore, for a fixed morphism , the “category of adjoint equivalence data ” is either empty (if is not an equivalence) or equivalent to the terminal category (if is an equivalence). In other words, it is a (-1)-category.
Therefore, in any 2-category, the following data are all equivalent (i.e. form equivalent categories):
A morphism with the property of being an equivalence.
A morphism with the structure of a morphism and an isomorphism , together with the property that there exists an isomorphism .
A morphism together with the structure of adjoint equivalence data .
In other words, adjoint equivalences are the way to make the property of “being an equivalence” completely into “algebraic” structure. However, they are not equivalent to the category of the following data:
One instance of the usefulness of adjoint equivalences is that the “walking adjoint equivalence” 2-category is equivalent to the point. Thus, it can be used as an interval object in , and in fact it is one of the generating cofibrations for the canonical (Lack) model structure on . This is not true of the “walking non-adjoint equivalence.”
The original definition of tricategory by Gordon-Power-Street involved coherence 2-morphisms with the property of being equivalences in the relevant hom-bicategories. This is fine for most purposes, but for others it is insufficient, such as the following.
Since “being an equivalence” is not algebraic structure, the GPS definition of tricategory, taken literally, is not an algebraic structure. In particular, it is not monadic over 3-globular sets, nor is it the algebras for a globular operad. Such monadicity is important if one wants to state coherence theorems as properties of free structures.
The definition of 3-functors and higher transfors between tricategories include data and axioms that involve composites incorporating not just the coherence equivalences, but their pseudo-inverses. Therefore, strictly speaking these definitions are not well-defined unless the definition of tricategory comes with chosen pseudo-inverses for these coherence equivalences—in which case one should certainly also choose full adjoint equivalence data in order that the space of choices be contractible.
These problems are, of course, easy to remedy by simply requiring adjoint equivalence data rather than merely single equivalence morphisms. This change was first written down by Gurski.
where the top arrow on the right side is (composition, reversed composition) and the bottom arrow factors through . One can then prove that the maps and are monic, so that can be regarded either as “the object of maps which are isomorphisms” or “the object of maps which are isomorphisms” (or, as is most evident from its construction, “the object of pairs of maps and which are inverse isomorphisms”).
In a cartesian closed 2-category?, however, the analogous “2-equalizer” , does not have similar properties: the projections and will not in general be fully faithful. Thus, we can only regard as “the object of not-necessarily-adjoint equivalence data .” However, if we use a further equifier to construct its “subobject of adjoint equivalence data” , then the projections and will be fully faithful, so that can also be regarded as “the object of maps which are equivalences” and dually.
In higher category theory, one expects to have a similar “fully coherent” notion of “adjoint equivalence” in any n-category or infinity-category, and one hopes to prove a similar theorem that any equivalence can be refined to an adjoint equivalence. This is known to be true at least in the following cases:
For tricategories, the corresponding statement can be deduced from the Gray-categorical version using the coherence theorem for tricategories. A direct proof can also be found in Nick Gurski’s paper Biequivalences in tricategories.