The n-Category Café

If there’s a problem, it’s because its not a model for a theory, which is why I posed it the way I did.

Mike wrote:

But anyway, if that’s your convention, then why are you talking about multi-sorted operads right now? I don’t see any maps between operads here except for the models, which are functors $O\to Set$ that certainly don’t preserve the sorts.

Maybe I’m thinking about it suboptimally, but I like to fix a set $S$ of sorts, and study $S$-sorted operads, which have models (= algebras) in $Set^S$. I also like to study $S$-sorted PROPs and $S$-sorted Lawvere theories, which also have models in $Set^S$. If $T$ is any $S$-sorted operad or PROP or Lawvere theory, I like to think about its category $Mod(T)$ of models, which comes with an adjunction

$$U : Mod(T) \to Set^S$$ $$F : Set^S \to Mod(T)$$

with lots of great properties.

I can easily imagine wanting to integrate the setups for different choices of $S$ into a larger setup where you have sort-changing maps $S \to S'$, or simply downplay the importance of sorts and with symmetric multicategories, symmetric monoidal categories and cartesian categories instead of $S$-sorted operads, PROPs and Lawvere theories. But in my work these days, which focuses on applications to engineering and chemistry, I seem pretty happy with an ‘$S$-centric’ viewpoint, often with $S = 1$.

Maybe you can show me some slicker setup that doesn’t have too much conceptual overhead.

No, I don’t think I’ll try to sell you anything “slicker”. I tend to want to “downplay the importance of sorts” as you said, probably mainly because I’m interested in “models” of the same theory that live in all sorts of different places; so I can talk about them all as being functors of multicategories with the same domain and different codomains. But certainly if we fix both the domain multicategory $T$ and the codomain multicategory $Set$, then the category of functors $T\to Set$ is related to the category $Set^{ob(T)}$ by a nice adjunction, and if this is what you’re interested in then it makes sense to focus on it.

This dichotomy already appears for ordinary categories. If $T$ is an ordinary category then we can talk about functors with domain $T$ and arbitrary codomain, but if we fix a sufficiently cocomplete codomain category like $Set$, then the category of functors $T\to Set$ is monadic over $Set^{ob(T)}$, and both points of view are important. (But even when taking the second point of view, we don’t call $T$ an “$S$-sorted monoid”…)

Now that I think about it, perhaps the physical universe is mathematics done without terminology or notation.

Has anyone made a serious stab at connecting relevance monoidal categories to relevance logic?

Of course, this connection is where the name comes from. But I guess you’re asking whether anyone has made this connection totally precise in writing. The answer is that I don’t know a reference that works out all the details.

I think it’s a fairly easy exercise to show the posetal case, that relevance monoidal posets are the semantics of proof-irrelevant relevance logic. But the “proof-relevant” versions of “partially substructural” type theories like relevance logic and affine logic (which corresponds to semicartesian monoidal categories) are sometimes a bit fiddly, and I haven’t seen it done carefully. But maybe some other reader of the blog will supply a reference!

Relevance logic is a special case of the general framework for modal/substructural logics that Dan Licata, Mitchell Riley, and I described here, so in a certain sense our theorem about semantics applies to it. However, the semantics used there doesn’t usually correspond directly to the “correct” categorical semantics, plus the syntax is a bit different from the usual one too. (We’re working on an improved framework that will hopefully solve these problems.)

After writing out the post below, I found a good reference (for the single-sorted case): Proposition 7.3 in Harper, “Homotopy theory of modules over operads and non-$\Sigma$-operads in monoidal model categories”, JPAA 2010. There he actually does the generalization to pushouts of diagrams of the form $M \leftarrow F(X) \rightarrow F(Y)$.

Lemme write down what’s true in the single-sorted case; maybe that will prod somebody to write it down (or remember seeing it) in the general case.

• Let $\Sigma=$ the groupoid of finite sets and isomorphisms between them (or use a skeleton of it).

• A symmetric sequence is a functor $\Sigma\to \mathrm{Set}$.

• Every symmetric sequence $A$ determines a functor $$\Phi_A\colon \mathrm{Set}\to\mathrm{Set},\qquad \Phi_A(X) = \mathrm{Coend}_{\Sigma}(A, N\mapsto X^N) \approx \coprod_{n\geq0} (A(\underline{n})\times X^\underline{n})_{S_n},$$ where $\underline{n}=\{1,\dots,n\}$, and $S_n=\mathrm{Aut}(\underline{n})$.

• There’s a (nonsymmetric) monoidal structure on $\mathrm{Fun}(\Sigma,\mathrm{Set})$ denoted by $\circ$, so that $\Phi_{A\circ B}\approx \Phi_A\Phi_B$. (There’s a formula, but I’m not going to write it out.)

• Operads are just monoids in the monoidal category of symmetric sequences.

