August 27, 2017

A Puzzle on Multi-Sorted Lawvere Theories

Posted by John Baez

I hope you know that a Lawvere theory is a category $T$ with finite products where the objects are all of the form $x^n$ for some object $x$. A model of $T$ is a finite-product-preserving functor $M : T \to \Set$. There’s a category $Mod(T)$ where the objects are models and the morphisms are natural transformations between such functors. Many familiar algebraic structures defined by $n$-ary operations and equations, like groups or vector spaces over some field $k$, can be seen as models of Lawvere theories. So, there’s a Lawvere theory $T$ for which $Mod(T)$ is equivalent to $Grp$, another one that gives $Vect_k$, and so on.

Categories of this sort have been studied a lot and are sometimes called finitary monadic categories or finitary algebraic categories (though sometimes the latter term is used more generally — see the link). These categories always have coproducts, so it’s natural to wonder when the canonical morphism

$i: M \to M + N$

is monic. After all, it’s true in $Grp$ and $Vect_k$, and in enough other cases that people sometimes call $i$ the ‘inclusion’ of an object $M$ in $M + N$.

But $i: M \to M + N$ is not always monic in the category of models of a Lawvere theory. Can you think of a counterexample before read on?

Okay, here’s one: it’s not always monic in the category $CommRing$, where the coproduct is the familiar ‘tensor product’ of commutative rings. Consider the commutative rings $\mathbb{Q}$ and $\mathbb{Z}/2$; then $\mathbb{Q} \otimes \mathbb{Z}/2 = \{0\}$, since we always have

$a \otimes b = \frac{1}{2}a \, \otimes \, 2b = 0$

so of course the canonical morphism $\mathbb{Q} \to \mathbb{Q} + \mathbb{Z}/2$ is not monic.

However, something weaker is true. For any Lawvere theory $T$ there’s a forgetful functor

$U : Mod(T) \to Set$

$F : Set \to Mod(T)$

giving a monad $U F$ on $Set$ whose category of algebras is equivalent (in a standard sort of way) to $Mod(T)$.

So, we can talk about ‘free’ models of $T$, and it turns out that the canonical morphism

$M \to M + N$

is monic when $N$ is free.

Proposition. If $T$ is a Lawvere theory, $M \in Mod(T)$ and $X \in Set$, the canonical morphism $i: M \to M + F(X)$ is monic.

I would like, just for the sake of my happiness, to know that this proposition generalizes to multi-sorted Lawvere theories. These are like ordinary Lawvere theories except instead of describing a single set with $n$-ary operations obeying equations, they describe a bunch of sets with $n$-ary operations obeying equations. For example, there’s a 2-sorted Lawvere theory that describes ring-module pairs. A model of this theory is a ring together with a module of that ring.

Here’s the definition: a multi-sorted Lawvere theory with $S$ as its set of sorts is a category with finite products where every object is a finite product of some chosen objects $\{x_\lambda\}_{\lambda \in S}$. So, if $S = 1$ we’re back to an ordinary Lawvere theory, and if $S = 2$ we have a 2-sorted Lawvere theory, and so on. Click the link if you want a more conscientious definition… but honestly, I’m not leaving out anything.

A model of an $S$-sorted Lawvere theory $T$ is a functor $M : T \to \Set^S$. Again we get a category $Mod(T)$ with these models as objects and natural transformations as morphisms. Again we have a forgetful functor

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

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

Here’s my guess:

Conjecture. If $T$ is an multi-sorted Lawvere theory with $S$ as its set of sorts, $M \in Mod(T)$ and $X \in Set^S$, the canonical morphism $i: M \to M + F(X)$ is monic.

Can you prove this? One approach would be to actually ‘build’ $M + F(X)$ in a very concrete way as an $S$-tuple of sets equipped with a bunch of $n$-ary operations, then look at the underlying morphism

$U(i): U(M) \to U(M + F(X))$

in $Set^S$ and show this is monic. That would do the job: since $U$ is faithful it reflects monics. And it’s easy to check if a morphism in $Set^S$ is monic: it’s an $S$-tuple of functions, and they all need to be monic. But it would be nice to find a less grungy proof.

