Kerodon

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

Proposition 8.5.1.7 (Retracts of Isomorphisms). Let $\operatorname{\mathcal{C}}$ be an $\infty $-category containing morphisms $f: X \rightarrow X'$ and $g: Y \rightarrow Y'$. Suppose that $g$ is a retract of $f$ (when regarded as objects of the arrow $\infty $-category $\operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}})$). If $f$ is an isomorphism, then $g$ is also an isomorphism.

Proof. By virtue of Variant 8.5.1.3, we may assume that $\operatorname{\mathcal{C}}$ is (the nerve of) an ordinary category. Choose a commutative diagram

\[ \xymatrix@R =50pt@C=50pt{ Y \ar [d]^{g} \ar [r]^-{ i } & X \ar [r]^-{r} \ar [d]^{f} & Y \ar [d]^{g} \\ Y' \ar [r]^-{i' } & X' \ar [r]^-{r'} & Y', } \]

where the horizontal compositions are the identity morphisms $\operatorname{id}_{Y}$ and $\operatorname{id}_{Y'}$, respectively. If $f$ is an isomorphism, then $g$ is also an isomorphism, with inverse given by the composition $Y' \xrightarrow {i'} X' \xrightarrow { f^{-1} } X \xrightarrow {r} Y$. This follows from the calculations

\[ g \circ r \circ f^{-1} \circ i' = r' \circ f \circ f^{-1} \circ i' = r' \circ \operatorname{id}_{X'} \circ i' = r' \circ i' = \operatorname{id}_{Y'} \]

\[ r \circ f^{-1} \circ i' \circ g = r \circ f^{-1} \circ f \circ i = r \circ \operatorname{id}_{X} \circ i = r \circ i = \operatorname{id}_{Y}. \]
$\square$