Operadic envelopes

Proof. By definition, \(\Op _{\Ff }\) is a full subcategory of \((\Cat _\infty )^{\Ll \mathrm {-cocart}}_{/\Span _{L,R}(F)}\). We will similarly identify \(\Mon _{\Ff }(\Cat _{\infty })\) with a full subcategory of \(\Cocart (\Span _{L,R}(F))\), see Remark 17.3.9. Recall from Corollary 17.2.10 that the forgetful functor \(\Cocart (\Span _{L,R}(F)) \hookrightarrow (\Cat _\infty )^{\Ll \mathrm {-cocart}}_{/\Span _{L,R}(F)}\) admits a left adjoint \[ E_{\Rr }\colon (\Cat _\infty )^{\Ll \mathrm {-cocart}}_{/\Span _{L,R}(F)} \to \Cocart (\Span _{L,R}(F)). \] Since \(\Mm \) is defined as the restriction of this forgetful functor, it remains to show that \(E_{\Rr }\) restricts to a functor \[ \Env _{\Ff }\colon \Op _{\Ff } \to \Mon _{\Ff }(\Cat _{\infty }). \] To this end, let \(\Oo \) be an \(\Ff \)-operad, and consider the cocartesian fibration \(E_{\Rr }(p_{\Oo }) \to \Span _{L,R}(F)\) from Proposition 17.2.8. We must show that its straightening \(\Span _{L,R}(F) \to \Cat _{\infty }\) satisfies the Segal condition. The description of cocartesian morphisms in Proposition 17.2.8, applied to the factorization of a composite of spans, gives the following explicit description of this straightening:

