Kerodon

Proof. Let $g: D \rightarrow C$ be a homotopy inverse to $f$, so that there exists an isomorphism $\eta : \operatorname{id}_{C} \xRightarrow {\sim } g \circ f$ in the category $\underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(C,C)$. It follows from Proposition 6.1.4.1 that $\eta $ is the unit of an adjunction, and therefore exhibits $g$ as a right adjoint to $f$. A similar argument shows that $g$ is left adjoint to $f$. $\square$

Proof. The implication $(3) \Rightarrow (1)$ and $(3) \Rightarrow (2)$ are immediate from the definitions, and the reverse implications follow by applying Proposition 6.1.4.1 to $\operatorname{\mathcal{C}}$ and the conjugate $2$-category $\operatorname{\mathcal{C}}^{\operatorname{c}}$. $\square$

Proof. Since postcomposition with $g$ induces a fully faithful functor

there is a unique $2$-morphism $\epsilon : f \circ g \Rightarrow \operatorname{id}_{D}$ for which the horizontal composition $\operatorname{id}_{g} \circ \epsilon $ is equal to the composite map

Moreover, $\epsilon $ is an isomorphism and the pair $(\eta , \epsilon )$ automatically satisfies condition $(Z2)$ of Definition 6.1.1.1. Let $\beta $ denote the composition

Since $\epsilon $ and $\operatorname{id}_{f} \circ \eta $ are isomorphisms, it follows that $\beta $ is an isomorphism. Applying Corollary 6.1.2.8, we see that $\beta ^2 = \beta $, so that $\beta = \operatorname{id}_ f$. $\square$

Proof of Proposition 6.1.4.1. Let $\operatorname{\mathcal{C}}$ be a $2$-category, let $f: C \rightarrow D$ and $g: D \rightarrow C$ be $1$-morphisms in $\operatorname{\mathcal{C}}$, and assume that $g$ is an isomorphism (the case where $f$ is an isomorphism can be treated by applying a similar argument in the opposite $2$-category $\operatorname{\mathcal{C}}^{\operatorname{op}}$). Suppose first that $\eta : \operatorname{id}_{C} \Rightarrow g \circ f$ is an isomorphism in the category $\underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(C,C)$. It follows that the horizontal compositions

are isomorphisms in $\underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(C,D)$ and $\underline{\operatorname{Hom}}_{\operatorname{\mathcal{D}}}(D,C)$, respectively. For each object $T \in \operatorname{\mathcal{C}}$, our assumption that $g$ is an isomorphism guarantees that the composition functor $\underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}( T, D) \xrightarrow { g \circ } \underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(T,C)$ is an equivalence of categories, and therefore fully faithful. Invoking the criterion of Proposition 6.1.4.7, we conclude that $\eta $ is the unit of an adjunction.

We now prove the converse. Suppose that the $2$-morphism $\eta : \operatorname{id}_{C} \Rightarrow g \circ f$ is the unit of an adjunction. Our assumption that $g$ is an isomorphism guarantees that we can choose a $1$-morphism $f': C \rightarrow D$ and an isomorphism $\eta ': \operatorname{id}_{C} \xRightarrow {\sim } g \circ f'$ in the category $\underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(C,C)$. It follows from the first part of the proof that $\eta '$ is the unit of an adjunction. Applying Corollary 6.1.3.7, we deduce that there is a unique isomorphism $\beta : f \xRightarrow {\sim } f'$ for which $\eta '$ is equal to the composition

Since $\eta '$ and $(\operatorname{id}_ g \circ \beta )$ are isomorphisms in the category $\underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(C,C)$, it follows that $\eta $ is also an isomorphism. $\square$

