Kerodon

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

Corollary 8.1.2.13. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category, let $\mathrm{h} \mathit{\operatorname{\mathcal{C}}}$ be its homotopy category, and let

\[ \underline{\operatorname{Hom}}_{\mathrm{h} \mathit{\operatorname{\mathcal{C}}}}: \mathrm{h} \mathit{\operatorname{\mathcal{C}}}^{\operatorname{op}} \times \mathrm{h} \mathit{\operatorname{\mathcal{C}}} \rightarrow \mathrm{h} \mathit{\operatorname{Kan}} \quad \quad (X,Y) \mapsto \operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Y) \]

denote the functor determined by the $\mathrm{h} \mathit{\operatorname{Kan}}$-enrichment of Construction 4.6.8.13. Then the assignment $(X,Y) \mapsto \alpha _{X,Y}$ of Notation 8.1.2.10 determines an isomorphism from $\underline{\operatorname{Hom}}_{\mathrm{h} \mathit{\operatorname{\mathcal{C}}}}$ to the homotopy transport representation of the left fibration $(\lambda _{-}, \lambda _{+}): \operatorname{Tw}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}} \times \operatorname{\mathcal{C}}$.

Proof. Let $H: \mathrm{h} \mathit{( \operatorname{\mathcal{C}}^{\operatorname{op}})} \times \mathrm{h} \mathit{\operatorname{\mathcal{C}}} \rightarrow \mathrm{h} \mathit{\operatorname{Kan}}$ denote the homotopy transport representation for the left fibration $(\lambda _{-}, \lambda _{+})$, given on objects by the formula $H(X,Y) = \{ X\} \times _{ \operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \times _{\operatorname{\mathcal{C}}} \{ Y\} $. For every pair of objects $X,Y \in \operatorname{\mathcal{C}}$, Notation 8.1.2.10 determines an isomorphism

\[ \alpha _{X,Y}: \underline{\operatorname{Hom}}_{\mathrm{h} \mathit{\operatorname{\mathcal{C}}}}(X,Y) \xrightarrow {\sim } H(X,Y) \]

in the homotopy category $\mathrm{h} \mathit{\operatorname{Kan}}$. We wish to show that $\alpha _{X,Y}$ depends functorially on $X$ and $Y$.

We first establish a strong form of functoriality in $Y$. Fix an object $X \in \operatorname{\mathcal{C}}$, and let $h^{X}: \mathrm{h} \mathit{\operatorname{\mathcal{C}}} \rightarrow \mathrm{h} \mathit{\operatorname{Kan}}$ denote the $\mathrm{h} \mathit{\operatorname{Kan}}$-enriched functor corepresented by $X$, given concretely by the formula $h^{X}(Y) = \underline{\operatorname{Hom}}_{\mathrm{h} \mathit{\operatorname{\mathcal{C}}}}(X,Y) = \operatorname{Hom}_{\operatorname{\mathcal{C}}}(X,Y)$. Let $H^{X}: \mathrm{h} \mathit{\operatorname{\mathcal{C}}} \rightarrow \mathrm{h} \mathit{\operatorname{Kan}}$ denote the restriction $H|_{ \{ X\} \times \mathrm{h} \mathit{\operatorname{\mathcal{C}}} }$, which we also regard as an $\mathrm{h} \mathit{\operatorname{Kan}}$-enriched functor (using Variant 5.2.8.11). Note that $h^{X}$ can be identified with the (enriched) homotopy transport representation of the left fibration $\{ X\} \operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}$ (see Example 5.2.8.13). Corollary 4.6.4.18 and Proposition 8.1.2.5 supply equivalences

\[ \{ X\} \operatorname{\vec{\times }}_{\operatorname{\mathcal{C}}} \operatorname{\mathcal{C}}\hookleftarrow \operatorname{\mathcal{C}}_{X/} \hookrightarrow \{ X\} \times _{\operatorname{\mathcal{C}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{C}}) \]

of left fibrations over $\operatorname{\mathcal{C}}$, which induce an isomorphism of $\mathrm{h} \mathit{\operatorname{Kan}}$-enriched functors $\alpha _{X,-}: h^{X} \xrightarrow {\sim } H^{X}$. By construction, this isomorphism carries each object $Y \in \mathrm{h} \mathit{\operatorname{\mathcal{C}}}$ to the isomorphism $\alpha _{X,Y}: \underline{\operatorname{Hom}}(X,Y) \xrightarrow {\sim } H(X,Y)$ of Notation 8.1.2.10, which proves that $\alpha _{X,Y}$ depends functorially on $Y$.

We now show that $\alpha _{X,Y}$ depends functorially on $X$. Fix a morphism $f: W \rightarrow X$ in the $\infty $-category $\operatorname{\mathcal{C}}$. We then have a diagram of $\mathrm{h} \mathit{\operatorname{Kan}}$-enriched functors

8.4
\begin{equation} \begin{gathered}\label{equation:homotopy-transport-twisted-arrow} \xymatrix@R =50pt@C=50pt{ h^{X} \ar [d] \ar [r]^-{\alpha _{X,-}} & H^{X} \ar [d] \\ h^{W} \ar [r]^-{ \alpha _{X,-} } & H^{W}, } \end{gathered} \end{equation}

where the vertical maps are induced by the homotopy class $[f] \in \operatorname{Hom}_{\mathrm{h} \mathit{\operatorname{\mathcal{C}}}^{\operatorname{op}} }(X,W)$. To complete the proof, it will suffice to show that this diagram commutes. Using the corepresentability of the $\mathrm{h} \mathit{\operatorname{Kan}}$-enriched functor $h^{X}$, we are reduced to showing that clockwise and counterclockwise composition around the diagram (8.4) carry $[ \operatorname{id}_{X} ] \in \pi _0( h^{X}(X) ) = \operatorname{Hom}_{\mathrm{h} \mathit{\operatorname{\mathcal{C}}}}(X,X)$ to the same element of $\pi _0( H^{W}(X) )$. We conclude by observing that under the identification $\pi _0( H^ W(X) ) \simeq \operatorname{Hom}_{\mathrm{h} \mathit{\operatorname{\mathcal{C}}}}(W,X)$ supplied by Corollary 8.1.2.7, both constructions carry $[ \operatorname{id}_{X} ]$ to $[f]$ (Exercise 8.1.2.9). $\square$