# Kerodon

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

Corollary 6.1.2.8. 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 suppose we are given $2$-morphisms $\eta : \operatorname{id}_{C} \Rightarrow g \circ f$ and $\epsilon : f \circ g \Rightarrow \operatorname{id}_{D}$ satisfying condition $(Z1)$ of Definition 6.1.1.1. Let $\gamma : g \Rightarrow g$ denote the $2$-morphism given by the composition

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

Then $\gamma$ is idempotent: that is, $\gamma ^2 = \gamma$ in the category $\underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}(D,C)$. In particular, if $\gamma$ has either a left or a right inverse, then $\gamma = \operatorname{id}_{g}$ (so that $(\eta , \epsilon )$ is an adjunction between $f$ and $g$).

Proof. Let $\gamma '$ denote the composition $g \xRightarrow {\gamma } g \xRightarrow { \rho _{g}^{-1} } g \circ \operatorname{id}_ D$. Then $\gamma '$ is the right adjunct of $\epsilon$ with respect to $\eta$ (see Example 6.1.2.3). Invoking Remark 6.1.2.4, we deduce that the horizontal composition $\gamma ' \gamma$ is the right adjunct of $\epsilon '$ with respect to $\eta$, where $\epsilon '$ denotes the composite map $f \circ g \xRightarrow { \operatorname{id}_ f \circ \gamma } f \circ g \xRightarrow {\epsilon } \operatorname{id}_ D$. Combining Example 6.1.2.2 with Remark 6.1.2.4, we see that $\epsilon '$ is the left adjunct of $\gamma '$ with respect to $\epsilon$. Since the pair $(\eta , \epsilon )$ satisfies $(Z1)$, it follows that $\gamma ' \gamma = \gamma '$, Composing with the right unit constraint $\rho _ g$, we conclude that $\gamma \gamma = \gamma$. $\square$