Envelope definition

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