Comparison to Lurie's operads

Proof. Condition (1) in the two definitions is the same. Suppose first that \(p_{\Oo }\colon \Oo ^\otimes \to \Fin _*\) is an \(\infty \)-operad in the sense of Lurie. The functor \[ \Oo ^\otimes _J \longrightarrow \prod _{j \in J}\Oo ^\otimes _{\{j\}} \] induced by cocartesian transport along the Segal maps is essentially surjective by condition (3) of Definition 17.4.3. It is fully faithful as well: condition (2), restricted to the fiber over \(\id _{J_+}\), identifies the hom anima in \(\Oo ^\otimes _J\) with the product of the hom animae in the fibers over the singletons, using cocartesian transport along the Segal maps on the sources. Thus condition (2) holds for the decomposition of \(J\) into singletons, and hence for every finite decomposition by grouping the singleton factors. Condition (3) follows similarly from condition (2): apply it to the singleton decomposition of \(J\) and to those of the summands \(J_i\), and group the resulting factors according to \(J = \bigsqcup _i J_i\).

Conversely, if \(\Oo \) is an \(\Ff _{\mathrm {Lurie}}\)-operad, condition (1) gives the required cocartesian lifts of inert maps. Specializing condition (3) to the decomposition of \(J\) into singletons gives condition (2) of Definition 17.4.3, while condition (2) gives condition (3). Finally, both notions of morphism require precisely the preservation of cocartesian morphisms over inert maps. □

Proof. Any \(p_{\Oo }\)-cocartesian lift of a backwards span \(I \hookleftarrow J \xrightarrow {=} J\) will still be \(p_{\Pp }\)-cocartesian, verifying condition (1). Condition (2) is immediate from Lemma 14.1.10. Condition (3) is immediate from condition (ii) in Proposition 14.1.9. The claim on morphisms is checked similarly. □

Proof. By the pullback formula in Construction 17.2.2, it suffices to construct a natural equivalence \[ \Fin _* \times _{\Span (\Fin ),t}\Ar _{\Rr }(\Span (\Fin )) \simeq \Ar _{\Rr _*}(\Fin _*) \] over \(\Fin _*\). The objects on both sides are forward spans, equivalently maps of finite sets \(r\colon I \to J\). A morphism on the left is a commutative square in \(\Span (\Fin )\)

in which \(g\) belongs to \(\Fin _*\). The composite \(gr\) has injective backwards leg because this leg is obtained by pulling back the injective backwards leg of \(g\) along \(r\). Since \(r'\) is forward, the backwards leg of \(r'f\) is the backwards leg of \(f\). The equivalence \(r'f \simeq gr\) therefore shows that \(f\) also belongs to \(\Fin _*\). As \(\Fin _* \hookrightarrow \Span (\Fin )\) is a wide subcategory inclusion, its hom animae are unions of components, so the homotopy making the square commute also lies in \(\Fin _*\). Thus the displayed square is precisely a morphism in \(\Ar _{\Rr _*}(\Fin _*)\), which proves the claim. □

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

Proof. Define a classical 1-category \(\Oo ^{\otimes ,\mathrm {Lurie}}\) as in Construction 12.4.1, with the additional requirement that in the underlying span \(I \xleftarrow {f} K \xrightarrow {g} J\) the finite set \(K\) is an actual subset of \(I\) and \(f\) is its inclusion. Composition is defined as in Construction 12.4.1, taking as the pullback of spans the literal preimage: the composite of \((K \subseteq I, g\colon K \to J)\) with \((M \subseteq J, k\colon M \to L)\) has underlying subset \(g^{-1}(M) \subseteq K \subseteq I\) and underlying map the restriction of \(k \circ g\) to it. This is again a subset inclusion, and the resulting composition is strictly associative: composing with a third morphism \((N \subseteq L, l\colon N \to P)\) in either of the two possible orders yields the subset \(g^{-1}(k^{-1}(N)) \subseteq I\), together with the restriction of \(l \circ k \circ g\). The identity of \(\{x_i\}_{i \in I}\) is given by \(K = I\) and \(g = \id _I\), labeled by identity multimorphisms. On the level of the multimorphism labels, associativity and unitality of this composition are precisely the associativity and unitality axioms of the colored operad \(\Oo \). Thus \(\Oo ^{\otimes ,\mathrm {Lurie}}\) is a classical 1-category. Sending \(\{x_i\}_{i \in I}\) to \(I_+\) and a morphism \((K \subseteq I, g, \{\phi _j\}_{j \in J})\) to the pointed map \(I_+ \to J_+\) that restricts to \(g\) on \(K\) and sends \(I \setminus K\) to the basepoint defines a functor of 1-categories \[ p_{\Oo }\colon \Oo ^{\otimes ,\mathrm {Lurie}} \longrightarrow \Fin _*. \] Its fiber over \(I_+\) consists of the \(I\)-tuples of colors of \(\Oo \) and the \(I\)-tuples of unary multimorphisms between them, i.e. it is the \(I\)-fold power of the category of colors and unary multimorphisms of \(\Oo \). For an inert morphism, the morphism obtained by restricting an \(I\)-tuple of colors and labeling the resulting unary operations by identities is \(p_{\Oo }\)-cocartesian. These cocartesian lifts give the required equivalences from the fiber over \(I_+\) to the product of the fibers over its elements.

It remains to verify the condition on morphism sets. Let \(X=\{x_i\}_{i\in I}\) and \(Y=\{y_j\}_{j\in J}\). For a pointed map \(\alpha \colon I_+\to J_+\), the set of morphisms \(X\to Y\) over \(\alpha \) is, by construction, \[ \prod _{j\in J} \Oo \bigl ((x_i)_{i\in \alpha ^{-1}(j)};y_j\bigr ). \] The \(j\)-th factor is precisely the set of morphisms from \(X\) to \(y_j\) over the composite of \(\alpha \) with the Segal map \(\rho _j\). Consequently the square in condition (2) of Lurie’s definition is a pullback. Thus \(p_{\Oo }\) is an \(\infty \)-operad in Lurie’s sense. A morphism of colored operads acts on tuples and multimorphism labels and thereby induces a functor between the resulting categories over \(\Fin _*\). Applying an inverse to the equivalence in Proposition 17.4.8 therefore produces the claimed functor from colored operads to \(\infty \)-operads over \(\Span (\Fin )\). □

Proof. Apply Proposition 17.4.9 to each of the indicated colored operads. The comparison with the span model is induced by restriction along \(\Fin _* \hookrightarrow \Span (\Fin )\) and therefore preserves the fibers of hom animae over active maps. The displayed formula in the proof of Proposition 17.4.9 consequently identifies the resulting multimorphism animae with the discrete animae associated with the classical multimorphism sets. □

Proof. Both envelopes have the unordered tuples of colors as objects. The description of the classical morphism sets in Definition 12.3.3 agrees with the mapping-anima formula of Lemma 17.3.17, since the latter is discrete for a classical colored operad. These identifications respect composition, and both tensor products are given by concatenation of tuples. □