Todd Trimble found a very quick proof for the unsorted case, but curiously, it doesn’t obviously generalize to this case. Nonetheless, he figured out how to handle the case I actually needed: I’m studying PROPs, which are models of a certain multi-sorted Lawvere theory, and I needed to show that for any PROP $M$ and any free PROP $F(X)$, the canonical morphism $i : M \to M + F(X)$ is monic. In fact Todd’s argument applies to any multi-sorted Lawvere theory that comes from a multi-sorted operad, more commonly called a colored operad.

Any good ideas?

Posted at August 27, 2017 10:59 AM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2979

Re: A Puzzle on Multi-Sorted Lawvere Theories

I don’t know what the very elegant proof is in the unsorted case. But: would it apply to your setup in the case that $X$ only has elements of a single sort? If so, the result would follow (using that filtered colimits in $Mod(T)$ commute with $U$).

Posted by: Charles Rezk on August 27, 2017 4:34 PM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

We may as well mention how some of the arguments we’ve found go, because they are pretty simple.

A very simple case is where we have an ordinary (unsorted) Lawvere theory $T$. Let $M$ be a $T$-algebra and $X$ be a set. Then the coproduct coprojection $M \to M + F(X)$ is monic because this comes down to checking injectivity at the level of underlying sets and functions. There, either $M$ is empty and the injectivity is trivial, or $M$ is inhabited and then we can split the coprojection: all we need to do is construct an algebra map $F(X) \to M$, where this is tantamount to constructing a function $X \to U(M)$, which we can do because $U(M)$ has at least one element.

However, I don’t know a simple way to extend this simple-minded argument to the case of general $S$-sorted Lawvere theories.

It’s not very difficult to augment this argument to handle the case where $T$ is an $S$-sorted Lawvere theory that comes from an $S$-sorted operad (aka, a multicategory). It’s based on a trick of adjoining elements to enforce inhabitation: if $M$ is a $T$-algebra, we can form a new $T$-algebra $M^\ast$ by putting

$M^\ast(s) = M(s) \sqcup \{x_s\}$

where $x_s$ denotes an element we adjoin, and defining the $T$-algebra structure on $M^\ast$ as follows: if $\theta \in T(s_1, \ldots, s_n; s)$ belongs to the $S$-sorted multicategory, then the corresponding operation

$M^\ast(s_1) \times \ldots \times M^\ast(s_n) \to M^\ast(s),$

when applied to a tuple of elements $m_i \in M^\ast(s_i)$, agrees with the operation on $M$ in case all the $m_i$ belong to $M(s_i)$; if on the other hand $m_i = x_{s_i}$ for some $i$, then the tuple is taken to $x_s$. (In other words, the $x_s$ behave like “absorbing elements”, in the same way that $0$ is an absorbing element for the multiplication operation in a ring.) One can check readily that this really works.

With that construction in hand, we can finish proving that the coprojection $j: M \to M + F(X)$ is monic for any $X$. It’s basically a variation on the proof we gave before, where we split a coprojection in the unsorted case. We have just constructed a monic $T$-algebra map $i: M \to M^\ast$. Now extend this to a map $k: M + F(X) \to M^\ast$: we just need a $T$-algebra map $F(X) \to M^\ast$, which we could take to be the one corresponding to the map $X \to U(M^\ast)$ whose component $X(s) \to U(M^\ast)(s)$ is the function taking all of $X(s)$ to $x_s$. Then, we have $i = k \circ j$, and since $i$ is monic, so must be the coprojection $k: M \to M + F(X)$.

However, this idea of adjoining absorbing elements doesn’t work in the greater generality of $S$-sorted Lawvere theories $T$. It doesn’t even work in the unsorted case where $T$ is the theory of groups, since groups can’t have absorbing elements. So some other method would be needed in that generality.

Posted by: Todd Trimble on August 27, 2017 4:35 PM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

Consider a category whose objects are data $(R,S,f)$ where:

1. $R$ is a commutative ring,

2. $S$ is a set, and

3. $f\colon S\to R$ is a function such that:

4. $f(s)=0$ for all $s\in S$, and

5. $f(s)=1$ for all $s\in S$.

Is this an example of models for a 2-sorted theory? If so, I’d think it would be a counterexample.

Posted by: Charles Rezk on August 27, 2017 4:50 PM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

Posted by: Todd Trimble on August 27, 2017 4:56 PM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

They are not contradictory, since it is possible for $0=1$ in a commutative ring (namely, when $R$ has only one element).

So objects are of two types: (i) $R$ any commutative ring and $S=\varnothing$, or (ii) $R=\{0\}$ and $S$ any non-empty set.

