For \(J\in \mathrm{Cat}_{\infty}\) and \(\mathcal C\in \mathrm{Pr}^\mathrm{L}\), the functor \(\mathcal C\times J \rightarrow\mathrm{Fun}(J^{\mathrm{op}}, \mathcal C)\), \[ (c,j)\mapsto c \otimes \mathrm{Hom}_{J}(-, j) \in \mathrm{Fun}(J^{\mathrm{op}}, \mathcal C)\] (where \(\otimes\) denotes the action of \(\mathcal S\) on \(\mathcal C\) inherited from the presentability of \(\mathcal C\)) induces an equivalence \[ \mathcal C\otimes \mathcal P(J) \simeq \mathrm{Fun}(J^{\mathrm{op}}, \mathcal C)\] in \(\mathrm{Pr}^\mathrm{L}\) (where \(\otimes\) denotes the tensor product of \(\mathrm{Pr}^\mathrm{L}\)).
Proof.
Consider the chain of equivalences \[\mathcal C\otimes \mathcal P(J) \simeq \mathrm{Fun^L}(\mathcal P(J), \mathcal C^{\mathrm{op}})^{\mathrm{op}} \simeq \mathrm{Fun}(J, \mathcal C^{\mathrm{op}})^{\mathrm{op}} \simeq \mathrm{Fun}(J^{\mathrm{op}}, \mathcal C)\] Here, the first equivalence follows from ([002Z]), the second equivalence is the universal property of the Yoneda embedding [Lur09, Thm. 5.1.5.6], and the last records the interplay between functor categories and opposites. Precomposing this equivalence with the inclusion functor \(\mathcal C\times J \rightarrow\mathcal C\otimes \mathcal P(J)\) (which is cocontinuous in its second argument) unpacks to the functor ([0063]). ◻
Original source: arXiv:2401.02956v2
Original source · 2401.02956v2