Is there a reasoned derivation of the coherence conditions for symmetric rig categories?

Question

I know what the coherence conditions are, I can look them up in

• M. Laplaza, Coherence for distributivity, Lecture Notes in Mathematics 281, Springer Verlag, Berlin, 1972, pp. 29-72.

In theory, apparently I can find these also in

• G. Kelly, Coherence theorems for lax algebras and distributive laws, Lecture Notes in Mathematics 420, Springer Verlag, Berlin, 1974, pp. 281-375.

but I tried to find them there, and failed. Note that I really mean rig category here, as I definitely want non-strictness, so bipermutative categories will not do. (The main examples I am trying to understand are the rig category of permutations with $\oplus$ as disjoint union and $\otimes$ as tensor product, and the probably-rig-category of Types).

I am already aware of the work by Beke -- Categorification, term rewriting and the Knuth-Bendix procedure, which explicitly excludes this case, as the underlying term rewrite system is not confluent.

There might be something in the work of JA Cohen, in particular in Coherence without unique normal forms or his thesis Coherence for rewriting 2-theories, but I have having a hard time extracting an explicit algorithm from these. In the same way, there might be something in the works Guirand and Malbos, Lafont or Mimram (see the links at the end of the nLab page on rewriting, but I am unable to extract an explicit algorithm from these).

I am, above all, looking for a reasoned derivation of the coherence conditions, rather than something ad hoc that just happens to work. A general rewriting theory would be the kind of answer I would prefer; but any kind of explicit algorithm would be satisfying as well.

Answer 1

I'm stating here what I think is the correct version of the conjecture in John Baez's answer.

The 1-categorical theory of rigs has morphisms given by polynomials whose coefficients are in $\mathbb{N}$. The fact that the coefficient and exponent are numbers is the source of the problem when trying to make a symmetric rig category into a (weak) model of the theory: it is not clear what $n \times X$ or $X^n$ means when $n$ is a number (and not an $n$ element sets).

To solve that problem, we need to replace these numbers by finite sets. That is, we will look at the 2-categorical Lawvere whose arrow are "finite polynomial functors", that is functors of the form

$$ P(X) = \coprod_{x \in C}{ X^{B_c}}$$

where $C$ is a finite set and for each $C \in C$, $B_c$ is a finite set. $n$-variables polynomial functor are defined in the same way as $$ P(X_1,\dots,X_n) = \coprod_{c \in C} X_1^{B_{1,c}} \times \dots \times X_n^{B_{n,c}}$$

A natural isomorphism between two polynomial functors can be shown to be in 1-1 corresponds with bijection $\phi:C \simeq C'$ and family of bijections $B_{i,c} \simeq B'_{i,\phi(c)}$.

We can show that we have a $(2,1)$-categorical Lawvere theory, whose morphism $O^n \to O^m$ are collection of $m$ finite polynomial functor on $n$-variables, with only isomorphism between them.

This is exactly the category of polynomial as defined at the beginning of the n-Lab pagein the category of finite sets.

This is a natural categorification of the theory of rigs: the theory of rig is litterally obtained by identifying isomorphic map in this $2$-categorical theory.

Conjecture: Symmetric Rig categories are the models (in an appropriate $(2,1)$-categorical sense) of this Theory in Cat.

As far as I'm concerned, a proof of that conjecture would be the best possible answer to the question:

There are a lot of general theories that can tell you how to "weaken" some theory, but it seem to me that none of then applies directly to the theory of commutative rig.

So the only way to justify the kind of ad-hoc definition that one can find in the literature is to start from a more conceptual definition like the one above, and find a set of axioms for it as simple as possible.

Answer 2

I have not seen a reasoned derivation of Laplaza's coherence laws for what we now call a symmetric rig category, namely a category with two symmetric monoidal structures $\otimes, \oplus$ obeying the commutative rig axioms up to coherent natural isomorphisms. But I believe there is a simpler, equivalent definition.

I conjecture that a symmetric rig category is the same thing as a 'weak model' of the Lawvere theory of commutative rigs in the 2-category $\mathbf{Cat}$, by which I mean a product-preserving pseudofunctor

$$\mathsf{Th}(\text{CommRig}) \to \mathbf{Cat}.$$

If anyone proves this please let me know!

For starters, it should be fairly routine, although quite a bit of work, to prove all of Laplaza's coherence laws starting from this more abstract characterization. (I believe there are about 19 independent coherence laws: he lists more, but then proves implications relating them.) The harder part is the converse.

[EDIT: this conjecture has been refuted below.]

Answer 3

I believe you already hint at the answer.

In theory, apparently I can find these also in

• G. Kelly, Coherence theorems for lax algebras and distributive laws, Lecture Notes in Mathematics 420, Springer Verlag, Berlin, 1974, pp. 281-375.

They may be found in Example 6.11 of that paper. Roughly speaking, Kelly shows that there is a pseudo-distributive law between the free symmetric monoidal category 2-monad and itself (although Kelly uses the language of clubs), and then studies the algebras for the composite 2-monad. Algebras for composite 2-monads may be characterised in terms of algebra structures for each component 2-monad, with the same underlying object, together with several compatibility conditions. In this case: two symmetric monoidal category structures on the same category, together with 10 compatibility conditions, which Kelly states are equivalent to the 24 axioms given by Laplaza.