Kerodon

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

Proposition 1.4.4.2. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category containing morphisms $f: X \rightarrow Y$ and $g: Y \rightarrow Z$. Then:

$(1)$

There exists a morphism $h: X \rightarrow Z$ which is a composition of $f$ and $g$.

$(2)$

Let $h: X \rightarrow Z$ be a composition of $f$ and $g$, and let $h': X \rightarrow Z$ be another morphism in $\operatorname{\mathcal{C}}$ having the same source and target. Then $h'$ is a composition of $f$ and $g$ if and only if $h'$ is homotopic to $h$.

Proof. The tuple $(g, \bullet , f)$ determines a map of simplicial sets $\sigma _0: \Lambda ^{2}_{1} \rightarrow \operatorname{\mathcal{C}}$ (Proposition 1.2.4.7). Since $\operatorname{\mathcal{C}}$ is an $\infty $-category, we can extend $\sigma _0$ to a $2$-simplex $\sigma $ of $\operatorname{\mathcal{C}}$. Then $\sigma $ witnesses the morphism $h = d^{2}_1(\sigma )$ as a composition of $f$ and $g$. This proves $(1)$. To prove $(2)$, let us first suppose that $h': X \rightarrow Z$ is some other morphism in $\operatorname{\mathcal{C}}$ which is a composition of $f$ and $g$. We will show that $h$ is homotopic to $h'$. Choose a $2$-simplex $\sigma '$ which witnesses $h'$ as a composition of $f$ and $g$. Then the tuple $( s^{1}_1(g), \bullet , \sigma ', \sigma )$ determines a morphism of simplicial sets $\tau _0: \Lambda ^{3}_{1} \rightarrow \operatorname{\mathcal{C}}$ (Proposition 1.2.4.7), which we depict informally as a diagram

\[ \xymatrix@C =70pt@R=70pt{ & Y \ar [r]^-{g} \ar [drr]^{ g } & Z \ar@ {-->}[dr]^{\operatorname{id}_ Z} & \\ X \ar [ur]^{f} \ar@ {-->}[urr]^{h} \ar@ {-->}[rrr]^{h'} & & & Z } \]

where the dotted arrows indicate the boundary of the “missing” face of the horn $\Lambda ^{3}_{1}$. Using our assumption that $\operatorname{\mathcal{C}}$ is an $\infty $-category, we can extend $\tau _0$ to a $3$-simplex $\tau $ of $\operatorname{\mathcal{C}}$. Then the face $d^{2}_1(\tau )$ is a homotopy from $h$ to $h'$.

We now prove the converse. Let $\sigma $ be a $2$-simplex of $\operatorname{\mathcal{C}}$ which witnesses $h$ as a composition of $f$ and $g$, and let $h': X \rightarrow Z$ be a morphism of $\operatorname{\mathcal{C}}$ which is homotopic to $h$. Let $\sigma ''$ be a $2$-simplex of $\operatorname{\mathcal{C}}$ which is a homotopy from $h$ to $h'$. Then the tuple $( s^{1}_1(g), \sigma '', \bullet , \sigma )$ determines a map of simplicial sets $\rho _0: \Lambda ^{3}_{2} \rightarrow \operatorname{\mathcal{C}}$ (Proposition 1.2.4.7), which we depict informally as a diagram

\[ \xymatrix@C =70pt@R=70pt{ & Y \ar [r]^-{g} \ar@ {-->}[drr]^{ g } & Z \ar [dr]^{\operatorname{id}_ Z} & \\ X \ar@ {-->}[ur]^{f} \ar [urr]^{h} \ar@ {-->}[rrr]^{h'} & & & Z. } \]

Our assumption that $\operatorname{\mathcal{C}}$ is an $\infty $-category guarantees that we can extend $\rho _0$ to a $3$-simplex $\rho $ of $\operatorname{\mathcal{C}}$. Then the face $d^{2}_2(\rho )$ witnesses $h'$ as a composition of $f$ and $g$. $\square$