Universal property of cartesian monoidal structures

Proof. We use the concrete model of the cartesian operad. Evaluation at the identity maps \(\id _I\) will send an operad map \(\Oo \to \OpCart _C\) to an \(\Oo \)-monoid, and restriction along inert morphisms will provide the inverse construction.

Let \(r\colon A\to \Span (\Fin )\) be the cartesian fibration from Construction 15.3.7. For an \(\infty \)-operad \(\Oo \), put \[ D_{\Oo }:=\Oo ^{\otimes }\times _{\Span (\Fin )}A. \] The fiber of the projection \(D_{\Oo }\to \Oo ^{\otimes }\) over \(X\in \Oo ^{\otimes }_I\) is \((\Fin _{/I})\catop \), whose initial object is \(\id _I\). By Proposition 23.3.4, these initial objects determine a unique left-adjoint section \[ s\colon \Oo ^{\otimes }\to D_{\Oo }, \qquad X\longmapsto (X,\id _I). \]

The cocartesian fibration \(\widetilde C^{\times }\to \Span (\Fin )\) of Construction 15.3.7 is the parametrized functor category associated to \(r\). Hence Theorem 23.8.3 gives an equivalence \begin {equation} \label {eq:Currying_Cartesian_Operad} \Fun _{/\Span (\Fin )}(\Oo ^{\otimes },\widetilde C^{\times }) \iso \Fun (D_{\Oo },C). \end {equation} It sends \(\Phi \) to the evaluation functor \[ G_{\Phi }(X,u\colon U\to I):=\Phi (X)(u). \]

By construction of \(r\), an object \(u\colon U\to I\) of its fiber over \(I\) indexes the backwards span \[ I\xleftarrow {u}U\xrightarrow {=}U. \] The functoriality of partial cocartesian lifts from Proposition 23.1.4 therefore gives, naturally in \(\Oo \), a functor \[ \theta _{\Oo }\colon D_{\Oo }\to \Oo ^{\otimes }, \qquad (X,u\colon U\to I)\longmapsto X_U, \] and a natural transformation \[ \delta \colon \id _{D_{\Oo }}\longrightarrow s\theta _{\Oo } \] whose component at \((X,u)\) has \(\Oo ^{\otimes }\)-component the inert lift \(X\to X_U\) of the backwards span above and \(A\)-component the cartesian lift from \(u\) to \(\id _U\) over the same span. Restriction along identity maps gives a natural isomorphism \(\theta _{\Oo }s\simeq \id _{\Oo ^{\otimes }}\).

Let \(\Phi \colon \Oo \to \OpCart _C\) be a morphism of \(\infty \)-operads. Regarding its total functor as a functor to the concrete model and applying Equation 15.2, define \[ R(\Phi ):=G_{\Phi }s, \qquad R(\Phi )(X)=\Phi (X)(\id _I) \] for \(X\in \Oo ^{\otimes }_I\). This functor preserves finite products. Indeed, for a finite collection of objects \(X_a\in \Oo ^{\otimes }_{I_a}\), product preservation of \(\Phi \) and Lemma 15.3.9 give \[ R(\Phi )\left (\prod _aX_a\right ) \simeq \left (\prod _a\Phi (X_a)\right )\left (\id _{\bigsqcup _aI_a}\right ) \simeq \prod _a\Phi (X_a)(\id _{I_a}) = \prod _aR(\Phi )(X_a). \] The same formula includes the empty product. We have therefore obtained a functor \[ R\colon \Fun _{\Op _{\infty }}(\Oo ,\OpCart _C) \longrightarrow \Fun ^{\times }(\Oo ^{\otimes },C). \]