Posted by: Charles Rezk on August 27, 2017 5:05 PM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

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.

Posted by: Charles Rezk on August 27, 2017 5:10 PM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

Oh, wait: not so fast Todd. Let me see if I understand what looks like a potentially clever idea here.

Yes, that looks like a perfectly acceptable 2-sorted theory.

What are the possible models? Well, $R$ could be any commutative ring and $S$ is empty. Or, $R$ could be the terminal ring (where $0 = 1$) and $S$ could be any set.

Okay, then, what does the free model on a pair of sets $(A, B)$ look like? A map $(A, B) \to U(R, S, f)$ is a pair of functions $A \to R$, $B \to S$. If $B$ is inhabited, then $S$ here cannot be empty, so we must be in the case where $R$ is terminal. In particular, when we come to consider the unit $(A, B) \to U F(A, B)$ of the monad, we see the ring-part of $F(A, B)$ has to be the terminal ring if $B$ is inhabited. And I guess the set-part of $F(A, B)$ is just $S$, so the unit here is the pair of maps $(A \to 1, id: B \to B)$.

On the other hand, if $B$ is empty, then it looks like the ring-part of $F(A, B)$ is the polynomial ring $\mathbb{Z}[A]$ with $A$ as the set of indeterminates, and the set-part is $S = \emptyset$.

Pressing on: now let’s consider the coproduct coprojection

$(R, S) \to (R, S) + F(A, B)$

where $B$ is inhabited. Well, I’m guessing the point now is that the ring-part of the coproduct is forced to be terminal, so the underlying function between the ring-parts is $R \to 1$, which for general $R$ is not monic.

So: aha! I guess I want to mull over this a bit longer, but it seems very clever and seems to answer John’s question negatively. Very nice, Charles!

Posted by: Todd Trimble on August 27, 2017 5:29 PM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

Possibly you could present this as two unary operations, f and f’, say and then force them to be equal. I’m just trying to think of what the Lawvere theory would look like, given your presentation, and not coming up successful at this point of the morning.

Posted by: David Roberts on August 27, 2017 11:27 PM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

The Lawvere theory here is generated by two objects $r, s$, and maps (“function symbols”) $+, \cdot: r \times r \to r$, and maps (“constants”) $0, e: 1 \to r$ (where the interpretation of $e$ in models will be the multiplicative identity), and finally a map $f: s \to r$. These are subject to the commutative ring equations, and also the equation which says the map $s \stackrel{f}{\to} r \stackrel{!}{\to} 1$ equalizes the two maps $0, e: 1 \rightrightarrows r$. When regarded as a presentation of a category with products, this gives a 2-sorted Lawvere theory.

Posted by: Todd Trimble on August 28, 2017 12:43 AM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

Ah, of course. Thanks :-)

Posted by: David Roberts on August 28, 2017 2:50 AM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

Thanks, Charles, for that nice counterexample!

For readers who are struggling to understand what’s going on, I feel an obligation to add that rings aren’t essential here. Charles was just using a ring because it’s the most familiar example of a set equipped with two constants. He could equally well have used the 2-sorted Lawvere theory for which a model is:

1. a set $R$ equipped with elements called $0$ and $1$,

2. a set $S$,

3. a function $f : S \to R$ such that

4. $f(s) = 0$ for all $s \in S$, and

5. $f(s) = 1$ for all $s \in S$.

(There is of course no requirement that $0$ and $1$ are distinct, since inequalities cannot be among the laws in a Lawvere theory.)

We can see that such gadgets are not described by a 2-sorted operad because equations 4. and 5. involve a variable on one side that doesn’t appear on the other side. It is these laws that ‘bite’ and sometimes force a model to ‘collapse’ when we take its coproduct with a free model.

Posted by: John Baez on August 28, 2017 2:36 AM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

The link in the second paragraph at the text “studied a lot” is broken.

Posted by: Blake Stacey on August 28, 2017 12:05 AM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

Thanks for catching that! The link goes here:

If you want a lot more, try:

Posted by: John Baez on August 28, 2017 1:21 AM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

Now that Charles has killed my conjecture for multi-sorted Lawvere theories, I’m happy to settle for what Todd has proved for multi-sorted operads.

