Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$

Proposition 6.1.4.6. Let $\operatorname{\mathcal{C}}$ be a $2$-category, let $f: C \rightarrow D$ and $g: D \rightarrow C$ be $1$-morphisms of $\operatorname{\mathcal{C}}$, and let $\eta : \operatorname{id}_{\operatorname{\mathcal{C}}} \Rightarrow g \circ f$ be a $2$-morphism of $\operatorname{\mathcal{C}}$ which satisfies the following conditions:

  • The $2$-morphisms

    \[ (\operatorname{id}_{f} \circ \eta ): f \circ \operatorname{id}_{C} \Rightarrow f \circ (g \circ f) \quad \quad (\eta \circ \operatorname{id}_{g}): \operatorname{id}_{C} \circ g \Rightarrow (g \circ f) \circ g \]

    are isomorphisms.

  • For every object $T \in \operatorname{\mathcal{C}}$, the composition functor $\underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}( T, D) \xrightarrow { g \circ } \underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(T,C)$ is fully faithful.

Then $\eta $ is the unit of an adjunction $(\eta , \epsilon )$. Moreover, the counit map $\epsilon : f \circ g \Rightarrow \operatorname{id}_{D}$ is an isomorphism.

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

\[ \underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}( D, D ) \rightarrow \underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}( D, C ), \]

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

\[ g \circ (f \circ g) \xRightarrow {\alpha _{g,f,g} } (g \circ f) \circ g \xRightarrow { ( \eta \circ \operatorname{id}_ g)^{-1} } \operatorname{id}_{C} \circ g \xRightarrow { \lambda _{g} } g \xRightarrow { \rho _{g}^{-1} } g \otimes \operatorname{id}_{D}. \]

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

\[ f \xRightarrow [\sim ]{\rho _{f}^{-1}} f \circ \operatorname{id}_{C} \xRightarrow {\operatorname{id}_ f \circ \eta } f \circ (g \circ f) \xRightarrow [\sim ]{\alpha _{f,g,f}} (f \circ g) \circ f \xRightarrow {\epsilon \circ \operatorname{id}_ f} \operatorname{id}_{D} \circ f \xRightarrow [\sim ]{\lambda _{f}} f \]

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$