Conversely, let \(M\colon \Oo ^{\otimes }\to C\) preserve finite products. The functor \[ M\theta _{\Oo }\colon D_{\Oo }\to C \] corresponds under Equation 15.2 to a functor \[ \widehat M\colon \Oo ^{\otimes }\to \widetilde C^{\times }. \] This functor factors through \(C^{\times }_{\mathrm {con}}\). Indeed, fix \(X\in \Oo ^{\otimes }_I\). A finite product in \((\Fin _{/I})\catop \) is represented by a disjoint union \(\bigsqcup _aU_a\to I\) in \(\Fin _{/I}\), and operadic inert restriction gives a natural isomorphism \[ X_{\bigsqcup _aU_a}\simeq \prod _aX_{U_a}. \] Consequently, \[ \widehat M(X)\left (\bigsqcup _aU_a\to I\right ) = M\left (X_{\bigsqcup _aU_a}\right ) \simeq \prod _aM(X_{U_a}), \] including the empty product. Thus \(\widehat M(X)\colon (\Fin _{/I})\catop \to C\) preserves finite products.

We identify \(C^{\times }_{\mathrm {con}}\) with \(C^{\times }\) using Proposition 15.3.10. The resulting total functor \(\widehat M\colon \Oo ^{\otimes }\to C^{\times }\) preserves finite products. Indeed, let \(\{X_a\}_{a\in S}\) lie over finite sets \(\{I_a\}_{a\in S}\), and let \(u\colon U\to \bigsqcup _aI_a\). Writing \(U_a:=U\times _{\bigsqcup _aI_a}I_a\), compatibility of inert restriction with products gives \[ \left (\prod _aX_a\right )_U\simeq \prod _a(X_a)_{U_a}. \] After applying \(M\), these isomorphisms identify, at every \(u\), the product-comparison map for \(\widehat M\) with an isomorphism. They are natural in \(u\) by the coherence of \(\theta _{\Oo }\), and isomorphisms in a functor category are detected pointwise. Thus the comparison is an isomorphism in the relevant functor category. Hence \(\widehat M\) is a morphism of \(\infty \)-operads. We have constructed a functor \[ \widehat {(-)}\colon \Fun ^{\times }(\Oo ^{\otimes },C) \longrightarrow \Fun _{\Op _{\infty }}(\Oo ,\OpCart _C). \]

The natural isomorphism \(\theta _{\Oo }s\simeq \id _{\Oo ^{\otimes }}\) gives, naturally in \(M\), \[ R(\widehat M)=M\theta _{\Oo }s\simeq M. \] In the other direction, apply \(G_{\Phi }\) to \(\delta \). This gives a natural transformation \[ G_{\Phi } \longrightarrow G_{\Phi }s\theta _{\Oo } = R(\Phi )\theta _{\Oo }. \] Its component at \((X,u\colon U\to I)\) is the canonical map \[ \Phi (X)(u)\longrightarrow \Phi (X_U)(\id _U). \] It is an isomorphism: the \(\Oo ^{\otimes }\)-component of \(\delta \) is inert, so \(\Phi \) carries it to an inert, hence cocartesian, morphism in \(C^{\times }\) by Corollary 14.1.11; the concrete transport formula then identifies its target, evaluated at \(\id _U\), with its source, evaluated at \(u\). Currying therefore gives a natural isomorphism \[ \Phi \simeq \widehat {R(\Phi )}. \] Thus \(R\) and \(\widehat {(-)}\) are inverse equivalences.

The construction is natural in \(\Oo \) by pullback and the naturality of \(\theta \) and \(\delta \). It is natural in \(C\) because postcomposition with a finite-product-preserving functor commutes with currying and preserves the concrete subcategories \(C^{\times }_{\mathrm {con}}\). Under Proposition 15.3.10, the resulting map between the concrete models is the morphism of cartesian operads supplied by Proposition 15.3.6. Hence we obtain a natural equivalence of functors \[ \Op _{\infty }\catop \times \Cat _{\infty }^{\mathrm {prod}} \longrightarrow \Cat _{\infty }. \] Passing to groupoid cores gives the natural equivalence of hom animae which exhibits \(\Oo \mapsto \Oo ^{\otimes }\) as left adjoint to \(\OpCart \). □