Kerodon

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

Corollary 6.1.5.9. Let $\operatorname{\mathcal{C}}$ be a $2$-category containing objects $C$, $D$, and $E$, together with $1$-morphisms

\[ f: C \rightarrow D \quad \quad g: D \rightarrow C \quad \quad f': D \rightarrow E \quad \quad g': E \rightarrow D. \]

Let $(\eta ,\epsilon )$ be an adjunction between $f$ and $g$, and let $(\eta ',\epsilon ')$ be an adjunction between $f'$ and $g'$. Then the pair $( c(\eta , \eta '), c(\epsilon , \epsilon ') )$ is an adjunction between $f' \circ f$ and $g \circ g'$. Here $c(\eta ,\eta ')$ is the contraction of $\eta $ with $\eta '$ (in the sense of Construction 6.1.5.1), and $c(\epsilon , \epsilon ')$ is the contraction of $\epsilon $ with $\epsilon '$ (in the sense of Construction 6.1.5.7).

Proof. By virtue of Proposition 6.1.5.3 and Corollary 6.1.2.6, it will suffice to show that for every object $T \in \operatorname{\mathcal{C}}$ equipped with $1$-morphisms $c: T \rightarrow C$ and $e: T \rightarrow E$, the diagram

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{Hom}_{ \underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(T,E)}( (f' \circ f) \circ c, e ) \ar [r]_{\sim }^{\alpha _{f',f,c}} & \operatorname{Hom}_{ \underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(T,E)}( f' \circ (f \circ c), e ) \\ & \operatorname{Hom}_{ \underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(T,D)}( f \circ c, g' \circ e ) \ar [u] \\ \operatorname{Hom}_{ \underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(T,C)}( c, (g \circ g') \circ e ) \ar [r]^-{\alpha _{g,g',e}}_{\sim } \ar [uu] & \operatorname{Hom}_{ \underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(T,C)}( c, g \circ (g' \circ e) ) \ar [u] } \]

commutes, where the right vertical maps are given by the formation of left adjuncts with respect to $\epsilon $ and $\epsilon '$, and the left vertical map is given by the formation of left adjuncts with respect to the contraction $c(\epsilon ,\epsilon ')$ of Construction 6.1.5.7. This follows by applying Proposition 6.1.5.3 to the conjugate $2$-category $\operatorname{\mathcal{C}}^{\operatorname{c}}$. $\square$