Proof. We first show that $(1)$ and $(1')$ are equivalent. If $\epsilon $ is an isomorphism, then $f \circ g$ is isomorphic to $\operatorname{id}_{D}$ (as an object of the category $\underline{\operatorname{Hom}}_{\operatorname{\mathcal{D}}}(D,D)$) and is therefore an isomorphism of $\operatorname{\mathcal{C}}$ (Remark 2.2.8.23). Conversely, suppose that $f \circ g$ is an isomorphism. Then it is invertible when viewed as an object of the monoidal category $\underline{\operatorname{End}}_{\operatorname{\mathcal{C}}}(D)$. Since $(\eta , \epsilon )$ is an adjunction, we can regard $f \circ g$ as a coalgebra object of $\underline{\operatorname{End}}_{\operatorname{\mathcal{C}}}(D)$ with counit $\epsilon $ (see Remark ). Applying Proposition 2.1.5.23 (to the monoidal category $\underline{\operatorname{End}}_{\operatorname{\mathcal{C}}}(D)^{\operatorname{op}}$), we deduce that $\epsilon $ is an isomorphism.

We now show that $(1)$ implies $(2)$. Assume that $\epsilon : f \circ g \Rightarrow \operatorname{id}_{D}$ is an isomorphism. Axiom $(Z1)$ of Definition 6.1.1.1 guarantees that the composition

is equal to the identity $2$-morphism $\operatorname{id}_{f}$, which proves that the horizontal composition $\operatorname{id}_{f} \circ \eta $ is an isomorphism in $\underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(C,D)$. Similarly, it follows from axiom $(Z2)$ of Definition 6.1.1.1 that the horizontal composition $\eta \circ \operatorname{id}_{g}$ is an isomorphism in $\underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(D,C)$. For every $1$-morphism $d: T \rightarrow D$ in $\operatorname{\mathcal{C}}$, the map

is an isomorphism, so that $d$ belongs to the essential image of the functor $\underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(T,C) \xrightarrow { f \circ } \underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(T,D)$.

We now show that $(2)$ implies $(2')$. Let $d: T \rightarrow D$ be a $1$-morphism of $\operatorname{\mathcal{C}}$. If the functor $\underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(T,C) \xrightarrow { f \circ } \underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(T,D)$ is essentially surjective, then $d$ is isomorphic to $f \circ c$ for some $1$-morphism $c: T \rightarrow C$ of $\operatorname{\mathcal{C}}$. If $\operatorname{id}_{f} \circ \eta $ is an isomorphism, then the chain of isomorphisms

shows that $d$ belongs to the essential image of the composite functor

We next show that $(2')$ implies $(3)$. Fix an object $T \in \operatorname{\mathcal{C}}$ and a pair of $1$-morphisms $d,d': T \rightarrow D$; we wish to show that the composition map

is a bijection. By virtue of assumption $(2')$, we may assume that $d' = f \circ c$, where $c: T \rightarrow C$ is a $1$-morphism of the form $g \circ d''$. By virtue of Proposition 6.1.2.9, the composition

is a bijection. It will therefore suffice to show that the $2$-morphism $(\eta \circ \operatorname{id}_ c): \operatorname{id}_{C} \circ c \Rightarrow (g \circ f) \circ c$ is an isomorphism. This follows from assumption $(2')$, since $(\eta \circ \operatorname{id}_ c)$ can be rewritten as a composition

The implication $(3) \Rightarrow (3')$ is clear. We will complete the proof by showing that $(3')$ implies $(1)$. Assume that $(3')$ is satisfied; we wish to show that the $2$-morphism $\epsilon : f \circ g \Rightarrow \operatorname{id}_{D}$ is an isomorphism. To prove this, it will suffice to show that for every $1$-morphism $u: D \rightarrow D$, vertical precomposition with $\epsilon $ induces a bijection $\operatorname{Hom}_{ \underline{\operatorname{End}}_{\operatorname{\mathcal{C}}}(D)}( \operatorname{id}_ D, u ) \rightarrow \operatorname{Hom}_{ \underline{\operatorname{End}}_{\operatorname{\mathcal{C}}}(D)}( f \circ g, u )$. We now observe that this map fits into a commutative diagram

where the bottom horizontal map is induced by the right unit constraint $\rho _{g}: g \circ \operatorname{id}_ D \xRightarrow {\sim } g$, the right vertical map is given by the formation of right adjuncts with respect to $\eta $ (and is therefore bijective by virtue of Corollary 6.1.2.6), and the left vertical map is bijective by virtue of assumption $(3')$. $\square$