Cartesian monoidal structures

Proof. Apply Corollary 15.1.5 to \(C^{(-)}\). The resulting transport sends an \(I\)-indexed family to \[ (x_i)_{i\in I}\longmapsto \left (\prod _{k\in g^{-1}(j)}x_{f(k)}\right )_{j\in J}. \] The argument of Proposition 15.2.1 applies verbatim to show that the construction preserves finite products: the inclusion \(\Fin \catop \hookrightarrow \Span (\Fin )\) preserves finite products and is the identity on objects, so product preservation may be tested on the original functor \(C^{(-)}\). The empty product gives the terminal object as unit, and transport along \(\lra {2}\xleftarrow {=}\lra {2}\xrightarrow {\nabla }\lra {1}\) gives the binary product. The inert projections in \(C^{\times }\) induce in the fiber \(C\) the two projection maps from this product. □

Proof. This is an instance of Lemma 15.2.22 applied to the opposite symmetric monoidal \(\infty \)-category. □

Proof. The transport formula in Proposition 15.3.1 shows that the monoidal unit is the terminal object of \(C\) and the binary tensor product is the product in \(C\). Under the identification of the fiber over \(\lra {1}\) with \(C\), the two inert projections are the two maps from this product induced by the terminal maps of its factors, hence are precisely the product projections. Thus \((C,\times )\) satisfies the two conditions of Lemma 15.3.4. □

Proof. Passing to opposites identifies \(\Cat _{\infty }^{\otimes ,\cart }\) with \(\Cat _{\infty }^{\otimes ,\cocart }\), and identifies the forgetful functor \(U\) with the corresponding forgetful functor \[ \Cat _{\infty }^{\otimes ,\cocart }\to \Cat _{\infty }^{\mathrm {coprod}}. \] The latter is an equivalence by Corollary 15.2.21: the functor \(C\mapsto (C,\amalg )\) is an equivalence whose composite with the forgetful functor is the identity on \(\Cat _{\infty }^{\mathrm {coprod}}\). Hence \(U\) is an equivalence as well.

By Proposition 15.3.5, the assignment \(C\mapsto (C,\times )\) lands in \(\Cat _{\infty }^{\otimes ,\cart }\). Full faithfulness of \(U\) uniquely lifts every finite-product-preserving functor \(C\to D\) to a symmetric monoidal functor \((C,\times )\to (D,\times )\). These lifts define a functor whose composite with \(U\) is the identity, and hence an inverse to \(U\). □

Proof. For a span \(I\xleftarrow {f}K\xrightarrow {g}J\), the functor \(f_!g^*\colon \Fin _{/J}\to \Fin _{/I}\) preserves finite coproducts: pullback along \(g\) does so because \(\Fin \) is extensive, while postcomposition along \(f\) plainly does so. Hence \((f_!g^*)\catop \) preserves finite products, and restriction along it preserves finite-product-preserving functors. □

Proof. Regarding \(I\) as a discrete \(\infty \)-category, the description of finite families in Construction 14.1.16 gives a finite-coproduct-preserving equivalence \[ \Fin (I)\iso \Fin _{/I} \] which sends a finite family of elements of \(I\) to its indexing map to \(I\). The dual of Lemma 14.1.17 therefore identifies restriction to the singleton families with an equivalence \[ \Fun ^{\times }((\Fin _{/I})\catop ,C) \simeq \Fun (I,C) = C^I. \] Under this equivalence, a functor \(F\) corresponds to its values on the singleton inclusions, and one has \[ F(U\to I)\simeq \prod _{u\in U}F(\{u\}\to I).\qedhere \] □

Proof. By the uniqueness of cartesian monoidal structures from Proposition 15.3.6, it suffices to show that \(C^{\times }_{\mathrm {con}}\) defines a cartesian monoidal structure on \(C\).

By Lemma 15.3.8, the projection \(C^{\times }_{\mathrm {con}}\to \Span (\Fin )\) is a cocartesian fibration. Under the fiber equivalences of Lemma 15.3.9, the product-comparison maps of its straightening are the canonical equivalences \[ C^{I\sqcup J}\simeq C^I\times C^J, \] and its value at \(\emptyset \) is the terminal category. Thus the straightening preserves finite products, so Lemma 14.2.4 makes \(C^{\times }_{\mathrm {con}}\) into a symmetric monoidal \(\infty \)-category with underlying \(\infty \)-category \(C\).

Transport along a span \(I\xleftarrow {f}K\xrightarrow {g}J\) sends an \(I\)-indexed family to \[ (x_i)_{i\in I}\longmapsto \left (\prod _{k\in g^{-1}(j)}x_{f(k)}\right )_{j\in J}. \] Hence its unit is terminal, its binary tensor product is the product in \(C\), and its inert structure maps are the product projections. By Lemma 15.3.4, it is therefore cartesian monoidal. □

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 \). □

Proof. Apply Theorem 15.3.11 to \(\Oo =\OpCart _C\). The identity of \(\OpCart _C\) corresponds to a finite-product-preserving functor \(\Pi _C\colon C^{\times }\to C\). By the naturality in \(\Oo \), the equivalence for a general \(\Oo \) is given by postcomposition with this functor.

Unwinding the construction of the equivalence, if \(F\colon (\Fin _{/I})\catop \to C\) is an object of \(C^{\times }\) over \(I\), then \[ \Pi _C(F)\simeq F(\id _I). \] Under the equivalence of Lemma 15.3.9, this sends the family \(\{x_i\}_{i\in I}\) to \(\prod _{i\in I}x_i\). □

Proof. This is the special case of Theorem 15.3.11 where \(\Oo =\Assoc \) and \(\Oo =\Comm \), respectively. □