Alas, these are usually known as colored operads, since people call their sorts ‘colors’. And to obscure the connection to multi-sorted Lawvere theories even further, people call the models of a colored operad ‘algebras’. There’s nothing like diverse and disorganized of terminology to hide the underlying unity and simplicity of mathematics!

So, in this jargon: any colored operad $O$ has a category $Alg(O)$ of algebras, and there’s a forgetful functor

$U : Alg(O) \to Set^C$

where $C$ is the set of colors. This functor $U$ is monadic, with left adjoint

$F : Set^C \to Alg(O)$

Moreover:

Theorem. If $O$ is a colored operad with $C$ as its set of colors, $M \in Alg(O)$ and $X \in Set^C$, the canonical morphism $i: M \to M + F(X)$ is monic.

Todd sketched the proof above.

Posted by: John Baez on August 28, 2017 4:49 AM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

And now I will reveal my secret reason for being interested in this somewhat technical issue.

My student Jason Erbele is using PROPs to study ‘control theory’, the branch of engineering where you design systems with feedback loops that help stabilize them:

Jason likes to describe PROPs using generators and relations. This raises a bunch of questions. For example: if I have a PROP $P$ presented in this way, and I throw in some extra generators but no extra relations, I get a new PROP $P'$ and a morphism of PROPs

$i : P \to P'$

Is this a monomorphism?

Yes, since PROPs are algebras of a colored operad, and we can use the theorem mentioned above to establish this:

Corollary. Suppose $O$ is a colored operad with $C$ as its set of colors, and let $F : Set^C \to Alg(O)$ be the left adjoint to the forgetful functor $U: Alg(O) \to Set^C$. Suppose we have a coequalizer in $Alg(O)$: $F(R) \stackrel{\to}{\to} F(G) \to P$ and a monomorphism $f : G \to G'$. Composing the unlabelled arrows above with $F(f)$, we get a new coequalizer: $F(R) \stackrel{\to}{\to} F(G') \to P'$ and thus by the universal property of $P$, a morphism $i: P \to P'$ This is a monomorphism.

I won’t give the proof here, since I’ll write it up and show y’all later.

So, we have a general situation where “adding new generators but not new relations cannot force previously unequal elements of an algebra to become equal”: it’s true for algebras of colored operads. Charles Rezk’s counterexample shows it ain’t generally true for models of multi-sorted Lawvere theories! But it is true for single-sorted Lawvere theories.

Posted by: John Baez on August 28, 2017 5:21 AM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

these are usually known as colored operads

Some of us prefer to call them “symmetric multicategories”. Our co-host Tom argued eloquently for this terminology in his book:

I prefer the term ‘multicategory’ because it emphasizes that we are dealing with a categorical structure, with objects and arrows. Moreover, although thinking of the objects as colours is practical when there is only a small, finite, number of them, it becomes somewhat baroque otherwise: in the multicategory of abelian groups, for instance, one has to paint each group a different colour (the real numbers are green, the cyclic group of order 10 is pink, and so on). This is not entirely a frivolous issue: the coloured viewpoint has given rise to eyebrow-raising statements such as

[…] it serves us well to have a subtle generalization of operad known as a bicolored operad. Still more colorful operads can be defined, but they are currently not of great importance

(Markl, Shnider and Stasheff [2002, p. 115]); of course, most of the coloured operads that one meets every day (Set, Top, R-Mod, …) have not just more than two colours, but a proper class of them. The quotation above is analogous to, and indeed includes, the statement that no important category has more than two objects.

We can also emphasize the relation to multi-sorted Lawvere theories by calling the latter cartesian multicategories.

Posted by: Mike Shulman on August 28, 2017 7:35 AM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

John wrote:

these are usually known as colored operads

Mike wrote:

Some of us prefer to call them “symmetric multicategories”.

I share your and Tom’s distaste for the term ‘colored operads’, but I make a slight mental distinction between multi-sorted operads and symmetric multicategories. When I talk about multi-sorted operads, I usually have some fixed set $S$ of sorts (= objects) in mind, so I’m actually talking about ‘$S$-sorted operads’, and the maps between $S$-sorted operads should preserve the sorts. When I talk about symmetric multicategories, I imagine the set of objects (= sorts) as variable, and the maps between symmetric multicategories don’t need to preserve the objects. It’s like the difference between multi-sorted Lawvere theories and categories with finite products.

(In fact I prefer the word ‘type’ to ‘sort’, but I don’t feel that’s a big deal.)

