Proposition 17.4.8 (cf. [Barkan et al. (2022), Theorem 5.1.1, Corollary 5.1.15]). The forgetful functor \(\Op _{\infty } \to \Op _{\infty }^{\mathrm {Lurie}}\) is an equivalence.
Proof. By Lemma 17.4.4, we may work with \(\Ff _{\mathrm {Lurie}}\)-operads. The proof of Proposition 17.3.18 applies to this span pattern as well. Indeed, full faithfulness is the general statement Lemma 17.2.11; the Segal and mapping-anima arguments use only conditions (2) and (3); and the forward-transport calculation of Lemma 17.3.15 applies unchanged. After the equivalence of Proposition 5.3.9, we therefore obtain a fully faithful functor \[ \Env ^{\mathrm {Lurie}}\colon \Op _\infty ^{\mathrm {Lurie}} \longrightarrow (\Cat _\infty ^\otimes )_{/(\Fin ,\amalg )} \] with essential image characterized by the two conditions in Proposition 17.3.18.
Now let \(u\colon \Fin _* \hookrightarrow \Span (\Fin )\) be the inclusion and let \(\Oo \) be an \(\infty \)-operad over \(\Span (\Fin )\). Applying Lemma 17.4.7 to \(p_{\Oo }\) gives a natural equivalence of \(\Ff _{\mathrm {Lurie}}\)-monoidal \(\infty \)-categories \[ \Env ^{\mathrm {Lurie}}(u^*\Oo ) \simeq u^*\Env (\Oo ). \] Under Proposition 5.3.9, the right-hand side corresponds to the original symmetric monoidal \(\infty \)-category \(\Env (\Oo )\). The equivalence is compatible with the maps to \((\Fin ,\amalg )\) by naturality of the construction. We therefore obtain a naturally commutative diagram
Both diagonal functors are equivalences onto the same essential image. It follows by 2-out-of-3 that the left vertical functor is an equivalence, as desired. □
Generated from the authoritative LaTeX source.