• On objects, it sends \(I \in F\) to the pullback \(\infty \)-category \((F_R)_{/I} \times _{\Span _{L,R}(F)} \Oo ^{\otimes }\).
• Given a backwards morphism \(g\colon J \leftarrow I\), the functor \((F_R)_{/J} \times _{\Span _{L,R}(F)} \Oo ^{\otimes } \to (F_R)_{/I} \times _{\Span _{L,R}(F)} \Oo ^{\otimes }\) sends a pair \((X,r\colon J' \to J)\) with \(r \in F_R\) and \(X \in \Oo ^{\otimes }_{J'}\) to the pair \((Y,r'\colon I' \to I)\), where \(r'\) is defined via the pullback square

  

  and where \(Y\) is the target of a \(p_{\Oo }\)-cocartesian lift \(\hat {f}_X\colon X \to Y\) of \(f\).
• Given a forward morphism \(g\colon I \to J\), the transport functor sends \((X,r\colon K \to I)\) to \((X,gr\colon K \to J)\).

Indeed, in the backwards case the displayed pullback is precisely the factorization of the composite span used in Proposition 17.2.8. In the forward case, the composite \(gr\) already belongs to \(F_R\), so its factorization has left factor \(\id _K\) and the cocartesian lift leaves \(X\) unchanged. Consider now a collection of objects \(J_1, \dots , J_n\) and let \(J := \bigsqcup _{i=1}^n J_i\). We must show that the map \[ (F_R)_{/J} \times _{\Span _{L,R}(F)} \Oo ^{\otimes } \to \prod _{i=1}^n (F_R)_{/J_i} \times _{\Span _{L,R}(F)} \Oo ^{\otimes } \] is an equivalence.

Essential surjectivity: Consider an object \((X_i,r_i\colon I_i \to J_i)_{i=1}^n\) of the target. We define \(I := \bigsqcup _{i=1}^n I_i\), let \(r\colon I \to J\) be the map whose \(i\)-th component is \(r_i\), and we let \(X \in \Oo ^{\otimes }_I\) correspond to the tuple \((X_i)_{i=1}^n\) under the equivalence \(\Oo ^{\otimes }_I \iso \prod _{i=1}^n \Oo ^{\otimes }_{I_i}\) from condition (2) of Definition 17.3.10. Then \((X,r\colon I \to J)\) is the desired preimage.

Full faithfulness: Consider two objects \((X,r\colon I \to J)\) and \((X',r'\colon I' \to J)\) of \((F_R)_{/J} \times _{\Span _{L,R}(F)} \Oo ^{\otimes }\). We must show that the map \[ \Hom _{(F_R)_{/J}}(I,I') \times _{\Hom _{\Span _{L,R}(F)}(I,I')} \Hom _{\Oo ^{\otimes }}(X,X') \to \prod _{i=1}^n \Hom _{(F_R)_{/J_i}}(I_i,I'_i) \times _{\Hom _{\Span _{L,R}(F)}(I_i,I'_i)} \Hom _{\Oo ^{\otimes }}(X_i,X'_i) \] is an equivalence. Extensivity of \(F\) gives an equivalence \(F_{/J} \simeq \prod _i F_{/J_i}\). It restricts to the displayed slices of \(F_R\): membership in \(F_R\) is preserved by base change along the inclusions \(J_i \hookrightarrow J\) by adequacy, and is detected on the resulting components because \(F_R\) is closed under finite coproducts by weak coextensivity. Consequently \((F_R)_{/J} \to \prod _{i=1}^n (F_R)_{/J_i}\) is an equivalence, and hence there is a natural equivalence \[ \Hom _{(F_R)_{/J}}(I,I') \simeq \prod _{i=1}^n \Hom _{(F_R)_{/J_i}}(I_i,I'_i). \] It thus remains to show that this map induces equivalences on fibers for every map \(f \in \Hom _{(F_R)_{/J}}(I,I')\). Condition (3) of Definition 17.3.10 identifies the relevant fiber with the product of the fibers of \(\Hom _{\Oo ^\otimes }(X,X'_i)\) over the spans \(I \leftarrow I_i \to I'_i\). Cocartesian transport along the backwards spans \(I \leftarrow I_i \xrightarrow {=} I_i\) then identifies these fibers with those of \(\Hom _{\Oo ^\otimes }(X_i,X'_i)\) over the forward spans \(I_i \to I'_i\). This is precisely the map on fibers displayed above, so it is an equivalence. □

Proof. This is a special case of the previous proposition. For \(\Ff = (\Fin ,\Fin ,\Fin )\), Proposition 14.1.9 identifies the objects of \(\Op _{\Ff }\) with the \(\infty \)-operads from Definition 14.1.1, while Corollary 14.1.11 identifies the two notions of morphism. □

Proof. Let \(E\) be an \(\infty \)-category. Using Lemma 14.2.12, the adjunction of Proposition 17.3.13, and currying, we obtain natural equivalences \begin {align*} \Hom _{\Cat _{\infty }}(E,\Alg _{\Oo }(C)) &\simeq \Hom _{\Op _\infty }(\Oo ,\Mm _{\Fun (E,C)}) \\ &\simeq \Map ^\otimes (\Env (\Oo ),\Fun (E,C)) \\ &\simeq \Hom _{\Cat _{\infty }}(E,\Fun ^\otimes (\Env (\Oo ),C)). \end {align*}

Here \(\Fun (E,C)\) carries the pointwise symmetric monoidal structure. Since these equivalences are natural in \(E\), the Yoneda lemma gives the claimed equivalence of \(\infty \)-categories. □

Proof. Under the Segal equivalence, the two tuples on the left determine the object of the fiber over \(\lra {2}\) indexed by their disjoint union \(I \sqcup J\). The tensor product is cocartesian transport of this object along the forward fold span \(\lra {2} \xleftarrow {=} \lra {2} \to \lra {1}\). By the forward-transport calculation in the proof of Proposition 17.3.12, this transport leaves the object of \(\Oo ^\otimes \) unchanged and postcomposes its indexing map with the fold map. The result is the concatenated tuple. The same calculation for the unique forward map \(\emptyset \to \lra {1}\) gives the empty tuple as the unit. □

Proof. The total category of the terminal operad \(\Comm \) is \(\Span (\Fin )\) itself. The pullback description of the underlying category of the envelope therefore gives \(\Env (\Comm ) \simeq \Fin \), and Lemma 17.3.15 identifies the tensor product with disjoint union. □

Proof. As noted above, the underlying \(\infty \)-category of \(\Env (\Oo )\) is the pullback \(\Fin \times _{\Span (\Fin )} \Oo ^{\otimes }\) along the inclusion \(\Fin \hookrightarrow \Span (\Fin )\) of the forward spans. Consequently, \(\Hom _{\Env (\Oo )}(\{x_i\}_{i \in I}, \{y_j\}_{j \in J})\) is the pullback of \[ \Hom _{\Oo ^{\otimes }}(\{x_i\}_{i \in I}, \{y_j\}_{j \in J}) \longrightarrow \Hom _{\Span (\Fin )}(I,J) \] and the subanima \(\Hom _{\Fin }(I,J)\) of forward spans, which produces the coproduct over the maps \(f\colon I \to J\). Fixing such an \(f\), condition (3) of Definition 17.3.10 identifies the fiber over \(f\) with the product over \(j \in J\) of the fibers of \(\Hom _{\Oo ^{\otimes }}(\{x_i\}_{i \in I}, y_j)\) over the span \(I \hookleftarrow f^{-1}(j) \to \lra {1}\). Cocartesian transport along the inert morphism \(\{x_i\}_{i \in I} \to \{x_i\}_{i \in f^{-1}(j)}\) identifies the latter fiber with the multimorphism anima \(\Oo (\{x_i\}_{i \in f^{-1}(j)}; y_j)\). The final statement is the case \(J = \lra {1}\). □

Proof. The full faithfulness is an instance of Lemma 17.2.11. To identify the essential image, we first show that the two conditions are always satisfied for \(C = \Env (\Oo )\). Condition (1) follows from the Segal condition on \(\Oo \) and Lemma 17.3.15: the underlying map \(\Env (\Oo ) \to \Fin \) is simply the pullback of the map \(\Oo ^{\otimes } \to \Span (\Fin )\). For condition (2), let us write \(X := \bigotimes _{j\in J} X_j\) and \(Y := \bigotimes _{j \in J} y_j\), where these two tensor products in \(C = \Env (\Oo )\) are computed as unordered concatenations in \(\Oo ^{\otimes }\). Then we have a pullback square

The claim now follows from condition (3) of Definition 17.3.10.

It remains to show that any \(C\) satisfying (1) and (2) is of the form \(\Env (\Oo )\) for some \(\infty \)-operad \(\Oo \). We define \(\Oo \) as the following pullback:

The pullback is formed in \((\Cat _\infty )_{/\Span (\Fin )}\). It is again an \(\infty \)-operad: cocartesian lifts of backwards spans are formed componentwise, the Segal equivalences on fibers are preserved by pullback, and condition (3) is inherited by taking pullbacks of the corresponding squares. Here the bottom map is the unit of the adjunction \(\Env \dashv \Mm \). The projection \(\Oo \to \Mm _C\) induces a composite of symmetric monoidal functors \[ \Env (\Oo ) \longrightarrow \Env (\Mm _C) \longrightarrow C, \] where the second map is the counit of the adjunction. Equivalently, this is the symmetric monoidal functor corresponding under Corollary 17.3.14 to the projection \(\Oo \to \Mm _C\). Naturality of the counit with respect to \(p\) shows that this composite is a functor over \((\Fin ,\amalg )\). We show that it is an equivalence.

The colors of \(\Oo \) are precisely the objects of \(C_{\lra {1}}\). Since every object of \(\Env (\Oo )\) is a tensor product of colors, essential surjectivity follows from condition (1) on \(C\). For full faithfulness, first consider a target color \(y\in C_{\lra {1}}\). We have equivalences: \[ \Hom _{\Env (\Oo )}(\{x_i\},y) \simeq \Oo (\{x_i\};y) \simeq \Hom _C(\bigotimes _{i \in I} x_i, y) \] The first is Lemma 17.3.17. For the second, the pullback defining \(\Oo \) identifies its multimorphism anima with the fiber of \[ \Hom _C(\bigotimes _{i \in I}x_i,y) \longrightarrow \Hom _{\Fin }(I,\lra {1}) \] over the unique map \(I\to \lra {1}\); this fiber is the entire source because the target is contractible.

For a general target \(\{y_j\}_{j\in J}\), Lemma 17.3.17 decomposes the hom anima in \(\Env (\Oo )\) as a coproduct indexed by maps \(f\colon I\to J\), with the fiber over \(f\) equal to \[ \prod _{j\in J} \Hom _C\left (\bigotimes _{i\in f^{-1}(j)}x_i,y_j\right ). \] Condition (2) identifies this product with the fiber over \(f\) of \[ \Hom _C\left (\bigotimes _{i\in I}x_i,\bigotimes _{j\in J}y_j\right ) \longrightarrow \Hom _{\Fin }(I,J). \] Taking the coproduct over all \(f\) proves full faithfulness. □