If someone could figure out how to do mathematics without terminology, just think how much time we’d save!

Posted by: John Baez on August 28, 2017 11:39 AM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

When I talk about multi-sorted operads, I usually have some fixed set $S$ of sorts (= objects) in mind, so I’m actually thinking about ‘$S$-sorted operads’, and the maps between $S$-sorted operads should preserve the sorts. When I talk about symmetric multicategories, I imagine the set of objects (= sorts) as variable, and the maps between symmetric multicategories don’t need to preserve the objects.

I suppose there’s some sense in making a terminological distinction there, although since “$S$-sorted operad” isn’t in common use, it seems to me you might as well say “$S$-sorted multicategory”.

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.

If someone could figure out how to do mathematics without terminology, just think how much time we’d save!

I know, right?

Posted by: Mike Shulman on August 28, 2017 4:06 PM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

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.

Posted by: John Baez on August 29, 2017 1:34 AM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

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”…)

Posted by: Mike Shulman on August 29, 2017 5:34 AM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

If someone could figure out how to do mathematics without terminology, just think how much time we’d save!

Not to mention notation. Notation just drives me crazy.

Posted by: Mark Meckes on August 28, 2017 4:16 PM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

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

Posted by: John Baez on August 28, 2017 5:03 PM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

For whatever it’s worth, I think Todd’s proof works more generally for “relevance multicategories”, which are to cartesian multicategories (multi-sorted Lawvere theories) the way relevance monoidal categories are to cartesian monoidal categories. Relevance multicategories describe algebraic theories for which every equational axiom involves the same set of variables on both sides, though perhaps a different number of times: we can duplicate inputs but not discard them. Note that Charles’s counterexample uses equations $f(s)=0$ and $f(s)=1$ in which a variable on the left disappears on the right.

Posted by: Mike Shulman on August 28, 2017 7:51 AM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

Ah, John and I were wondering whether it holds in that greater generality. Thanks, Mike!

Posted by: Todd Trimble on August 28, 2017 10:54 AM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

Mike wrote:

For whatever it’s worth, I think Todd’s proof works more generally for “relevance multicategories”, which are to cartesian multicategories (multi-sorted Lawvere theories) the way relevance monoidal categories are to cartesian monoidal categories.

Todd and I had pondered this generalization, but I hadn’t seen the relevance to anything interesting. In our correspondence, Todd wrote:

There is a small question in my mind whether your conjecture holds in the slightly greater generality where there is the “contraction rule” in logic, i.e., where we consider the doctrine where we have natural diagonal maps $x \to x \otimes x$ (plus coassociativity etc.) but not necessarily projections $x \to I$ to the monoidal unit — cosemigroups if you will. All the counterexamples uncovered so far seem to devolve on projections.

I replied:

I was going to mention this too! I’ve often talked about “semicartesian categories”, which allow deletion but not duplication. This could be the first time I’ve seen an interesting result for “hemicartesian categories” — my silly name for the symmetric monoidal categories you’re talking about, which allow duplication but not deletion. (We should use silly names for useless concepts, saving the good names for the useful ones.) But since I don’t know any other interesting results about hemicartesian categories — do you? —- I’m not motivated to pursue this one.

Thus the concepts that people already like, get more attention and become even more likeable, while the losers continue to languish.

I’m happy to hear that relevance monoidal categories are of enough interest to have their own $n$Lab entry. Given this, I’ll stop using a deliberately silly name for them.

(With my silly nomenclature, a semicartesian hemicartesian category is cartesian, in analogy with how $\frac{1}{2} + \frac{1}{2} = 1$, and in disanalogy to the demisemiquaver, which is $\frac{1}{2} \times \frac{1}{2} = \frac{1}{4}$ of a quaver.)

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

And while I’m at it, here are some puzzles. The free cartesian category on one object is the opposite of the category of finite sets and functions, with disjoint union as the product. The free symmetric monoidal category on one object is the groupoid of finite sets and bijections, with disjoint union as the tensor product. So such things tend to be interesting.

Puzzle 1. What is the free semicartesian category on one object?

Puzzle 2. What is the free relevance monoidal category on one object?

I don’t know the answers for sure, but I have guesses, based on the facts I just stated.

Posted by: John Baez on August 28, 2017 11:18 AM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

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

Posted by: Mike Shulman on August 28, 2017 4:37 PM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

