Day convolution between symmetric monoidal categories

Proof. Let us write \(\Dd \) for this pullback. We will show directly that \(\Dd \) satisfies the defining universal property of \(\oDay (\Mm _C,\Mm _D)\). It will suffice to produce for any \(\infty \)-operad \(\Pp \) a natural equivalence \[ \Fun _{\Op _{\infty }}(\Pp ,\Dd ) \simeq \Fun _{\Op _{\infty }}(\Pp \times \Mm _C, \Mm _D). \] For the left-hand side, note that \(\Fun _{\Op _{\infty }}(\Pp ,-)\) commutes with pullbacks. Since \(\Comm \) is the terminal \(\infty \)-operad, we have \(\Fun _{\Op _{\infty }}(\Pp ,\Comm ) \simeq *\). Since operad morphisms from \(\Pp \) into a cartesian operad correspond to \(\Pp \)-monoids by Theorem 15.3.11, we obtain equivalences \[ \hspace {-5pt} \Fun _{\Op _{\infty }}(\Pp ,\OpCart _{\Ar ^{\oplax }}) \simeq \Mon _{\Pp }(\Ar ^{\oplax }), \qquad \Fun _{\Op _{\infty }}(\Pp ,\OpCart _{\Cat _{\infty } \times \Cat _{\infty }}) \simeq \Mon _{\Pp }(\Cat _{\infty } \times \Cat _{\infty }). \] It follows that the \(\infty \)-category \(\Fun _{\Op _{\infty }}(\Pp ,\Dd )\) is equivalent to the fiber of the map \[ \Mon _{\Pp }(\Ar ^{\oplax }) \to \Mon _{\Pp }(\Cat _{\infty }) \times \Mon _{\Pp }(\Cat _{\infty }) \] over the pair \((C_{\Pp },D_{\Pp })\), where \(C_{\Pp }\) and \(D_{\Pp }\) are obtained from \(C\) and \(D\) by precomposition with the operad map \(p_{\Pp }\colon \Pp \to \Comm \). By Theorem 16.2.2, this fiber is the \(\infty \)-category \(\Fun ^{\Pp \dlax }(C_{\Pp },D_{\Pp }) = \Fun _{(\Op _{\infty })_{/\Pp }}(\Mm _{C_{\Pp }/\Pp }, \Mm _{D_{\Pp }/\Pp })\) of lax \(\Pp \)-monoidal functors \(C_{\Pp } \to D_{\Pp }\). By the definition of \(C_{\Pp }\) and \(D_{\Pp }\) we have \[ \Mm _{C_{\Pp }/\Pp } \simeq \Pp \times _{\Comm } \Mm _C \qquadtext { and } \Mm _{D_{\Pp }/\Pp } \simeq \Pp \times _{\Comm } \Mm _D, \] hence \[ \hspace {-6pt} \Fun _{(\Op _{\infty })_{/\Pp }}(\Mm _{C_{\Pp }/\Pp }, \Mm _{D_{\Pp }/\Pp }) \simeq \Fun _{(\Op _{\infty })_{/\Pp }}(\Pp \times _{\Comm } \Mm _C, \Pp \times _{\Comm } \Mm _D) \simeq \Fun _{\Op _{\infty }}(\Pp \times _{\Comm } \Mm _C, \Mm _D), \] where the second equivalence uses the universal property of pullbacks. Since \(\Comm \) is terminal, the fiber product \(\Pp \times _{\Comm }\Mm _C\) is the product \(\Pp \times \Mm _C\) in \(\Op _{\infty }\). This was precisely what we wanted to show. □

Proof. Let us write \(\Oo := \oDay (\Mm _C, \Mm _D)\) for simplicity. By definition, the anima of multimorphisms \(\Oo (\{F_i\}_{i \in I}; G)\) is the fiber of the projection map \[ p_{\Oo }\colon \Hom _{\Oo ^{\otimes }}(\{F_i\}_{i \in I}, G) \to \Hom _{\Span (\Fin )}(I, \lra {1}) \] over the active span \(I \xleftarrow {\;\id \;} I \to \lra {1}\). By Theorem 16.2.4, the operad \(\Oo \) sits in the following pullback square of \(\infty \)-operads:

Since hom animae in a pullback of \(\infty \)-categories form a pullback of animae, \(\Hom _{\Oo ^{\otimes }}(\{F_i\}_{i \in I}, G)\) is itself the fiber in a pullback square of hom animae. Taking the fibers of these hom animae over the active span \(I \to \lra {1}\), we find that \(\Oo (\{F_i\}_{i \in I}; G)\) is the fiber in the following pullback square of animae: \begin {equation*}

\end {equation*} Here the object \(\Un (F_i) \in \Ar ^{\oplax }\) is the cartesian unstraightening of the functor \([1]\catop \to \Cat _{\infty }\) which takes the arrow \(1 \to 0\) to \(F_i\colon C \to D\), and similarly for \(\Un (G)\). Since \(\Cat _{\infty }\) and \(\Ar ^{\oplax }\) have finite products, we may write the three multimorphism animae in the source and target of the right vertical map as hom animae in \(\Ar ^{\oplax }\) and \(\Cat _{\infty }\) out of the corresponding products, which results in a pullback square as follows:

By applying Theorem 16.2.2 to the trivial \(\infty \)-operad, we get that the functor \((s,t)\colon \Ar ^{\oplax } \to \Cat _{\infty } \times \Cat _{\infty }\) is a cartesian fibration over \(\Cat _{\infty } \times \{D\}\) and a cocartesian fibration over \(\{C\} \times \Cat _{\infty }\). The fibers of \((s,t)\) are given by the functor categories \(\Fun (C,D)\), with functoriality in \(C\) given by precomposition and functoriality in \(D\) given by postcomposition. The fiber of the upper-right hom anima over a pair \((f,g)\) is therefore the anima of natural transformations \(g\circ \prod _iF_i\to G\circ f\). In particular, Equation 16.1 identifies the required fiber as \[ \Oo (\{F_i\}_{i \in I}; G) \simeq \Hom _{\Fun (C^I,D)}(\bigotimes _D^I \circ \prod _{i \in I} F_i, G \circ \bigotimes _C^I), \] as claimed. □

Proof. Every relative slice category \((\bigotimes _C^n)_{/c}\) is a pullback of the diagram \(C^n \to C \times C \leftarrow \Ar (C)\). Since \(C\) is small, so are \(C^n\) and \(\Ar (C)\), and hence so is \((\bigotimes _C^n)_{/c}\). The collection \(\Kk \) of Proposition 16.2.7 therefore consists of small \(\infty \)-categories, so both of its conditions are implied by the assumptions on \(D\). □

Proof of Proposition 16.2.7. We wish to show that the Day convolution operad \(\Oo := \oDay (\Mm _C, \Mm _D)\) defines a symmetric monoidal \(\infty \)-category, i.e., that the functor \(p_{\Oo }\colon \Oo ^{\otimes } \to \Span (\Fin )\) is a cocartesian fibration. Recall from Lemma 14.2.8 that it is enough to show that the following two conditions are satisfied:

(a)

For every finite collection of functors \(\{F_i\}_{i \in I}\), there exists a functor \(G = \bigotimes _{i \in I}^{\Day } F_i\) and a multimorphism \(\{F_i\}_{i \in I} \to G\) in \(\Oo \) inducing for every other functor \(H\colon C \to D\) an equivalence \[ \Hom _{\Oo _{\lra {1}}}(G,H) \iso \Oo (\{F_i\};H). \]

(b)

For a map \(f\colon I \to J\) of finite sets, if we let \(G_j := \bigotimes _{i \in f^{-1}(j)}^{\Day } F_i\) for all \(j \in J\), then the canonical map \[ \bigotimes _{i \in I}^{\Day } F_i \to \bigotimes _{j \in J}^{\Day } G_j \] is a natural isomorphism of functors \(C \to D\).

For part (a), we define \(G\) as the left Kan extension of the composite functor \[ \prod _{i \in I} C \xrightarrow {\prod _{i \in I} F_i} \prod _{i \in I} D \xrightarrow {\otimes _D} D \] along the tensor product functor \(\otimes _C\colon C^I \to C\). Explicitly, for an object \(c \in C\), its value is given by the colimit: \[ G(c) := \colim _{\{c'_i\}_{i \in I} \in (\bigotimes _C^I)_{/c}} \left ( \bigotimes _{i \in I} F_i(c'_i) \right ). \] The existence of this left Kan extension is guaranteed by condition (1) of our hypothesis, as the indexing category \((\bigotimes _C^I)_{/c}\) is in our collection \(\Kk \). The universal property of this left Kan extension provides a natural transformation \[ \eta \colon \bigotimes _D^I \circ \prod _{i \in I} F_i \Longrightarrow G \circ \bigotimes _C^I, \] which by Proposition 16.2.6 corresponds to a multimorphism \(\eta \colon \{F_i\}_{i \in I} \to G\) in \(\Oo \). The universal property of left Kan extension precisely says that for any other functor \(H\colon C \to D\), composition with \(\eta \) induces an equivalence \[ \Hom _{\Oo _{\lra {1}}}(G,H) \simeq \Nat (G, H) \iso \Nat \left ( \bigotimes _D^I \circ \prod _{i \in I} F_i, H \circ \bigotimes _C^I \right ) \simeq \Oo (\{F_i\}_{i \in I};H), \] as desired.

We now show that also (b) holds. Let \(f\colon I \to J\) be a map in \(\Fin \), and write \(G_j := \bigotimes _{i \in f^{-1}(j)}^{\Day } F_i\) for all \(j \in J\). We need to show that the canonical transformation \[ \bigotimes _{i \in I}^{\Day } F_i \to \bigotimes _{j \in J}^{\Day } G_j \] is a natural isomorphism of functors \(C \to D\). To help visualize this, consider the following diagram:

Since left Kan extensions compose, it will suffice to show that the composite \(\bigotimes _D^J \circ \prod _{j \in J} G_j\colon C^J \to D\) is the left Kan extension of the composite \(\bigotimes _D^I \circ \prod _{i \in I} F_i \colon C^I \to D\) along \((\bigotimes _C^f)\colon C^I \to C^J\). By the pointwise formula for Kan extensions, this amounts to showing that for every tuple \((c_j)_{j \in J} \in C^J\), the map \[ \colim _{(c'_i) \in (\bigotimes _C^f)_{/c}} \bigotimes _{i \in I}^D F_i(c'_i) \to \bigotimes _{j \in J} G_j(c_j) \] is a natural isomorphism. Since the functor \(\bigotimes _C^f\colon C^I \to C^J\) is a product of the individual functors \(\bigotimes _C^{I_j}\colon C^{I_j} \to C\), the indexing category \((\bigotimes _C^f)_{/c}\) on the left is a product over \(j \in J\) of the relative slice categories \((\bigotimes _C^{I_j})_{/c_j}\). But we also have \[ G_j(c_j) = \colim _{(c''_i) \in (\bigotimes _C^{I_j})_{/c_j}} \bigotimes _{i \in I_j}^D F_i(c''_i), \] and since the functor \(\bigotimes _{j \in J}^D\colon D^J \to D\) preserves the relevant colimits in each variable separately it follows that the map is a natural isomorphism. This finishes the proof. □

Proof. Part (1) is induced by precomposition on Day convolution operads. For part (2), postcomposition first gives a lax symmetric monoidal refinement. Since \(v\) is symmetric monoidal and preserves the colimits in the pointwise formulas of Remark 16.2.9, it carries each Day convolution product and the Day convolution unit to the corresponding product and unit in \(\Fun (C,D')\). Its structure maps are therefore isomorphisms. □

Proof. The hypotheses on the relative slice categories ensure that pointwise left Kan extension along \(u\) exists. Its right adjoint \(u^*\) is lax symmetric monoidal by Proposition 16.2.10. By Proposition 14.3.11, it therefore suffices to show that for every finite collection of functors \(F_i\colon A\to D\), indexed by a finite set \(I\), the canonical comparison \[ u_!\bigl (\bigotimes _{i\in I}^{\Day }F_i\bigr ) \longrightarrow \bigotimes _{i\in I}^{\Day }u_!(F_i) \] is an isomorphism.

Set \[ H:=\bigotimes _D^I\circ \prod _{i\in I}F_i\colon A^I\to D. \] By the description of Day convolution in Remark 16.2.9 and the composition law for left Kan extensions, the source of the comparison is the left Kan extension of \(H\) along \[ A^I\xrightarrow {\smash {\bigotimes _A^I}}A\xrightarrow {u}B. \] On the other hand, the pointwise formula for left Kan extensions and the assumptions on the tensor product of \(D\) show that \[ \bigotimes _D^I\circ \prod _{i\in I}u_!(F_i)\colon B^I\to D \] is the left Kan extension of \(H\) along \(u^I\colon A^I\to B^I\): the relative slice of \(u^I\) over a tuple \((b_i)_{i\in I}\) is the product of the relative slices \(u_{/b_i}\), and its colimit may be computed iteratively. Applying Day convolution and composing left Kan extensions therefore identifies the target of the comparison with the left Kan extension of \(H\) along \[ A^I\xrightarrow {u^I}B^I\xrightarrow {\smash {\bigotimes _B^I}}B. \] Since \(u\) is symmetric monoidal, these two composite functors are naturally equivalent. The canonical comparison is therefore an isomorphism, as desired. □

Proof. The cited corollary applies since \(\An \) admits small colimits and the functor \(- \times -\colon \An \times \An \to \An \) preserves colimits in both variables. □

Proof. It suffices to show that for every third functor \(H\colon C \to D\) there is a natural equivalence \[ \Nat (H \otimes _{\Day } F, G) \simeq \Nat \left (H, \int _{Y \in C} \iHom _D(F(Y), G(- \otimes _C Y))\right ). \] Since the Day convolution is a left Kan extension, the left-hand side is equivalent to the anima \[ \Nat (H(-) \otimes _D F(-), G(- \otimes _C -)) \] of natural transformations of functors \(C \times C \to D\). By Proposition 23.6.6, this anima is the end \[ \int _{(X,Y) \in C \times C} \Hom _D(H(X) \otimes _D F(Y), G(X \otimes _C Y)). \] Using the Fubini rule for ends, Lemma 23.6.5, the adjunction \(- \otimes _D F(Y) \dashv \iHom _D(F(Y),-)\), and the fact that \(\Hom _D(H(X),-)\) preserves limits, we may rewrite this as \begin {align*} \int _{X \in C} &\int _{Y \in C} \Hom _D(H(X), \iHom _D(F(Y), G(X \otimes _C Y))) \\ &\simeq \int _{X \in C} \Hom _D\left (H(X), \int _{Y \in C} \iHom _D(F(Y), G(X \otimes _C Y))\right ). \end {align*}

Using the end description of animae of natural transformations once more gives the desired result. □