# Kerodon

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

Proposition 6.1.3.4. Let $\operatorname{\mathcal{C}}$ be a $2$-category containing $1$-morphisms $f,f': C \rightarrow D$ which admit $(\eta , \epsilon )$ between $f$ and $g$ and $(\eta ', \epsilon ')$ between $f'$ and $g'$. Then every $2$-morphism $\beta : f \Rightarrow f'$ determines a $2$-morphism $\beta ^{R}: g' \Rightarrow g$, which is uniquely determined by either of the following properties:

$(1)$

The diagram

$\xymatrix@R =50pt@C=50pt{ \operatorname{id}_{C} \ar@ {=>}[r]^-{\eta } \ar@ {=>}[d]^{\eta '} & g \circ f \ar@ {=>}[d]^{ \operatorname{id}_{g} \circ \beta } \\ g' \circ f' \ar@ {=>}[r]^-{ \beta ^{R} \circ \operatorname{id}_{f'} } & g \circ f' }$

commutes (in the category $\underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(C,C)$).

$(2)$

The diagram

$\xymatrix@R =50pt@C=50pt{ f \circ g' \ar@ {=>}[r]^-{\operatorname{id}_{f} \circ \beta ^{R} } \ar@ {=>}[d]^{\beta \circ \operatorname{id}_{g'} } & f \circ g \ar@ {=>}[d]^{ \epsilon } \\ f' \circ g' \ar@ {=>}[r]^-{\epsilon '} & \operatorname{id}_{D} }$

commutes (in the category $\underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(D,D)$).

Proof. It follows from Corollary 6.1.3.3 that there is a unique morphism $\beta ^{R}$ satisfying condition $(1)$. We will prove that $\beta ^{R}$ also satisfies condition $(2)$ (it is also uniquely determined by condition $(2)$, by virtue of Corollary 6.1.3.3). Note $(2)$ is equivalent to the assertion that $\epsilon '(\beta \circ \operatorname{id}_{g'})$ is the left adjunct of $\rho _{g}^{-1} \beta ^{R}$ with respect to $\epsilon$ (in the sense of Construction 6.1.2.1). By virtue of Proposition 6.1.2.5, this is equivalent to the assertion that $\rho _{g}^{-1} \beta ^{R}$ is the right adjunct of $\epsilon '(\beta \circ \operatorname{id}_{g'})$ with respect to $\eta$. This follows from the commutativity of the outer rectangle in the diagram

$\xymatrix@R =50pt@C=50pt{ g' \ar@ {=>}[r]^-{\lambda _{g'}^{-1}}_{\sim } \ar@ {=}[ddd] & \operatorname{id}_{C} \circ g' \ar@ {=>}[r]^-{\eta \circ \operatorname{id}_{g'} } \ar@ {=>}[d]_{\eta ' \circ \operatorname{id}_{g'} } & (g \circ f) \circ g' \ar@ {=>}[r]^-{ \alpha _{g,f,g'}^{-1}}_{\sim } \ar@ {=>}[d]_{ (\operatorname{id}_{g} \circ \beta ) \circ \operatorname{id}_{g'} } & g \circ (f \circ g') \ar@ {=>}[ddl]^{\operatorname{id}_{g} \circ (\beta \circ \operatorname{id}_{g'} )} \ar@ {=>}[dddd]^{ \operatorname{id}_{g} \circ \epsilon '(\beta \circ \operatorname{id}_{g'} ) } \\ & (g' \circ f') \circ g' \ar@ {=>}[r]^-{(\beta ^ R \circ \operatorname{id}_{f'}) \circ \operatorname{id}_{g'} } \ar@ {=>}[d]^{\sim }_{\alpha _{g',f',g'}^{-1}} & (g \circ f') \circ g' \ar@ {=>}[d]^{\sim }_{\alpha _{g,f',g'}^{-1}} & \\ & g' \circ (f' \circ g') \ar@ {=>}[r]^-{\beta ^{R} \circ (\operatorname{id}_{f'} \circ \operatorname{id}_{g'} ) } \ar@ {=>}[d]^{ \operatorname{id}_{g'} \circ \epsilon '} & g \circ (f' \circ g') \ar@ {=>}[ddr]^{\operatorname{id}_{g} \circ \epsilon '} & \\ g' \ar@ {=>}[r]^-{\rho _{g'}^{-1} } \ar@ {=>}[d]^{\gamma } & g' \circ \operatorname{id}_{D} \ar@ {=>}[drr]^{\beta ^{R} \circ \operatorname{id}_{\operatorname{id}_ D}} & & \\ g \ar@ {=>}[rrr]^{\rho _{g}^{-1} } & & & g \circ \operatorname{id}_{D} }$

in the category $\underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(D,C)$. Here the upper middle square commutes by virtue of condition $(1)$, the rectangle on the left commutes by virtue of the assumption that $(\eta , \epsilon )$ is an adjunction, and the commutativity of the rest of the diagram follows by the naturality properties of the associativity and unit constraints of the $2$-category $\operatorname{\mathcal{C}}$. $\square$