Todd’s proof in the operad case (above) is pretty slick. However, it’s worth noting that the claim in the operad case is immediate from the well-known “Taylor series expansion” formula for $M+F(X)$, which writes the underlying (multi-)set of this as a coproduct of “terms” associated to each “power of $X$”; the inclusion $M\to M+F(X)$ is just the inclusion of the “constant” term.

Posted by: Charles Rezk on August 28, 2017 6:01 PM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

That proof sounds nice, Charles! This approach is roughly what I was alluding to when I said:

One approach would be to actually ‘build’ $M + F(X)$ in a very concrete way as an $S$-tuple of sets equipped with a bunch of $n$-ary operations […]

but you just made it sound a lot easier.

I get the idea, but do you happen to know a reference for this “well-known” Taylor series expansion? I know a bunch of stuff about the coproduct of operads and free operad on a signature, and happen to have just written a paper that gives a painfully explicit descriptions of both these constructions using trees… but only in the unsorted case. I could wave my hands and say the sorted case is “just the same”, but in my old age I’ve started wanting to set a good example and give detailed proofs… or even better, refer to other people’s.

Posted by: John Baez on August 29, 2017 3:38 AM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

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.

Posted by: Charles Rezk on August 29, 2017 5:20 PM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

Thanks for the very detailed reply! I’ll say something more interesting later.

Posted by: John Baez on August 30, 2017 3:32 AM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

Well, this isn’t very interesting, but it is at least more interesting.

I think Charles’ proof here is the one in The Book: we can generalize it nicely to algebras of multi-sorted operads, replacing derivatives by partial derivatives, and it then shows that for any $S$-sorted operad $O$, any algebra $M$ of $O$, and any $S$-tuple of sets $X$, the canonical map of algebras

$M \to M + F(X)$

is monic, by giving a beautiful ‘Taylor expansion’ of $M + F(X)$… or more precisely, its underlying $S$-tuple of sets.

However, Todd’s proof is shorter, and requires less apparatus. Since all this stuff is supposed to be proving Corollary 53 in Appendix A.2 of a paper that’s already quite long, I decided to go with Todd’s approach.

Thanks a million to both of you! I learned some nice things about categories and operads, which will probably come in handy. (You are, of course, acknowledged in the paper.)

Posted by: John Baez on September 2, 2017 8:19 AM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

Since nobody has tackled my puzzles yet, I’ll record my guesses and let others prove ‘em or shoot ‘em down:

Puzzle 1. What is the free semicartesian monoidal category on one object?

Puzzle 2. What is the free relevance monoidal category on one object?

Recall that the free symmetric monoidal category on one object is $Bij$, the groupoid of finite sets and bijections. The tensor product here is disjoint union. For reasons soon to become clear, I’d prefer to work with the equivalent category $Bij^{op}$.

Recall also that the free cartesian monoidal category on one object is $FinSet^{op}$. The tensor product is again disjoint union, which is the coproduct in $FinSet$, and thus the cartesian product in $FinSet^{op}$. Every object $S$ comes with a deletion morphism

$!_S : S \to \emptyset$

(the opposite of the unique function $\emptyset \to S$) and a duplication morphism

$\Delta_S : S \to S \sqcup S$

(the opposite of the obvious function $S \sqcup S \to S$).

Loosely speaking, if we keep $!_S$ and forget about $\Delta_S$ we get a semicartesian monoidal category. If we keep $\Delta_S$ and forget about $!_S$ we get a relevance monoidal category.

$!_S$ is the opposite of the injection $\emptyset \to S$, while $\Delta_S$ is the opposite of the surjection $S \sqcup S \to S$.

So, I’m hoping that the answers to Puzzles 1 and 2 are two categories between $Bij^{op}$ and $FinSet^{op}$, namely $Inj^{op}$ and $Surj^{op}$.

If we look at the symmetric monoidal subcategory generated by all the objects of $FinSet^{op}$ but only the morphisms $!_S$, we get $Inj^{op}$, the opposite of the category of finite sets and injections. I believe $Inj^{op}$ is a semicartesian category. And I hope it’s the free semicartesian category on one object!

If we look at the symmetric monoidal subcategory generated by all the objects of $FinSet^{op}$ but only the morphisms $\Delta_S$, we get $Surj^{op}$, the opposite of the category of finite sets and surjections. I believe $Surj^{op}$ is a relevance category. And I hope it’s the free relevance monoidal category on one object!