• Fix an operad $O$, an $O$-algebra $M$, and a set $X$. We are interested in $$U(M+F(X)),$$ the underlying set of the coproduct in $O$-algebras of $M$ with the free $O$-algebra on the set $X$.

• The formula is: $$U(M+F(X)) \approx \Phi_T(X) \approx \coprod_{n\geq0} (T(\underline{n})\times X^{\underline{n}})_{S_n}$$ where $T=T_{O,M}$ (the “Taylor series”) is a certain symmetric sequence depending on $O$ and $M$, which I’ll describe below. It turns out that $T(\underline{0})=U(M)$, and that $M\to M+F(X)$ is inclusion of this $0$th summand.

• Given a symmetric sequence $O$ and a finite set $N$, let $D^N O$ (the “$N$-th derivative”) be the symmetric sequence defined by $$D^N O(M) = O(M\amalg N).$$ Note that $N\mapsto D^N O$ is itself a functor $\Sigma\to \Fun(\Sigma, \mathrm{Set})$. I.e., $D^{\underline{n}} O$ has an additional action by the symmetric group $S_n$ (which corresponds to “dividing by $n!$”).

• If $O$ is an operad, then the product map $O\circ O\to O$ gives rise to a map $D^N O\circ O\to D^N O$, which makes $D^N O$ into a “right module” over $O$. (Since I didn’t give the formula for $\circ$ I can’t give the formula for this. In any case, it’s best to picture it in terms of “grafting trees”, where the “inputs” corresponding to the label set $N$ are never used.)

• Now we can define $T(N)$. It is the coequalizer in sets of the pair of maps $$\Phi_{D^N O} \Phi_O (M) \rightrightarrows \Phi_{D^N O}(M),$$ induced by (i) the right $O$-module structure on $D^N O$ and (ii) the $O$-algebra structure on $M$.

I like to write this as $T(N)=(D^N O)\circ_O M$, so that the whole formula becomes $$U(M+F(X)) \approx \coprod_{n\geq0} ((D^n O)\circ_O M) \times X^n)_{S_n}.$$

Easy example: if $O$ is the commutative operad, then $D^n O\approx O$ as a right $O$-module (with trivial $S_n$ action), so $T(n)=(D^n O)\circ_O M \approx O\circ_O M \approx M$. The formula reduces in this case to $$U(M+F(X)) \approx \coprod_{n\geq0} U(M)\times (X^n)_{S_n} \approx U(M)\times U(F(X)).$$

Another example: if $O$ is the associative operad, then $$D^n O \approx \coprod_{S_n} O^{\otimes (n+1)},$$ where “$\otimes$” is yet another monoidal structure on symmetric sequences, with the property that $\Phi_{A\otimes B}(X)=\Phi_A(X)\times \Phi_B(X)$. This monoidal structure lifts to one on right $O$-modules, and in the above case we have an isomorphism $$O^{\otimes (n+1)} \approx I^{\otimes (n+1)} \circ O$$ of right $O$-modules, where $I$ is the symmetric sequence such that $\Phi_I\approx \mathrm{Id}$. Putting it together, we recover $$U(M+F(X)) \approx \coprod_{n\geq0} M^{n+1}\times X^n.$$

BTW, there is nothing special about sets here. This works in any closed symmetric monoidal category.

Interesting!

So back to the original motivation, can one just apply the left adjoints to $Bij^{op}$ to confirm John’s hunches?

I think I can prove my hunches ‘directly’, by showing that skeletons of $Inj^{op}$ and $Surj^{op}$ are PROPs with the presentations one would expect from them being the free semicartesian monoidal category on one object and the free relevance monoidal category on one object. The proofs seem to be hovering in my eyelids when I close my eyes, but it would take some work to fill in the details and write them up.

Since every function factors as an injection followed by a surjection, the PROP $FinSet^{op}$ should be ‘composed’ (in Steve Lack’s sense) of the PROPs $Inj^{op}$ and $Surj^{op}$. $FinSet^{op}$ is the PROP for cococommutative comonoids, and if my story hangs together, $Surj^{op}$ will be the PROP for cocommutative cosemigroups, while $Inj^{op}$ will be the PROP for ‘pointed’ objects.

This stuff is nice enough, and simple enough, that I should check to see if it’s already known!

I agree with Todd that the left adjoints should exist for formal reasons (which makes them rather inexplicit and probably not helpful for computing particular free objects). All four kinds of monoidal category are accessibly 2-monadic over Cat. Thus, the adjoint lifting theorem implies that the forgetful functors between the categories of such monoidal categories and strict monoidal functors has a left adjoint. A weak left adjoint between the corresponding 2-categories with pseudo monoidal functors can then be derived using the pseudo morphism classifier, as in Blackwell-Kelly-Power “Two-dimensional monad theory” (Theorem 5.12).