As Bott once said in his differential geometry seminar: if there’s any justice in the universe, this must be true.

Posted by: John Baez on August 29, 2017 9:34 AM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

Are there left adjoints to the various forgettings: Cartesian to semicartesian and to relevance, and from each of these to symmetric monoidal?

Posted by: David Corfield on August 30, 2017 1:12 PM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

The answer should be ‘yes’ on general doctrinal grounds, analogous to relative left adjoints between categories of algebras (i.e., left adjoints to forgetful functors $Alg_T \to Alg_S$ induced by morphisms of monads $S \to T$). But I’ll plead laziness and say nothing more for the moment, mainly because my 2-categorical algebra is not really up to scratch.

But what is interesting is that some of these forgetful functors have right (bi)adjoints which have very natural descriptions. For example, the right adjoint to the forgetful functor

$Cart \to SymmMon$

takes a symmetric monoidal category $C$ to the category of cocommutative comonoid objects in $C$. Similarly, the right adjoint to $SemiCart \to SymmMon$ takes $C$ to the slice $C/I$ over the monoidal unit, and the right adjoint to $RelMon \to SymmMon$ (relevance monoidal categories to their underlying symmetric monoidal categories) takes $C$ to the category of cocommutative cosemigroups. An offhand guess that some of these adjoints lift, so that e.g. the cofree cartesian monoidal category on a relevance monoidal category $C$ is the slice $C/I$, but as I say this is offhand and I’d need to check that more carefully.

Posted by: Todd Trimble on August 30, 2017 2:29 PM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

Interesting!

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

Posted by: David Corfield on August 30, 2017 2:44 PM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

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!

Posted by: John Baez on August 30, 2017 4:12 PM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

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

Posted by: Mike Shulman on August 30, 2017 5:07 PM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

Hi. Here are a couple of references that mention or use the universal property of Inj, which makes it quite popular and important in computer science:

• Marcelo Fiore and Sam Staton. Comparing operational models of name-passing process calculi. [preprint]

• John Power. Semantics for Local Computational Effects. [doi]

(I’m not claiming that the first is an “earliest reference”, and others may have many other references besides!)

Posted by: Sam on August 30, 2017 4:29 PM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

Example 2.10 of Hyland and Power’s Symmetric monoidal sketches characterises $Inj^{op}$ as a generic model for a sketch $c: X \to I$, and, as a single-sorted sketch, the free category on 1 with that structure.

Posted by: David Corfield on August 31, 2017 8:43 AM | Permalink | Reply to this

Re: A Puzzle on Multi-Sorted Lawvere Theories

Thanks, Sam and David!

David wrote:

Example 2.10 of Hyland and Power’s Symmetric monoidal sketches characterises $Inj^{op}$ as a generic model for a sketch $c: X \to I$, and, as a single-sorted sketch, the free category on 1 with that structure.

Great! I need to read that paper, since ‘symmetric monoidal sketches’ occupy a territory very similar to the ‘presentations of PROPs’ that I’ve been using a lot lately in my work on networks. They’re both ways of specifying symmetric monoidal categories in terms of generators and relations.

This characterization of $Inj^{op}$ is close to what I was struggling to say when I wrote:

$Surj^{op}$ will be the PROP for cocommutative cosemigroups, while $Inj^{op}$ will be the PROP for ‘pointed’ objects.

But I screwed up… I was off by an op!

By a pointed object in a symmetric monoidal category, I meant an object $X$ equipped with a morphism from the unit for the tensor product,

$p: I \to X$

$Inj$ is the PROP for pointed objects, while $Inj^{op}$ the PROP for copointed objects, meaning objects equipped with a morphism to the unit for the tensor product

$c : X \to I$

A pointed object that’s also a semigroup object in a nicely compatible way is a monoid object; a copointed object that’s also a comonoid object in a nicely compatible way is a comonoid object.

(Btw, calling a morphism $p: I \to X$ a ‘point’ is somewhat controversial unless the unit object $I$ is terminal. It makes lots of sense to call a morphism $c : X \to I$ an augmentation, so perhaps a morphism $p: I \to X$ should be called a coaugmentation. In that case, I could say $Inj^{op}$ is the PROP for augmented objects, and $Inj$ the PROP for coaugmented objects.)

Posted by: John Baez on September 2, 2017 7:59 AM | Permalink | Reply to this

Post a New Comment