Phil Scott
This article is dedicated to the memory of Phil Scott (1947–2023).
I was introduced to Phil in the summer of 2012 at a workshop in Halifax. At the time, I was an undergraduate student and do not remember understanding anything that took place. Nonetheless, I was made to feel welcome and my interest was warmly encouraged. A few years later, I would in turn be introduced to categorical logic by Lambek and Scott (Reference Lambek and Scott1986). Phil’s book was the first material on category theory that I really took to, and it has been a major influence on my view of the subject.
I would see Phil again from time to time, particularly during my time in Ottawa, where he lived, and in Edinburgh, where he would often visit. He was always kind, often smiling, and invariably good conversation. I think that Phil would have been interested in the work presented here, and I would have very much liked to pick his brain on the subject.
1. Introduction
This paper concerns the categorical representation of the partial recursive functions. More precisely, we are interested in assumptions on distributive monoidal categories which ensure the representability of all partial recursive functions therein. We build directly on the work of Plotkin (Reference Plotkin2013), which supplies one such set of assumptions. Specifically, it suffices to assume that the category in question has a weak (left or right) natural numbers object
$z : I \to N \leftarrow N : s$
in the sense of Paré and Román (Reference Paré and Román1989) with the additional property that the morphism
$[z,s] : I+N \to N$
is invertible, and that this inverse is a weakly final coalgebra of the functor
$I + -$
.
The first contribution of this paper is another set of assumptions, of a rather different flavor, on a distributive monoidal category that ensure it represents the partial recursive functions. Specifically, we consider distributive monoidal categories whose additive monoidal structure is traced, and which additionally contain a distinguished object
$N$
that is required to be isomorphic to
$I+N$
. We show that in any such category the conditions given by Plotkin are satisfied, meaning in particular that the partial recursive functions are representable. We propose to call categories like this in which the trace operator satisfies the uniformity axiom Elgot categories.
The second contribution of this paper is the construction of a category whose morphisms correspond to abacus programs in the sense of Lambek (Reference Lambek1961). This construction is inspired by (and largely adapted from) the work of Bonchi et al. (Reference Bonchi, Di Giorgio and Santamaria2023, Reference Bonchi, Di Giorgio and Di Lavore2024) on tape diagrams. We show that this category of abacus programs is an Elgot category, and that it is moreover an initial object in a suitable category of Elgot categories.
We also obtain that our category of abacus programs strongly represents the partial recursive functions. Loosely speaking, while (mere) representability is about being able to interpret a given partial function in some category, strong representability is about being able to define it in that category (see Section 3). Plotkin’s set of assumptions ensuring representability of the partial recursive functions can be extended to ensure their strong representability Plotkin (Reference Plotkin2013). Specifically, it suffices to ask that the numerals
$\underline {0} = z$
and
$\underline {1} = zs$
are distinct, and that any partial function that is strongly representable in the category in question is necessarily partial recursive. Our category of abacus programs satisfies these extra conditions. Thus, our initial Elgot category strongly represents (so in a sense, generates) the partial recursive functions.
The significance of our results is twofold. First, by exhibiting the category of abacus programs as an initial Elgot category, we demonstrate that abacus programs are a canonical notion, in the sense that they can be seen as an “internal language” for Elgot categories. Second, by showing that the partial recursive functions are precisely those partial functions that are strongly representable in the initial Elgot category of abacus programs, we demonstrate that the notion of Elgot category captures the partial recursive functions. While a number of categorical approaches to recursion theory have been proposed, we suggest that Elgot categories are distinguished by being mathematically natural, at least from the perspective of monoidal category theory. By this, we mean that each component of the definition is a well-behaved and well-studied mathematical structure in its own right, and that no component of the definition feels particularly mysterious, with each playing a clear role.
1.1 Related work
That distributive categories model a kind of finitary branching computation has been known for some time (see e.g., Walters (Reference Walters1989, Reference Walters1992); Cockett (Reference Cockett1993); Carboni et al. (Reference Carboni, Lack and Walters1993); Khalil and Walters (Reference Khalil and Walters1993)). However, the category of partial recursive functions is not distributive because it does not have products (Cockett and Lemay (Reference Cockett and Lemay2023)). Instead, it has restriction products (Cockett and Lack (Reference Cockett and Lack2007)), making it a distributive restriction category in the sense of for example Cockett and Lemay (Reference Cockett and Lemay2023). Every distributive restriction category is distributive monoidal, and the results of this paper can almost certainly be specialized to Elgot categories whose underlying distributive monoidal category is in fact a distributive restriction category. We leave this for future work (see Section 6) and restrict our attention to the more general setting herein.
Traced monoidal categories and their string diagrams, introduced in Joyal et al. (Reference Joyal, Street and Verity1996), have become a standard tool in the categorical modeling of systems with feedback. In particular, a cocartesian monoidal category admits a parameterized iteration operator if and only if it is traced (Hasegawa (Reference Hasegawa1997)). This kind of iteration operator would seem to be fundamental to computer science and has been studied extensively (see e.g., Elgot (Reference Elgot1975); Bloom et al. (Reference Bloom, Ésik, Bloom and Ésik1993); Simpson and Plotkin (Reference Simpson and Plotkin2000); Stefanescu (Reference Stefanescu2000); Adámek et al. (Reference Adámek, Milius and Velebil2010); Goncharov (Reference Goncharov2022)).
While distributive monoidal categories do not seem to have been much studied in and of themselves—with the notable exception of Labella (Reference Labella2003)—they are in particular rig categories,Footnote 1 which are the subject of a good amount of existing work (see e.g., Laplaza (Reference Laplaza2006); Johnson and Yau (Reference Johnson and Yau2024)). Tape diagrams, which are a string-diagrammatic calculus for rig categories (Bonchi et al. (Reference Bonchi, Di Giorgio and Santamaria2023, Reference Bonchi, Di Giorgio and Di Lavore2024)), are particularly relevant to our development. The construction of the initial Elgot category of Abacus programs presented here is largely adapted from that of the rig category of tape diagrams (see Section 5 for a discussion of the differences), and the present work has been inspired in part by the evident visual similarity between abacus programs and tape diagrams.
For a historical discussion of the notion of representability, see Part III of Lambek and Scott (Reference Lambek and Scott1986), which is itself concerned with the representability of (total) recursive functions in various categorical structures. The specific notion of (strong) representability used in this paper is from Plotkin (Reference Plotkin2013), and we use the results of Plotkin (Reference Plotkin2013) repeatedly in our development. Natural numbers objects first appear in Lawvere (Reference Lawvere1964), although the more general notion of natural numbers object in a monoidal category appears significantly later in Paré and Román (Reference Paré and Román1989). A recent survey of these ideas and results concerning them can be found in Section 4 of Hofstra and Scott (Reference Hofstra and Scott2021).
Finally, there is a line of work in the field of reversible computation which is similar in spirit to our work. Namely, various sorts of (initial) traced rig category have been proposed as reversible programming languages (Bowman et al. (Reference Bowman, James and Sabry2011); James and Sabry (Reference James and Sabry2012); Kaarsgaard and Veltri (Reference Kaarsgaard and Veltri2019); Chen and Sabry (Reference Chen and Sabry2021); Kaarsgaard and Rennela (Reference Kaarsgaard and Rennela2021)).
1.2 Synopsis
Section 2 recalls the notions of structured monoidal category that will be necessary for our development. Section 3 contains the necessary material on natural numbers algebras and (strong) representability of partial recursive functions. Section 4 contains the definition of Elgot category and establishes that every such category represents the partial recursive functions (Theorem4.3). Section 5 introduces Lambek’s abacus programs, constructs a category of abacus programs (Definition5.1), establishes that it is an initial Elgot category (Theorems5.2 and 5.3), and that it strongly represents all (and only) the partial recursive functions (Theorem5.4 and Corollary 5.5). The axioms for rig categories in both the usual and right-strict case are enumerated in Appendix A, and Appendix B contains the proof of Theorem5.2, which is long, tedious, and straightforward.
2. Traced and Distributive Monoidal Categories
In this section, we set up the rest of our development by recalling the required notions of structured monoidal category: cocartesian monoidal categories (Definition2.1), (uniform) traced monoidal categories (Definitions2.2 and 2.3), and distributive monoidal categories (Definition2.4).
We assume the reader to have some familiarity with category theory and in particular with monoidal categories and their string diagrams. Some elementary knowledge of the partial recursive functions would also be helpful, but is not, strictly speaking, required to read this paper. We consider only strict monoidal category structure. In particular, this means that the additive and multiplicative monoidal structures of our distributive monoidal categories are both strict. Herein, “monoidal category” means “strict monoidal category.” That said, one imagines that suitable analogues of the results presented here hold in the more general setting. We will write composition in diagrammatic order, meaning that given
$f : A \to B$
and
$g : B \to C$
we write
$fg : A \to C$
and not
$gf : A \to C$
. String diagrams are to be read top-to-bottom.
We begin with the notion of cocartesian monoidal category:
Definition 2.1.
A
$\text{cocartesian monoidal category}$
is a tuple
$((\mathbb{C},+,0,\sigma ^+),(\mu ,\eta ))$
such that:
-
•
$(\mathbb{C},+,0,\sigma ^+)$
is a symmetric monoidal category.
-
•
$\mu$
and
$\eta$
are monoidal natural transformations with components as in
$\mu _A : A + A \to A$
and
$\eta _A : 0 \to A$
. -
• For all objects
$A$
of
$\mathbb{C}$
,
$(A,\mu _A,\eta _A)$
is a commutative monoid in
$\mathbb{C}$
.
More explicitly, a symmetric monoidal category is cocartesian in case we have morphisms
$\mu _A : A + A \to A$
and
$\eta _A : 0 \to A$
for each object
$A$
of
$\mathbb{C}$
such that for all
$f : A \to B$
we have:
\begin{align*} \mu _Af = (f+f)\mu _B \quad \eta _Af = \eta _B \end{align*}
which give that
$\mu$
and
$\eta$
are natural transformations of the appropriate type, along with:
\begin{align*} \mu _I = 1_I \quad \mu _{A+B} = (1_A + \sigma ^+_{B,A} + 1_B)(\mu _A + \mu _B) \quad \eta _I = 1_I \quad \eta _{A + B} = \eta _A + \eta _B \end{align*}
which give that
$\mu$
and
$\eta$
are monoidal natural transformations, and finally for each
$(A,\mu _A,\eta _A)$
to be a commutative monoid means that we have:
\begin{align*} (\mu _A + 1_A)\mu _A = (1_A + \mu _A)\mu _A \quad \sigma ^+_{A,A}\mu _A = \mu _A \quad (1_A + \eta _A)\mu _A = 1_A \end{align*}
Morphisms of cocartesian monoidal categories may be represented string-diagrammatically by extending the diagrams for symmetric monoidal categories with the following components corresponding the
$\mu$
and
$\eta$
:
In a cocartesian monoidal category,
$A+B$
is always a coproduct of
$A$
and
$B$
, with the copairing
$[f,g] : A+B \to C$
of
$f : A \to C$
and
$g : B \to C$
given by
$(f+g)\mu _C$
. The coprojections are given by
$1_A + \eta _B : A \to A + B$
and
$\eta _A + 1_B : B \to A + B$
. Moreover, the unit object is necessarily initial, and so every cocartesian monoidal category has finite coproducts. In fact, asking that the tensor product and unit object of a symmetric monoidal category carry finite coproduct structure in this way is equivalent to asking that it be cocartesian monoidal Fox (Reference Fox1976).
The next notion we require is that of a traced monoidal category:
Definition 2.2.
A
$\text{traced monoidal category}$
is a tuple
$((\mathbb{C},\oplus ,0,\sigma ^\oplus ),\mathsf{Tr})$
such that:
-
•
$(\mathbb{C},\oplus ,0,\sigma ^\oplus )$
is a symmetric monoidal category.
-
•
$\mathsf{Tr}$
is a family of operations
$\mathsf{Tr}^C_{A,B} : \mathbb{C}(A \oplus C, B \oplus C) \to \mathbb{C}(A,B)$
satisfying the following axioms:
-
[TR1]
$\mathsf{Tr}^I_{A,B}(f) = f$
-
[TR2]
$\mathsf{Tr}^{C \oplus D}_{A,B} = \mathsf{Tr}^C_{A,B}(\mathsf{Tr}^D_{A \oplus C,B \oplus C}(f))$
-
[TR3]
$g\mathsf{Tr}^C_{A,B}(f)h = \mathsf{Tr}^C_{A',B'}((g \oplus 1_C)f(h \oplus 1_C))$
-
[TR4]
$1_D \oplus \mathsf{Tr}^C_{A,B}(f) = \mathsf{Tr}^C_{D \oplus A,D \oplus B}(1_D \oplus f)$
-
[TR5]
$\mathsf{Tr}^C_{A,B}((1_A \oplus h)f) = \mathsf{Tr}^D_{A,B}(f(1_B \oplus h))$
-
[TR6]
$\mathsf{Tr}^A_{A,A}(\sigma ^\oplus _{A,A}) = 1_A$
-
Morphisms of traced monoidal categories admit a helpful string-diagrammatic representation as in:
Some trace operators are additionally uniform Footnote 2 in the following sense:
Definition 2.3.
A traced monoidal category
$((\mathbb{C},\oplus ,0,\sigma ^\oplus ),\mathsf{Tr})$
is called
$\text{uniform}$
in case for all
$f : A \oplus C \to B \oplus C$
and
$g : A \oplus D \to B \oplus D$
, if there exists
$h : C \to D$
such that
$(1_A \oplus h)f = g(1_B \oplus h)$
then we have
$\mathsf{Tr}^C_{A,B}(f) = \mathsf{Tr}^D_{A,B}(g)$
.
Hasegawa has shown (Hasegawa (Reference Hasegawa1997)) that a cocartesian monoidal category is traced if and only if it admits a parameterized iteration operator in the sense of for example Simpson and Plotkin (Reference Simpson and Plotkin2000). Specifically, defining
$(\!-\!)^\dagger : \mathbb{C}(A,X+A) \to \mathbb{C}(A,X)$
by
$f^\dagger = \mathsf{Tr}^A_{A,X}(\mu _Af)$
makes
$(\!-\!)^\dagger$
into a parameterized iteration operator, where the fixed point property
$f^\dagger = f[1_X,f^\dagger ]$
holds as in:
While the uniformity axiom seems to resist intuitive explanation, it plays an important role in the algebraic theory of iteration.Footnote
3
For example, in any uniformly traced cocartesian monoidal category, the uniformity axiom interacts with the cocartesian structure in an interesting way. Naturality of
$\mu$
yields:
While naturality of
$\eta$
yields:
Uniformity is therefore a desirable property if we want to interpret the morphisms of the cocartesian traced monoidal category in question as, say, flowchart computations.
A distributive monoidal category is a category with two tensor product structures, one typically called multiplicative and the other additive, such that the multiplicative structure distributes over the additive one in the following sense:
Definition 2.4.
A
$\text{distributive monoidal category}$
is a tuple
$(\mathbb{C},(+,0,\sigma ^+),(\otimes ,I),(\mu ,\eta ),(\lambda ^\bullet , \rho ^\bullet ),$
$(\delta ^l,\delta ^r))$
such that:
-
•
$((\mathbb{C},+,0,\sigma ^+),(\mu ,\eta ))$
is a cocartesian monoidal category, which we refer to as the
$\text{additive}$
monoidal structure on
$\mathbb{C}$
. -
•
$(\mathbb{C},\otimes ,I)$
is a monoidal category, which we refer to as the
$\text{multiplicative}$
monoidal structure on
$\mathbb{C}$
. -
•
$\lambda ^\bullet$
and
$\rho ^\bullet$
are natural isomorphisms with components
$\lambda ^\bullet _A : 0 \otimes A \to 0$
and
$\rho ^\bullet _A : A \otimes 0 \to 0$
called the left and right
$\text{annihilator}$
, respectively.
-
•
$\delta ^l$
and
$\delta ^r$
are natural isomorphisms with components
called the left and right
\begin{align*} \delta ^l_{A,B,C} : A \otimes (B + C) \to (A \otimes B) + (A \otimes C) \quad \delta ^r_{A,B,C} : (A + B) \otimes C \to (A \otimes C) + (B \otimes C) \end{align*}
$\text{distributor}$
, respectively.
-
• The coherence axioms [B1] – [B22] (see Appendix A ) are satisfied.
We adopt a common notational convenience: when referring to the objects of a distributive monoidal category one often denotes the multiplicative tensor product
$\otimes$
by juxtaposition. For example,
$A \otimes B$
becomes
$AB$
,
$A \otimes B \otimes C$
becomes
$ABC$
, and
$A \otimes (B + (C \otimes D))$
becomes
$A(B + CD)$
.
The notion of distributive monoidal category may be partially strictified. In particular, we say that a distributive monoidal category is right-strict in case
$\lambda ^\bullet$
,
$\rho ^\bullet$
, and
$\delta ^r$
are identity natural transformations. The effect of these assumptions on the axioms of distributive monoidal category is treated explicitly in Appendix A. There is of course a dual notion of left-strict distributive monoidal category, although here we will work exclusively with the right-strict version.
While in this paper we privilege the point of view occupied by Definition2.4, which emphasizes the rig category structure of distributive monoidal categories, it is worth mentioning that distributive monoidal categories admit a much simpler axiomatisation: For any category
$\mathbb{C}$
with monoidal structure
$(\mathbb{C},\otimes ,I)$
and cocartesian monoidal structure
$((\mathbb{C},+,0,\sigma ^+),(\mu ,\eta ))$
, we may construct morphisms:
It so happens that asking for an inverse to every such map gets us most of the way to having a distributive monoidal category. Specifically, we have:
Lemma 2.5 (after Labella (Reference Labella2003))
Let
$((\mathbb{C},+,0,\sigma ^+),(\mu ,\eta ))$
be a cocartesian monoidal category, and let
$(\mathbb{C},\otimes ,I)$
be a monoidal category. Suppose that
$\lambda ^\bullet$
,
$\rho ^\bullet$
,
$\delta ^l$
, and
$\delta ^r$
are indexed families of morphisms as in Definition
2.4
. Then
$(\mathbb{C},(+,0,\sigma ^+),(\otimes ,I),(\mu ,\eta ),(\lambda ^\bullet ,\rho ^\bullet ),(\delta ^l,\delta ^r))$
is a distributive monoidal category if and only if:
-
• Each
$\lambda ^\bullet _A : 0 \otimes A \to 0$
is the inverse of the morphism
$\eta _{0 \otimes A} : 0 \to 0 \otimes A$
and, dually, each
$\rho ^\bullet _A : A \otimes 0 \to 0$
is the inverse of the morphism
$\eta _{A \otimes 0} : 0 \to A \otimes 0$
. -
• Each
$\delta ^l_{A,B,C}$
is the inverse of
$\mu ^l_{A,B,C}$
and, dually, each
$\delta ^r_{A,B,C}$
is the inverse of
$\mu ^r_{A,B,C}$
.
3. Categorical Representability of Partial Recursive Functions
In this section, we review the elementary definitions concerning (strong) representability and recall the results of Plotkin (Reference Plotkin2013) concerning the (strong) representability of the partial recursive functions (Theorems3.9 and 3.10). This section is almost entirely adapted from the work of Plotkin (Reference Plotkin2013), although it seems appropriate to mention the work of Lambek and Scott (Reference Lambek and Scott1986) in connection with the categorical representability of numerical functions and the work of Paré and Román (Reference Paré and Román1989) in connection natural numbers objects in monoidal categories.
We begin with the notion of natural numbers algebra, the point of which is to allow us to represent the natural numbers in a given monoidal category:
Definition 3.1.
A
$\text{natural numbers algebra}$
in a monoidal category
$(\mathbb{C},\otimes ,I)$
is a tuple
$(N,z,s)$
such that
$N$
is an object of
$\mathbb{C}$
and
$z : I \to N$
,
$s : N \to N$
are morphisms of
$\mathbb{C}$
. Any such natural numbers algebra defines a
$\text{numeral}$
$\underline {n} : I \to N$
for each
$n \in \mathbb{N}$
, as in:
\begin{align*} \underline {0} = z \quad \underline {n+1} = \underline {n}s \end{align*}
We will say that a natural numbers algebra is
$\text{strong}$
in case
$\underline {n} = \underline {m} \Rightarrow n = m$
for all
$n,m \in \mathbb{N}$
.
The notion of representability for numerical partial functions we consider is as follows:
Definition 3.2.
Suppose
$(\mathbb{C},\otimes ,I)$
is a monoidal category, and that
$(N,z,s)$
is a natural numbers algebra therein. Given a partial function
$f : \mathbb{N}^n \to \mathbb{N}$
and a morphism
$\underline {f} : N^n \to N$
of
$\mathbb{C}$
, we say that
$\underline {f}$
$\text{represents}$
$f$
$\text{with respect to}$
$(N,z,s)$
in case for all
$k_1,\ldots ,k_n \in \mathbb{N}$
we have:
\begin{align*} f(k_1,\ldots ,k_n) = k \hspace {0.3cm} \Rightarrow \hspace {0.3cm} (\underline {k_1} \otimes \cdots \otimes \underline {k_n})\underline {f} = \underline {k} \end{align*}
Note that since
$f$
is a partial function there may not be any such
$k \in \mathbb{N}$
, in which case
$f(k_1,\ldots ,k_n)$
is undefined and we require nothing of the morphism
$(\underline {k_1} \otimes \cdots \otimes \underline {k_n})\underline {f}$
.
Strong representability is now a natural strengthening of (mere) representability:
Definition 3.3.
Suppose
$(\mathbb{C},\otimes ,I)$
is a monoidal category, and that
$(N,z,s)$
is a natural numbers algebra therein. Given a partial function
$f : \mathbb{N}^n \to \mathbb{N}$
and a morphism
$\underline {f} : N^n \to N$
of
$\mathbb{C}$
, we say that
$\underline {f}$
$\text{strongly represents}$
$f$
$\text{with respect to}$
$(N,z,s)$
in case for all
$k_1,\ldots ,k_n \in \mathbb{N}$
we have:
\begin{align*} f(k_1,\ldots ,k_n) = k \hspace {0.3cm} \Leftrightarrow \hspace {0.3cm} (\underline {k_1} \otimes \cdots \otimes \underline {k_n})\underline {f} = \underline {k} \end{align*}
Note that in contrast to mere representability, strong representability requires that
$f(k_1,\ldots ,k_n)$
is undefined if and only if the morphism
$(\underline {k_1} \otimes \cdots \otimes \underline {k_n})\underline {f}$
is not a numeral. That is,
$(\underline {k_1} \otimes \cdots \otimes \underline {k_n})\underline {f}$
is not equal to
$\underline {k}$
for any
$k \in \mathbb{N}$
.
One way to understand strong representability is as a more general notion of Kleene equality. For partial functions
$f,g : \mathbb{N}^n \to \mathbb{N}$
recall that
$f$
$\text{is Kleene equal to}$
$g$
, written
$f \simeq g$
, in case for all
$k_1,\ldots ,k_n \in \mathbb{N}$
we have:
\begin{align*} f(k_1,\ldots ,k_n) = k \hspace {0.3cm} \Leftrightarrow \hspace {0.3cm} g(k_1,\dots ,k_n) = k \end{align*}
Intuitively,
$f \simeq g$
says that
$f$
is defined precisely when
$g$
is defined, in which case they agree.
There is a monoidal category structure
$(\mathsf{Par},\times ,1)$
on the category
$\mathsf{Par}$
of sets and partial functions where
$\times$
is the cartesian product of sets and
$1 = \{*\}$
is any singleton set. Let
$\mathsf{succ} : \mathbb{N} \to \mathbb{N}$
and
$\mathsf{zero} : 1 \to \mathbb{N}$
be the successor function and constant zero function, respectively. Then
$(\mathbb{N},\mathsf{zero},\mathsf{succ})$
is a natural numbers algebra in
$\mathsf{Par}$
. Now, given partial functions
$f,g : \mathbb{N}^n \to \mathbb{N}$
, we have that
$f$
strongly represents
$g$
with respect to
$(\mathbb{N},\mathsf{zero},\mathsf{succ})$
if and only if
$f \simeq g$
. Moreover,
$f$
(merely) represents
$g$
with respect to
$(\mathbb{N},\mathsf{zero},\mathsf{succ}$
) if and only if
$g$
extends
$f$
.
Another way to understand strong representability is in terms of definition of partial functions. If
$(N,z,s)$
is a strong natural numbers algebra in a monoidal category
$(X,\otimes ,I)$
, then any morphism
$f : N^n \to N$
defines a partial function
$\overline {f} : \mathbb{N}^n \to \mathbb{N}$
as in:
\begin{align*} \overline {f}(k_1,\ldots ,k_n) = \left\{\begin{array}{l@{\quad}l} k & \text{ if } (\underline {k_1} \otimes \cdots \otimes \underline {k_n})f = \underline {k} \\ \uparrow & \text{ otherwise} \end{array} \right. \end{align*}
Then
$f$
strongly represents
$\overline {f}$
with respect to
$(N,z,s)$
. Note that while any morphism strongly represents at most one partial function, a given partial function may be strongly represented by multiple morphisms.
Before moving on, let us record a convenient fact about strong natural numbers algebras:
Lemma 3.4.
Let
$(X,\otimes ,I)$
be a monoidal category, and let
$(N,z,s)$
be a natural numbers algebra therein. If
$\underline {0} \neq \underline {1}$
and the (total) predecessor function
$\mathsf{pred} : \mathbb{N} \to \mathbb{N}$
defined as in:
\begin{align*} \mathsf{pred}(n) = \left\{\begin{array}{l@{\quad}l} 0& \text{ if } n = 0\\ n'& \text{ if } n = n' + 1 \end{array}\right. \end{align*}
is representable with respect to
$(N,z,s)$
, then
$(N,z,s)$
is a strong natural numbers algebra.
Proof.
Let
$p : N \to N$
represent
$\mathsf{pred} : \mathbb{N} \to \mathbb{N}$
. Suppose
$\underline {n} = \underline {m}$
. If
$n \neq m$
, then we have (without loss of generality) that
$n \lt m$
, and so
$\mathsf{pred}^{m-1}(n) = 0$
and
$\mathsf{pred}^{m-1}(m) = 1$
. Now since
$p$
represents
$\mathsf{pred}$
, we have
$\underline {n}\,p^{m-1} = \underline {0}$
and
$\underline {m}\,p^{m-1} = \underline {1}$
. But then we have
$\underline {0} = \underline {n}\,p^{m-1} = \underline {m}\,p^{m-1} = \underline {1}$
, a contradiction. It follows that
$n = m$
, as required.
For the numerals of a natural numbers algebra to behave more-or-less like the natural numbers, it must be a natural numbers object. Here, we are interested in the “weak” version of this notion:
Definition 3.5.
A
$\text{weak left}$
Footnote
4
$\text{natural numbers object}$
in a monoidal category
$(\mathbb{C},\otimes ,I)$
is a natural numbers algebra
$(N,z,s)$
in
$(\mathbb{C},\otimes ,I)$
with the property that for any diagram
$B \stackrel {b}{\to } A \stackrel {a}{\leftarrow } A$
in
$\mathbb{C}$
there exists a morphism
$h : N \otimes B \to A$
of
$\mathbb{C}$
such that
Note in particular that
$h$
need not be the unique such morphism.
Weak natural numbers objects relate to representability of numerical partial functions as follows:
Proposition 3.6 Plotkin (Reference Plotkin2013)
Let
$(\mathbb{C},\otimes ,I)$
be a monoidal category, and let
$(N,z,s)$
be a weak left natural numbers object in
$\mathbb{C}$
. Then all primitive recursive functions are representable in
$\mathbb{C}$
relative to
$(N,z,s)$
.
We will be particularly interested in the case where the ambient monoidal category
$(\mathbb{C},\otimes ,I)$
is the multiplicative fragment of a distributive monoidal category. Then a natural numbers algebra is equivalently a morphism
$\iota : I + N \to N$
. From any such morphism, we recover a natural numbers algebra 
and conversely from any natural numbers algebra
$(N,z,s)$
we obtain
$\iota = [z,s] : I+N \to N$
. Moreover, these two constructions are inverses. Thus, a natural numbers algebra in given distributive monoidal category is equivalently a tuple
$(N,\iota )$
where
$\iota : I + N \to N$
.
We give an equivalent formulation of Definition3.5 in this new setting:
Lemma 3.7.
In a distributive monoidal category, a natural numbers algebra
$(N,\iota )$
defines a weak left natural numbers object
$(N,z,s)$
with
$[z,s] = \iota$
if and only if for any diagram
$B \stackrel {b}{\to } A \stackrel {a}{\leftarrow } A$
there exists a morphism
$h : NB \to A$
such that:
Proof.
Suppose that
$(N,z,s)$
is a weak left natural numbers object. Then we have:
\begin{align*} & \delta ^r_{I,N,B}[b,ha] = \delta ^r_{I,N,B}[(z \otimes 1_B)h,(s \otimes 1_B)h] = \delta ^r_{I,N,B}((z \otimes 1_B) + (s \otimes 1_B))\mu _{NB}h \\&\quad = ((z + s) \otimes 1_B)\delta ^r_{N,N,B}\mu _{NB}h = ((z+s) \otimes 1_B)(\mu _N \otimes 1_B)h = ([z,s] \otimes 1_B)h = (\iota \otimes 1_B)h \end{align*}
Conversely, suppose that we have
$\delta ^r_{I,N,B}[b,ha] = (\iota \otimes 1_B)h$
. Then we have:
and
The claim follows.
From this new perspective, natural numbers algebras are algebras of the
$I+-$
functor. We will also be interested in coalgebras of this functor, which we name appropriately:
Definition 3.8.
A
$\text{natural numbers coalgebra}$
in a distributive monoidal category is a tuple
$(N,\gamma )$
where
$\gamma : N \to I+N$
. A natural numbers coalgebra
$(N,\gamma )$
in a distributive monoidal category is said to be
$\text{weakly final}$
in case for all
$\beta : A \to I + A$
there exists a morphism
$h : A \to N$
such that
Note that
$h$
need not be the unique such morphism.
Of particular interest is the case in which we have an isomorphism
$I+N \cong N$
. That is, a natural numbers algebra
$\iota : I+N \to N$
and a natural numbers coalgebra
$\iota ^{-1} : N \to I+N$
which are mutually inverse. In this case, the numerals defined by
$\iota$
are augmented by a sort of predecessor operation, given by
$\iota ^{-1}$
. Moreover, straightforward conditions on
$\iota$
and
$\iota ^{-1}$
yield representability of all partial recursive functions:
Theorem 3.9 (after Plotkin (Reference Plotkin2013))
In a distributive monoidal category
$\mathbb{C}$
, suppose that:
-
•
$\iota : I+N \to N$
is an isomorphism with inverse
$\iota ^{-1} : N \to I+N$
. -
•
$(N,\iota )$
is a weak left natural numbers object.
-
•
$(N,\iota ^{-1})$
is a weakly final natural numbers coalgebra.
Then all partial recursive functions are representable in
$\mathbb{C}$
relative to
$(N,z,s)$
where
$[z,s] = \iota$
.
There is a version of Theorem3.9 for strong representability:
Theorem 3.10 (after Plotkin (Reference Plotkin2013))
In a distributive monoidal category
$\mathbb{C}$
, suppose that:
-
•
$\iota : I+N \to N$
is an isomorphism with inverse
$\iota ^{-1} : N \to I+N$
. -
•
$(N,\iota )$
is a weak left natural numbers object.
-
•
$(N,\iota ^{-1})$
is a weakly final natural numbers coalgebra.
-
•
$z \neq zs : I \to N$
where
$[z,s] = \iota$
. -
• Every partial function that is strongly representable in
$\mathbb{C}$
is partial recursive.
Then all partial recursive functions are strongly representable in
$\mathbb{C}$
relative to
$(N,z,s)$
where
$[z,s] = \iota$
.
It is worth noting that Theorems3.9 and 3.10 are in fact weaker, more specific versions of the results obtained by Plotkin in Plotkin (Reference Plotkin2013), which assume slightly less structure. We have chosen to present the weaker statements here in order to more easily integrate these results into our development.
In the situation described by Theorem3.10, the natural numbers algebra
$(N,\iota )$
is always strong:
Lemma 3.11.
Let
$(N,\iota )$
be a natural numbers algebra in a distributive monoidal category and suppose that
$\iota$
is invertible. If
$\underline {0} \neq \underline {1}$
, then
$(N,\iota )$
is a strong natural numbers algebra.
Proof.
Lemma 3.4 tells us that it suffices to show that
$\mathsf{pred} : \mathbb{N} \to \mathbb{N}$
is representable. Define
$p = \iota ^{-1}[z,1_N] : N \to N$
and let
$[z,s] = \iota$
. Then we have 
and 
. It follows that
$p$
represents
$\mathsf{pred}$
, and so
$(N,\iota )$
is strong.
4. Elgot Categories
In this section, we introduce (pre-)Elgot categories and show that in any (pre-)Elgot category the partial recursive functions are representable (Theorem4.3). We do this by showing that any pre-Elgot category satisfies the conditions of Theorem3.9. Of particular interest is the way in which the traced cocartesian monoidal structure gives rise to the necessary weakly initial and weakly final algebra structure (Lemma 4.2).
We begin with the definition of (pre-)Elgot category:
Definition 4.1.
A
$\text{pre-Elgot category}$
is a tuple
$(\mathbb{C},(+,0,\sigma ^+),(\otimes ,I),(\mu ,\eta ),\mathsf{Tr},(\lambda ^\bullet ,\rho ^\bullet ),(\delta ^l,\delta ^r), (N,\iota ))$
such that:
-
(i)
$(\mathbb{C},(+,0,\sigma ^+),(\otimes ,I),(\mu ,\eta ),(\lambda ^\bullet ,\rho ^\bullet ),(\delta ^l,\delta ^r))$
is a distributive monoidal category.
-
(ii)
$((\mathbb{C},+,0,\sigma ^+),\mathsf{Tr})$
is a traced monoidal category.
-
(iii)
$N$
is an object of
$\mathbb{C}$
with
$\iota : I+N \to N$
an isomorphism.
An
$\text{Elgot category}$
is a pre-elgot category in which the trace is uniform. Moreover, a given (pre-)Elgot category is
$\text{right-strict}$
in case the underlying distributive monoidal category structure is right-strict.
While the results of this section hold for any pre-Elgot category, the construction of an initial Elgot category of abacus programs given in Section 5 requires a uniform trace operator. That is, while the axioms of a pre-Elgot category are enough to ensure the representability of the partial recursive functions, they are not enough to characterize the abacus programs. Specifically, when we construct our category of abacus programs, we must ask for uniformity in order to obtain a distributive monoidal category. In particular, we require the uniformity axiom in order to show that the multiplicative tensor product on the category of abacus programs is functorial (Lemma B.8).
Our naming scheme is motivated by the convention that an “Elgot iteration operator” is implied to satisfy the uniformity axiom. Examples of Elgot categories (ignoring differences in strictness for the moment) include the category of sets and partial functions, and the category of sets and partial recursive functions.
In any pre-Elgot category, the conditions of Theorem3.9 are satisfied:
Lemma 4.2.
For any pre-Elgot category
$(\mathbb{C},(+,0,\sigma ^+),(\otimes ,I),(\mu ,\eta ),\mathsf{Tr},(\lambda ^\bullet ,\rho ^\bullet ),(\delta ^l,\delta ^r),(N,\iota ))$
, we have:
-
(i)
$(N,\iota )$
is a weak left natural numbers object in
$\mathbb{C}$
. -
(ii)
$(N,\iota ^{-1})$
is a weakly final natural numbers coalgebra in
$\mathbb{C}$
.
Proof.
-
(i) We will use the alternate presentation given in Lemma 3.7. Suppose we have
$B \stackrel {b}{\to } A \stackrel {a}{\leftarrow } A$
. Let
$h : NB \to A$
be given as in:Then we have:
\begin{equation*} h = \mathsf{Tr}^{NA}_{NB,A}([1_N \otimes b,1_N \otimes a](\iota ^{-1} \otimes 1_A)\delta ^r_{I,N,A}) \end{equation*}
where the marked equation (
\begin{align*} & (\iota \otimes 1_B)h = (\iota \otimes 1_B)\mathsf{Tr}^{NA}_{NB,A}([1_N \otimes b,1_N \otimes a](\iota ^{-1} \otimes 1_A)\delta ^r_{I,N,A}) \\&\quad \stackrel {*}{=} \delta ^r_{I,N,B}[b,\mathsf{Tr}^{NA}_{NB,A}([1_N \otimes b,1_N \otimes a](\iota ^{-1} \otimes 1_A)\delta ^r_{I,N,A})a] = \delta ^r_{I,N,B}[b,ha] \end{align*}
$\stackrel {*}{=}$
) holds as in:The claim follows.
-
(ii) We must show that for any
$\beta : A \to I+A$
there exists
$h : A \to N$
such that:To that end, suppose
$\beta : A \to I + A$
. Let
$\iota = [z,s]$
, and define
$h : A \to N$
as in:Then we have:
\begin{equation*} h = \mathsf{Tr}^{AN}_{A,N}([1_A \otimes z, 1_A \otimes s](\beta \otimes 1_N)\delta ^r_{I,A,N}) \end{equation*}
where the marked equation (
\begin{align*} & h = \mathsf{Tr}^{AN}_{A,N}([1_A \otimes z, 1_A \otimes s](\beta \otimes 1_N)\delta ^r_{I,A,N}) \\&\quad \stackrel {*}{=} \beta (1_I + \mathsf{Tr}^{AN}_{A,N}([1_A \otimes z, 1_A \otimes s](\beta \otimes 1_N)\delta ^r_{I,A,N}))\iota = \beta (1_I + h)\iota \end{align*}
$\stackrel {*}{=}$
) holds as in:The claim follows.
Now as a corollary, we obtain our representability result:
Theorem 4.3. Every partial recursive function is representable in any pre-Elgot category.
5. Abacus Programs
In this section, we introduce Lambek’s abacus programs Lambek (Reference Lambek1961), construct a category of abacus programs (Definition5.1), show that it is an Elgot category (Theorem5.2), that it strongly represents the partial recursive functions (Theorem5.4), and that it is an initial object in a category of right-strict Elgot categories and structure-preserving functors (Theorem5.3).
What we call abacus programs are a Turing-complete model of computation introduced by Lambek (Reference Lambek1961), in which one assumes a countably infinite set of locations, each of which contains a natural number of counters. Programs are specified as flowcharts with two sorts of instruction for each location
$X$
:
The instruction above left adds a single counter to location
$X$
, following the only arrow out of the instruction box to reach the next instruction. The effect of the instruction above right depends on the number of counters
$X$
contains. If it is zero, then it remains zero and we follow the left arrow to the next instruction box. If it is nonzero, then we remove a counter from
$X$
and follow the right arrow instead.Footnote
5
For example, the following abacus program moves all of the counters from location
$X$
to location
$Y$
:
Arrows with no source are entry points to the program, and arrows with no target are exit points. The textbook of Boolos, Burgess, and Jeffery treats abacus programs at some length (Boolos et al. Reference Boolos, Burgess and Jeffrey2002, Chapter 5) and is highly recommended to the reader interested in a more detailed exposition. We next turn to the construction of a category of abacus programs. Before we can proceed, we require some notation and terminology relating to the free monoid
$X^*$
on a set
$X$
and also to the the free monoid
$(X^*)^*$
on
$X^*$
. Elements of
$X^*$
, which we will refer to as monomials over
$X$
, are sequences of elements of
$X$
, and the monoid operation is concatenation of sequences. We write elements of
$X^*$
by juxtaposing the necessary elements of
$X$
, as in
$abc \in X^*$
for
$a,b,c \in X$
. We write
$I$
for the empty such sequence. Note in particular that since
$I$
is the unit of the monoid structure on
$X^*$
that we have
$IU = U = UI$
for any
$U \in X^*$
. The letters
$U,V,W,\ldots$
will tend to denote monomials.
Elements of
$(X^*)^*$
, which we will refer to as polynomials over
$X$
, are of course sequences of monomials with the monoid operation given by concatenation. We write elements of
$(X^*)^*$
as sequences delimited by the symbol ‘
$+$
’, as in
$U + V + W \in (X^*)^*$
for
$U,V,W \in X^*$
. We write
$0$
for the empty such sequence. Note in particular that since
$0$
is the unit of the monoid structure on
$(X^*)^*$
, we have
$0 + P = P = P + 0$
for any
$P \in (X^*)^*$
. The letters
$P,Q,R,\ldots$
will tend to denote polynomials.
For example, the following are all monomials over
$\{A,B\}$
:
\begin{align*} I \quad A \quad AB \quad BBB \quad BAABBBA \end{align*}
and the following are all polynomials over
$\{A,B\}$
that are not monomials:
\begin{align*} 0 \quad BA + A \quad AAB + BBBBB \quad A + A + 0 \end{align*}
We proceed to construct a category of abacus programs:
Definition 5.1.
Let
$\mathbb{A}$
be the category defined as follows: objects of
$\mathbb{A}$
are polynomials over a single generator
$N$
so that
$\mathbb{A}_0 = (\{N\}^*)^*$
. Arrows of
$\mathbb{A}$
are generated according to the following inference rules:
\begin{align*} & \frac {U,V \text{ monomial}}{\mathsf{succ}_{U,V} : UNV \to UNV} \quad \frac {U,V, \text{ monomial}}{\mathsf{zero}_{U,V} : UV \to UNV} \quad \frac {U,V \text{ monomial}}{\mathsf{pred}_{U,V} : UNV \to UV + UNV}\\& \qquad \qquad \frac {U \text{ monomial}}{1_U : U \to U} \quad \frac {U \text{ monomial}}{\eta _U : 0 \to U} \quad \frac {U \text{ monomial}}{\mu _U : U + U \to U} \quad \frac {\text{}}{1_0 : 0 \to 0}\\ & \quad \frac {U,W \text{ monomial}}{\sigma ^+_{U,W} : U + W \to W + U} \quad \frac {f : P \to Q \quad g : Q \to R}{fg : P \to R} \quad \frac {f : P \to Q \quad g : R \to S}{f + g : P + R \to Q + S} \\ & \qquad \qquad \qquad \frac {W \text{ monomial} \quad P,Q \text{ polynomial} \quad f : P + W \to Q + W}{\mathsf{Tr}^W_{P,Q}(f) : P \to Q} \end{align*}
These arrows are subject to the axioms of a uniformly traced distributive monoidal category. We give these explicitly in stages. At each stage, we will inductively construct the relevant structural morphisms and then give the corresponding equations.
First, we ensure that
$(\mathbb{A},+,0)$
is a monoidal category. This requires an identity morphism
$1_P : P \to P$
for any polynomial
$P$
, which we define inductively. Any such polynomial
$P$
is either
$0$
, in which case
$1_0$
exists by assumption, or
$U+Q$
for some monomial
$U$
and polynomial
$Q$
, in which case we define
$1_{U+Q} = 1_U + 1_Q$
, noting that
$1_U$
is assumed to exist for all monomials
$U$
. Now the following equations ensure that
$(\mathbb{A},+,0)$
is in fact monoidal:
\begin{gather*} \textbf {[S1]} (fg)h = f(gh) \quad \textbf {[S2]} 1_P f = f = f 1_Q\\ \textbf {[S3]} (f + g)(h + k) = fh + gk \quad \textbf {[S4]} 1_0 + f = f = f + 1_0 \quad \textbf {[S5]} (f + g) + h = f + (g + h) \end{gather*}
Next, we must ensure that
$(\mathbb{A},+,0,\sigma ^+)$
is a symmetric monoidal category. For any monomial
$U$
, we define
$\sigma ^+_{U,Q}$
for an arbitrary polynomial
$Q$
by structural induction on
$Q$
as in:
\begin{align*} \sigma ^+_{U,0} = 1_U \quad \sigma ^+_{U,V+Q} = (\sigma ^+_{U,V} + 1_Q)(1_V + \sigma ^+_{U,Q}) \end{align*}
and now for any polynomials
$P,Q$
we define
$\sigma ^+_{P,Q}$
by structural induction on
$P$
as in:
\begin{align*} \sigma ^+_{0,Q} = 1_Q \quad \sigma ^+_{U+P,Q} = (1_U + \sigma ^+_{P,Q})(\sigma ^+_{U,Q} + 1_P) \end{align*}
and we may now state the corresponding equations:
\begin{align*} \textbf {[S6]} \sigma ^+_{P,Q}\sigma ^+_{Q,P} = 1_{P+Q} \quad \textbf {[S7]} (f + 1_Q)\sigma ^+_{P',Q} = \sigma ^+_{P,Q}(1_Q + f) \end{align*}
For the cocartesian structure, we define
$\eta _P$
and
$\mu _P$
for arbitrary polynomials
$P$
by structural induction on
$P$
, as in:
\begin{gather*} \eta _0 = 1_0 \quad \eta _{U+P} = \eta _U + \eta _P\\ \mu _0 = 1_0 \quad \mu _{U+P} = (1_U + \sigma ^+_{P,U} + 1_P)(\mu _U + \mu _P) \end{gather*}
and the corresponding equations are as follows:
\begin{gather*} \textbf {[S8]} (\mu _P + 1_P)\mu _P = (1_P + \mu _P)\mu _P \quad \textbf {[S9]} \sigma ^+_{P,P}\mu _P = \mu _P \quad \textbf {[S10]} (\eta _P + 1_P)\mu _P = 1_P\\ \textbf {[S11]} (f + f)\mu _{Q} = \mu _Pf \quad \textbf {[S12]} \eta _Pf = \eta _{Q} \end{gather*}
For any polynomials
$P,Q,R$
and
$f : P+R \to Q+R$
, we define
$\mathsf{Tr}^R_{P,Q}$
by structural induction on
$R$
, as in:
\begin{align*} \mathsf{Tr}^0_{P,Q}(f) = f \quad \mathsf{Tr}^{W+R}_{P,Q}(f) = \mathsf{Tr}^{W}_{P,Q}(\mathsf{Tr}^{R}_{P+W,Q+W}(f)) \end{align*}
with the corresponding equations being:
\begin{gather*} \textbf {[S13]} g\mathsf{Tr}^R_{P,Q}(f)h = \mathsf{Tr}^R_{P',Q'}((g + 1_R)f(h+1_R)) \quad \textbf {[S14]} 1_S + \mathsf{Tr}^R_{P,Q}(f) = \mathsf{Tr}^R_{S+P,S+Q}(1_S + f) \\ \textbf {[S15]} \mathsf{Tr}^R_{P,Q}((1_P + h)f) = \mathsf{Tr}^{R'}_{P,Q}(f(1_Q + h)) \quad \textbf {[S16]} \mathsf{Tr}^P_{P,P}(\sigma ^+_{P,P}) = 1_P \end{gather*}
Moreover, we ask that this trace operator is uniform so that for all polynomials
$P,Q,R,S$
and morphisms
$f : P + S \to Q + S$
,
$g : P + R \to Q + R$
, and
$h : R \to S$
, we have:
\begin{align*} \textbf {[S17]} (1_P + h)f = g(1_Q + h) \Rightarrow \mathsf{Tr}^S_{P,Q}(f) = \mathsf{Tr}^R_{P,Q}(g) \end{align*}
Further, morphisms of
$\mathbb{A}$
are subject to a number of equations concerning
$\mathsf{succ}$
,
$\mathsf{zero}$
, and
$\mathsf{pred}$
:
-
[N1]
$(\mathsf{zero}_{U,V} + \mathsf{succ}_{U,V})\mu _{UNV}\mathsf{pred}_{U,V} = 1_{UV+UNV}$
-
[N2]
$\mathsf{pred}_{U,V}(\mathsf{zero}_{U,V} + \mathsf{succ}_{U,V})\mu _{UNV} = 1_{UNV}$
-
[N3]
$\mathsf{succ}_{U,VNW} \mathsf{succ}_{UNV,W} = \mathsf{succ}_{UNV,W} \mathsf{succ}_{U,VNW}$
-
[N4]
$\mathsf{succ}_{U,VW} \mathsf{zero}_{UNV,W} = \mathsf{zero}_{UNV,W} \mathsf{succ}_{U,VNW}$
-
[N5]
$\mathsf{zero}_{U,VNW} \mathsf{succ}_{UNV,W} = \mathsf{succ}_{UV,W} \mathsf{zero}_{U,VNW}$
-
[N6]
$\mathsf{zero}_{U,VW} \mathsf{zero}_{UNV,W} = \mathsf{zero}_{UV,W} \mathsf{zero}_{U,VNW}$
-
[N7]
$\mathsf{succ}_{U,VNW} \mathsf{pred}_{UNV,W} = \mathsf{pred}_{UNV,W} (\mathsf{succ}_{U,VW} + \mathsf{succ}_{U,VNW})$
-
[N8]
$\mathsf{zero}_{U,VNW} \mathsf{pred}_{UNV,W} = \mathsf{pred}_{UV,W} (\mathsf{zero}_{U,VW} + \mathsf{zero}_{U,VNW})$
-
[N9]
$\mathsf{succ}_{UNV,W} \mathsf{pred}_{U,VNW} = \mathsf{pred}_{U,VNW}(\mathsf{succ}_{UV,W} + \mathsf{succ}_{UNV,W})$
-
[N10]
$\mathsf{zero}_{UNV,W} \mathsf{pred}_{U,VNW} = \mathsf{pred}_{U,VW}(\mathsf{zero}_{UV,W} + \mathsf{zero}_{UNV,W})$
-
[N11]
$\mathsf{pred}_{U,VNW}(\mathsf{pred}_{UV,W} + \mathsf{pred}_{UNV,W})$
$= \mathsf{pred}_{UNV,W}(\mathsf{pred}_{U,VW} + \mathsf{pred}_{U,VNW})(1_{UVW} + \sigma ^+_{UNVW,UVNW} + 1_{UNVNW})$
Morphisms of
$\mathbb{A}$
can be understood as a modified notion of abacus program in which the locations used by the program are tracked explicitly. This modified notion of abacus program has the same expressive power as the original one. Briefly, the arrows of our flowcharts become wires in string diagrams corresponding to the additive structure of
$\mathbb{A}$
, and every such wire is now labeled with the non-repeating list of location names used by the program at that point. Explicitly, there are now three sorts of instruction:
The instructions above middle and above right work as before, although note that the
$X-$
instruction now removes the location
$X$
from the list in the case where it no longer contains counters. The instruction above left is new and adds a new location
$X$
containing no counters to the list. We reiterate that in these diagrams the lists of locations are assumed to be non-repeating, which in particular means that whenever we write
$\Gamma ,X,\Delta$
it is implied that neither
$\Gamma$
nor
$\Delta$
contains
$X$
. These non-repeating lists correspond to the monomial part of objects in
$\mathbb{A}$
with, for example, the list
$X$
,
$Y$
,
$Z$
,
$W$
corresponding to the monomial
$NNNN$
. The other differences from unmodified abacus programs are superficial: instead of directed arrows we draw wires, adopting the convention that a wire connected to the top of an instruction box is “incoming” and an arrow connected to the bottom is “outgoing”. Instruction boxes with multiple in-degree must now be constructed using the cocartesian monoidal structure, and arrows that point “backwards” must be constructed using the trace operator.
The location
$X$
labeling each instruction serves only to indicate a position in the relevant list, and in
$\mathbb{A}$
this positional information is present in the monomial subscripts of
$\mathsf{zero}$
,
$\mathsf{succ}$
, and
$\mathsf{pred}$
. For example, the morphism
$\mathsf{succ}_{NN,N}$
of
$\mathbb{A}$
corresponds to a modified abacus program concerned with a sequence of four locations that has the effect of adding a new counter to the third location in the sequence. This more structural representation means that modified abacus programs which are identical in all but choice of location names correspond to the same morphism of
$\mathbb{A}$
. For example, recall the abacus program that moves all of the counters from location
$X$
to location
$Y$
. From this, one obtains a modified abacus program concerning only locations
$X$
and
$Y$
and the corresponding morphism of
$\mathbb{A}$
as in:
The axioms [N1-N11] of
$\mathbb{A}$
are more easily understood by considering the corresponding abacus program. For example, from this perspective the axiom [N3] states that it does not matter which order one adds counters to distinct locations in:
and the axiom [N11] states something similar, if more involved, about the predecessor operation:
The axioms [N4] through [N10] are of a similar character. The axioms [N1] and [N2] are different, serving to ensure that
$N$
is isomorphic to
$I + N$
. Notice that the none of the equations of
$\mathbb{A}$
change the operational effect of the corresponding abacus program.
We proceed to show that
$\mathbb{A}$
is an Elgot category. First, we require another monoidal structure
$(\mathbb{A},\otimes ,I)$
. We begin with the action of
$\otimes$
on objects. Of course,
$I$
will be the empty monomial. We define
$UQ = U \otimes Q$
for
$U$
monomial and
$P$
polynomial by induction on
$P$
, as in:
\begin{align*} U0 = 0 \quad U(V+Q) = UV + UQ \end{align*}
Next, we define
$PQ = P \otimes Q$
for polynomials
$P,Q$
:
\begin{align*} 0P = P \quad (U+P)Q = UQ + PQ \end{align*}
Put another way, if
$P = \Sigma _i U_i$
and
$Q = \Sigma _j V_j$
then
$P \otimes Q = \Sigma _i (\Sigma _j U_iV_j)$
.
The definition of the multiplicative tensor product on morphisms is rather involved. The first step is to inductively define two endofunctors
$(U \ltimes -)$
and
$(\!- \rtimes U)$
on
$\mathbb{A}$
for any monomial
$U$
as follows:
\begin{align*} \begin{array}{l@{\quad}c@{\quad}c@{\quad}c@{\quad}l} \displaystyle U \ltimes \mathsf{succ}_{V,W} = \mathsf{succ}_{UV,W} & & & & \mathsf{succ}_{V,W} \rtimes U = \mathsf{succ}_{V,WU}\\ \displaystyle U \ltimes \mathsf{zero}_{V,W} = \mathsf{zero}_{UV,W} & & & & \mathsf{zero}_{V,W} \rtimes U = \mathsf{zero} _{V,WU}\\ \displaystyle U \ltimes \mathsf{pred}_{V,W} = \mathsf{pred}_{UV,W} & & & & \mathsf{pred}_{V,W} \rtimes U = \mathsf{pred}_{V,WU}\\ \displaystyle U \ltimes 1_V = 1_{UV} & & & & 1_V \rtimes U = 1_{VU} \\ \displaystyle U \ltimes \eta _V = \eta _{UV} & & & & \eta _V \rtimes U = \eta _{VU} \\ \displaystyle U \ltimes \mu _V = \mu _{UV} & & & & \mu _V \rtimes U = \mu _{VU}\\ \displaystyle U \ltimes 1_0 = 1_0 & & & & 1_0 \rtimes U = 1_0\\ \displaystyle U \ltimes \sigma ^+_{V,W} = \sigma ^+_{UV,UW} & & & & \sigma ^+_{V,W} \rtimes U = \sigma ^+_{VU,WU}\\ \displaystyle U \ltimes fg = (U \ltimes f)(U \ltimes g) & & & & fg \rtimes U = (f \rtimes U)(g \rtimes U)\\ \displaystyle U \ltimes f + g = (U \ltimes f) + (U \ltimes g) & & & & f + g \rtimes U = (f \rtimes U) + (g \rtimes U)\\ \displaystyle U \ltimes \mathsf{Tr}^W_{P,Q} = \mathsf{Tr}^{UW}_{UP,UQ}(U \ltimes f) & & & & \mathsf{Tr}^W_{P,Q} \rtimes U = \mathsf{Tr}^{WU}_{PU,QU}(f \rtimes U)\\ \end{array} \end{align*}
We call
$(U \ltimes -)$
and
$(\!- \rtimes U)$
monomial left whiskering and monomial right whiskering, respectively.
We also require the left distributors. While the right distributors in
$\mathbb{A}$
will be identities, the left distributors
$\delta ^l_{P,Q,R}$
are defined by induction on
$P$
as in:
\begin{align*} \delta ^l_{0,Q,R} = 1_0 \quad \delta ^l_{U+P,Q,R} = (1_{UQ+UR} + \delta ^l_{P,Q,R})(1_{UQ} + \sigma ^+_{UR,PQ} + 1_{PR}) \end{align*}
Notice that for monomials
$U$
, we have
$\delta ^l_{U,Q,R} = \delta ^l_{U+0,Q,R} = 1_{UP + UQ}$
.
Now, for any polynomial
$P$
in
$\mathbb{A}$
we define an endofunctor
$(P \ltimes -)$
of
$\mathbb{A}$
called polynomial left whiskering, defined on
$f : R \to S$
as in:
\begin{align*} 0 \ltimes f = 1_0 \quad U + P \ltimes f = (U \ltimes f) + (P \ltimes f) \end{align*}
Similarly, we define an endofunctor
$(\!- \rtimes P)$
of
$\mathbb{A}$
called polynomial right whiskering, defined on
$f : R \to S$
as in:
\begin{align*} f \rtimes 0 = 1_0 \quad f \rtimes U + P = \delta ^l_{R,U,P}((f \rtimes U) + (f \rtimes P))(\delta ^l_{S,U,P})^{-1} \end{align*}
Finally, the action of the multiplicative tensor product on morphsims
$f : R \to S$
and
$g : R' \to S'$
is given by
$f \otimes g = (f \rtimes R')(S \ltimes g) = (R \ltimes g)(f \rtimes S')$
and we have:
Theorem 5.2.
$(\mathbb{A},(+,0,\sigma ^+),(\otimes ,I),(\mu ,\eta ),\mathsf{Tr},(1,1),(\delta ^l,1),(N,(\mathsf{zero}_{I,I}+\mathsf{succ}_{I,I})\mu _N))$
is a right-strict Elgot category.
Proof. See Appendix B.
The construction of the category
$\mathbb{A}$
and the proof of Theorem5.2 are adapted from the construction of the category of tape diagrams over a monoidal signature and the proof that it forms a rig category with finite biproducts found in Section 5 of Bonchi et al. (Reference Bonchi, Di Giorgio and Santamaria2023). Therein, the authors begin with a monoidal signature
$\Sigma$
, construct the symmetric monoidal category
$C_\Sigma$
that it presents, and then freely add finite biproducts to the underlying category. The finite biproducts become the additve structure of the resulting rig category, while the multiplicative strucutre is essentially inherited from the monoidal structure of
$C_\Sigma$
. While this approach can also be used to construct a distributive monoidal category by freely adding finite coproducts instead of finite biproducts, it is not entirely suitable for the situation considered in this paper. In particular, we cannot include the generating morphisms
$\mathsf{pred}_{U,V} : UNV \to UV + UNV$
as part of a monoidal signature since their codomain involves the additive structure. We instead perform the construction in a single step, relying on the axioms
$\textbf {[N3-N11]}$
to ensure that the result is a distributive monoidal category. Curiously, for both the original construction of Bonchi et al. (Reference Bonchi, Di Giorgio and Santamaria2023) and our construction here to work in the case where the additive structure is traced, the trace operator must be assumed to be uniform. This is also observed in more recent work on tape diagrams (Bonchi et al. (Reference Bonchi, Di Giorgio and Di Lavore2024)) involving the trace.
The promised initiality result follows almost immediately:
Theorem 5.3.
$(\mathbb{A},(+,0,\sigma ^+),(\otimes ,I),(\mu ,\eta ),\mathsf{Tr},(1,1),(\delta ^l,1),(N,(\mathsf{zero}_{I,I}+\mathsf{succ}_{I,I})\mu _N))$
is initial in the category of right-strict Elgot categories and functors between them that strictly preserve the Elgot category structure.
Proof.
Say we have another right-strict Elgot category
$(\mathbb{C},(+,0,\sigma ^+),(\otimes ,I),(\mu ,\eta ),\mathsf{Tr},(1,1),$
$(\delta ^l,1),(N,\iota ))$
. Any functor
$F : \mathbb{A} \to \mathbb{C}$
that strictly preserves the Elgot category structure must have
$FN = N$
. Since
$F$
preserves the multiplicative monoidal structure this means that
$F(N^n) = F(N)^n$
, and so the value of the object mapping of
$F$
on monomials is forced. The object mapping of
$F$
on the polynomials is forced because
$F$
is assumed to strictly preserve the cocartesian monoidal structure.
On morphisms, the requirements that
$F$
be a functor, strictly preserves the cocartesian monoidal structure, and strictly preserves the trace operator means that the only choice we might have is where to map the
$\mathsf{zero}$
,
$\mathsf{succ}$
, and
$\mathsf{pred}$
arrows. Since
$F$
strictly preserves the distinguished object
$N$
and isomorphism
$\iota : I+N \to N$
, we must have 
. Together with the assumption that
$F$
strictly preserves the multiplicative monoidal structure this means that we must have 
Similarly, we must have
$F(\mathsf{zero}_{U,V}) = 1_U \otimes \mathsf{zero}_{I,I} \otimes 1_V$
. Since
$F$
is a functor and
$\mathsf{pred}_{U,V}$
is inverse to
$(\mathsf{zero}_{U,V} + \mathsf{succ}_{U,V})\mu _{UNV}$
in
$\mathbb{A}$
, we know that
$F(\mathsf{pred}_{U,V})$
must be the inverse of
$F((\mathsf{succ}_{U,V} + \mathsf{zero}_{U,V})\mu _{UNV})$
, and so the definition of the arrow mapping of
$F$
is forced. The claim follows.
Finally, our category of abacus programs strongly represents the partial recursive functions.
Theorem 5.4.
$\mathbb{A}$
strongly represents the partial recursive functions.
Proof.
We show that the conditions of Theorem3.10 are satisfied. By assumption, we have that
$\iota : I + N \to N$
is an isomorphism. Obviously,
$\underline {0} \neq \underline {1}$
in
$\mathbb{A}$
. Notice that the partial function
$\overline {f} : \mathbb{N}^n \to \mathbb{N}$
strongly represented by some morphism
$f : N^n \to N$
of
$\mathbb{A}$
coincides with the partial function implemented by the associated abacus program. It follows that any such
$\overline {f}$
is partial recursive. That the remaining conditions are satisfied follows from Lemma 4.2.
In particular, since any partial function that is strongly representable in
$\mathbb{A}$
is partial recursive, we have:
Corollary 5.5.
$\mathbb{A}$
strongly represents all and only the partial recursive functions.
6. Conclusions and Future Work
We have introduced (pre-)Elgot categories and shown that any such category represents the partial recursive functions. Moreover, we have constructed an initial Elgot category of abacus programs and have shown that it strongly represents the partial recursive functions, and so, in a sense, generates them.
We end by mentioning a few directions for future work. First, it seems very sensible to impose further assumptions on Elgot categories to the effect that the multiplicative monoidal structure forms a cartesian restriction category (see e.g., Cockett and Lack (Reference Cockett and Lack2007); Di Liberti et al. (Reference Di Liberti, Loregian, Nester and Sobociński2021); Nester (Reference Nester2024)). This more structured setting would more faithfully represent the partial recursive functions, and one imagines that stronger results would be obtainable. In particular, it seems likely that the initial such category is a Turing category Cockett and Hofstra (Reference Cockett and Hofstra2008).
Second, there are natural questions concerning the relationship between Elgot categories and Elgot monads (Adámek et al. (Reference Adámek, Milius and Velebil2010)). The identity functor on any Elgot category is an Elgot monad, and we might for example ask when the Kleisli category of an Elgot monad is an Elgot category. Moreover, the reformulation of Elgot monads as while monads given by Goncharov (Reference Goncharov2022) suggests that the ideas presented here might lead to a categorical semantics for at least some of the “While” languages one encounters in computer science.
Appendix
A. Distributive Monoidal Categories
Definition A.1.
A
$\text{distributive monoidal category}$
is a tuple
$(\mathbb{C},(+,0,\sigma ^+),(\otimes ,I),(\mu ,\eta ),(\lambda ^\bullet ,\rho ^\bullet ), (\delta ^l,\delta ^r))$
such that:
-
•
$((\mathbb{C},+,0,\sigma ^+),(\mu ,\eta ))$
is a cocartesian monoidal category.
-
•
$(\mathbb{C},\otimes ,I)$
is a monoidal category.
-
•
$\lambda ^\bullet$
and
$\rho ^\bullet$
are natural isomorphisms with components
$\lambda ^\bullet _A : 0 \otimes A \to 0$
and
$\rho ^\bullet _A : A \otimes 0 \to 0$
called the left and right
$\text{annihilator}$
, respectively.
-
•
$\delta ^l$
and
$\delta ^r$
are natural isomorphisms with components
called the left and right
\begin{align*} \delta ^l_{A,B,C} : A \otimes (B + C) \to (A \otimes B) + (A \otimes C) \quad \delta ^r_{A,B,C} : (A + B) \otimes C \to (A \otimes C) + (B \otimes C) \end{align*}
$\text{distributor}$
, respectively.
-
• The coherence axioms [B1] - [B22] are satisfied. Before enumerating these axioms, we recall a common convention: When referring to the objects of a distributive monoidal category we will denote the multiplicative tensor product
$\otimes$
by juxtaposition. For example,
$A \otimes B$
becomes
$AB$
,
$A \otimes B \otimes C$
becomes
$ABC$
, and
$A \otimes (B + (C \otimes D))$
becomes
$A(B + CD)$
. The coherence axioms ask that for all objects
$A,B,C,D$
of
$\mathbb{C}$
, we have:
Definition A.2.
A distributive monoidal category
$(\mathbb{C},(+,0,\sigma ^+),(\otimes ,I),(\mu ,\eta ),(\lambda ^\bullet ,\rho ^\bullet ),(\delta ^l,\delta ^r))$
is said to be
$\text{right-strict}$
in case
$\lambda ^\bullet$
,
$\rho ^\bullet$
, and
$\delta ^r$
are identity natural transformations. Explicitly, a
$\text{right-strict distributive monoidal category}$
is a tuple
\begin{equation*} (\mathbb{C},(+,0,\sigma ^+),(\otimes ,I),(\mu ,\eta ),\delta ^l) \end{equation*}
such that:
-
•
$(\mathbb{C},+,0,\sigma ^+)$
is a symmetric strict monoidal category.
-
•
$(\mathbb{C},\otimes ,I)$
is a strict monoidal category.
-
•
$\delta ^l$
is a natural isomorphism with components
$\delta ^l_{A,B,C} : A(B + C) \to AB + AC$
. That is, for all
$f : A \to A', g : B \to B', h : C \to C'$
of
$\mathbb{C}$
we must have:
-
• For all objects
$A,B,C$
of
$\mathbb{C}$
, we have:
Similarly, for all morphisms
\begin{align*} A0 = 0 \quad 0A = 0 \quad (A + B)C = AC + BC \end{align*}
$f,g,h$
of
$\mathbb{C}$
we have:
\begin{align*} f \otimes 1_0 = 1_0 \quad 1_0 \otimes f = 1_0 \quad (f + g) \otimes h = (f \otimes h) + (g \otimes h) \end{align*}
-
• The following equations are satisfied for all objects
$A,B,C,D$
of
$\mathbb{C}$
:
\begin{align*} \delta ^l_{0,A,B} = 1_0 \quad &\delta ^l_{A,0,B} = 1_{AB} \quad \delta ^l_{A,B,0} = 1_{AB}\quad \delta ^l_{I,A,B} = 1_{A + B} \quad \delta ^l_{A,B,C} \sigma ^+_{AB,AC} = (1_A \otimes \sigma ^+_{B,C})\delta ^l_{A,C,B}\\ \sigma ^+_{AC,BC} &= \sigma ^+_{A,B} \otimes 1_C \quad \delta ^l_{A,B+ C,D}(\delta ^l_{A,B,C} + 1_{AD}) = \delta ^l_{A,B,C + D}(1_{AB} + \delta ^l_{A,C,D})\\ \delta ^l_{AB,C,D} &= (1_A \otimes \delta ^l_{B,C,D})\delta ^l_{A,BC,BD} \quad \delta ^l_{A,BD,CD} = \delta ^l_{A,B,C} \otimes 1_D\\ \delta ^l_{A + B,C,D} &= (\delta ^l_{A,C,D} + \delta ^l_{B,C,D})(1_{AC} + \sigma ^+_{AD,BC} + 1_{BD}) \end{align*}
B. Proof of Theorem5.2
This section contains the proof of Theorem5.2, restated here as TheoremB.11. First, notice that by construction, we have:
Lemma B.1.
-
•
$((\mathbb{A},+,0,\sigma ^+),(\mu ,\eta ))$
is a cocartesian monoidal category.
-
•
$((\mathbb{A},+,0,\sigma ^+),\mathsf{Tr})$
is a uniform traced monoidal category.
To show that
$\mathbb{A}$
is an Elgot category, we must show that our proposed multiplicative monoidal structure satisfies the axioms of a monoidal category, and that it distributes over the existing additive structure. We begin by showing that our
$\otimes$
operation forms a monoid on the objects of
$\mathbb{A}$
:
Lemma B.2.
For all polynomials
$P,Q,R$
and monomials
$U$
:
-
(i)
$P0 = 0$
-
(ii)
$U(Q+R) = UQ + UR$
-
(iii)
$(P+Q)R = PR + QR$
-
(iv)
$P(QR) = (PQ)R$
-
(v)
$IP = P$
-
(vi)
$PI = P$
Proof. Straightforward structural induction.
Next, we establish some elementary properties of monomial whiskering:
Lemma B.3.
For all monomials
$U$
and polynomials
$Q,R,S$
, we have:
\begin{align*} \begin{array}{r@{\quad}l@{\quad}r@{\quad}l} \text{(i)} & U \ltimes 1_Q = 1_{UQ} & \text{(vi)} & 1_Q \rtimes U = 1_{QU}\\ \text{(ii)} & U \ltimes \sigma ^+_{Q,R} = \sigma ^+_{UQ,UR} & \text{(vii)} &\sigma ^+_{P,Q} \rtimes U = \sigma ^+_{PU,QU}\\ \text{(iii)} & U \ltimes \eta _Q = \eta _{UQ} & \text{(viii)} & \eta _Q \rtimes U = \eta _{QU}\\ \text{(iv)} & U \ltimes \mu _Q = \mu _{UQ} & \text{(ix)} & \mu _Q \rtimes U = \mu _{QU}\\ \text{(v)} & U \ltimes \mathsf{Tr}^Q_{R,S}(f) = \mathsf{Tr}^{UR}_{UP,UQ}(U \ltimes f) & \text{(x)} & \mathsf{Tr}^R_{P,Q}(f) \rtimes U = \mathsf{Tr}^{RU}_{PU,QU}(f \rtimes U)\\ \end{array} \end{align*}
Proof.
-
(i) By induction on
$Q$
. The base case is
$U \ltimes 1_0 = 1_0 = 1_{U0}$
. For the inductive case suppose
$U \ltimes 1_Q = 1_{UQ}$
. Then we have:and the claim follows.
\begin{align*} & U \ltimes 1_{V + Q} = U \ltimes (1_V + 1_Q) = (U\ltimes 1_V) + (U\ltimes 1_Q) = 1_{UV} + 1_{UQ} = 1_{U(V+Q)} \end{align*}
-
(ii) First, we show that
$U \ltimes \sigma ^+_{V,R} = \sigma ^+_{UV,UR}$
by induction on
$R$
. The base case is
$U \ltimes \sigma ^+_{V,0} = U \ltimes 1_V = 1_{UV} = \sigma ^+_{UV,U0}$
. For the inductive case, suppose
$U \ltimes \sigma ^+_{V,R} = \sigma ^+_{UV,UR}$
. Then we have:and it follows that
\begin{align*} & U \ltimes \sigma ^+_{V,W+R} = U \ltimes (\sigma ^+_{V,W} + 1_R)(1_W + \sigma ^+_{V,R}) \\&\quad = ((U \ltimes \sigma ^+_{V,W}) + 1_{UR})(1_{UW} + (U \ltimes \sigma ^+_{V,R})) \\&\quad = (\sigma ^+_{UV,UW} + 1_{UR})(1_{UW} + \sigma ^+_{UV,UR}) \\&\quad = \sigma ^+_{UV,UW+UR} = \sigma ^+_{UV,U(W+R)} \end{align*}
$U \ltimes \sigma ^+_{V,R} = \sigma ^+_{UV,UR}$
. We proceed to prove the full claim by induction on
$Q$
. The base case is
$U \ltimes \sigma ^+_{0,R} = U \ltimes 1_R = 1_{UR} = \sigma ^+_{U0,UR}$
. For the inductive case, suppose
$U \ltimes \sigma ^+_{Q,R} = \sigma ^+_{UQ,UR}$
. Then we have:and the claim follows.
\begin{align*} & U \ltimes \sigma ^+_{V+Q,R} = U \ltimes (1_V + \sigma ^+_{Q,R})(\sigma ^+_{V,R} + 1_Q) \\&\quad = (1_{UV} + (U \ltimes \sigma ^+_{Q,R}))((U \ltimes \sigma ^+_{V,R}) + 1_{UQ}) \\&\quad = (1_{UV} + \sigma ^+_{UQ,UR})(\sigma ^+_{UV,UR} + 1_{UQ}) \\&\quad = \sigma ^+_{UV+UQ,UR} = \sigma ^+_{U(V+Q),UR} \end{align*}
-
(iii) By induction on
$Q$
. The base case is
$U \ltimes \eta _0 = U \ltimes 1_0 = 1_0 = \eta _0 = \eta _{U0}$
. For the inductive case, suppose
$U \ltimes \eta _Q = \eta _{UQ}$
. Then we have:and the claim follows.
\begin{align*} & U \ltimes \eta _{V + Q} = U \ltimes (\eta _V + \eta _Q) = (U \ltimes \eta _V) + (U \ltimes \eta _Q) = \eta _{UV} + \eta _{UQ} = \eta _{U(V+Q)} \end{align*}
-
(iv) By induction on
$Q$
. The base case is
$U \ltimes \mu _0 = U \ltimes 1_0 = 1_0 = \mu _0 = \mu _{U0}$
. For the inductive case, suppose
$U \ltimes \mu _Q = \mu _{UQ}$
. Then we have:and the claim follows.
\begin{align*} & U \ltimes \mu _{V+Q} = U \ltimes (1_V + \sigma ^+_{Q,V} + 1_Q)(\mu _V + \mu _Q) \\&\quad = (1_{UV} + \sigma ^+_{UQ,UV} + 1_{UQ})((U \ltimes \mu _V) + (U \ltimes \mu _Q)) \\&\quad = (1_{UV} + \sigma ^+_{UQ,UV} + 1_{UQ})(\mu _{UV} + \mu _{UQ}) \\&\quad = \mu _{UV + UQ} = \mu _{U(V+Q)} \end{align*}
-
(v) The base case is
$U \ltimes \mathsf{Tr}^0_{R,S}(f) = U \ltimes f = \mathsf{Tr}^{U0}_{UR,US}(U \ltimes f)$
. For the inductive case, suppose
$U \ltimes \mathsf{Tr}^Q_{R',S'}(f) = \mathsf{Tr}^{UQ}_{UR',US'}(U \ltimes f)$
for all polynomials
$R',S'$
. Then we have:and the claim follows.
\begin{align*} & U \ltimes \mathsf{Tr}^{V + Q}_{R,S}(f) = U \ltimes \mathsf{Tr}^V_{R,S}(\mathsf{Tr}^Q_{R+V,S+V}(f)) \\&\quad = \mathsf{Tr}^{UV}_{UR,US}(U \ltimes \mathsf{Tr}^Q_{R+V,S+V}(f)) = \mathsf{Tr}^{UV}_{UR,US}(\mathsf{Tr}^{UQ}_{U(R+V),S(R+V)}(U \ltimes f)) \\&\quad = \mathsf{Tr}^{UV+UQ}_{UR,US}(U \ltimes f) = \mathsf{Tr}^{U(V+Q)}_{UR,US}(U \ltimes f) \end{align*}
-
(vi) By induction on
$Q$
. The base case is
$1_0 \rtimes U = 1_0 = 1_{0U}$
. For the inductive case, suppose
$1_P \rtimes U = 1_{PU}$
. Then we have:and the claim follows.
\begin{align*} & 1_V \rtimes (U+P) = \delta ^l_{V,U,P}((1_V \rtimes U) + (1_V \rtimes P))(\delta ^l_{V,U,P})^{-1} \\&\quad = 1_{VU+VP}(1_{VU} + 1_{VP})1_{VU+VP} = 1_{V(U+P)} \end{align*}
-
(vii) First, we show
$\sigma ^+_{V,Q} \rtimes U = \sigma ^+_{VU,QU}$
for all monomials
$V$
, polynomials
$Q$
. We proceed by induction on
$Q$
. The base case is
$\sigma ^+_{V,0} \rtimes U = 1_V \rtimes U = 1_{VU} = \sigma ^+_{VU,0U}$
. For the inductive case, suppose
$\sigma ^+_{V,Q} \rtimes U = \sigma ^+_{VU,QU}$
. Then we have:and it follows that
\begin{align*} & \sigma ^+_{V,W + Q} \rtimes U = (\sigma ^+_{V,W} + 1_Q)(1_W + \sigma ^+_{V,Q}) \rtimes U \\&\quad = (\sigma ^+_{VU,WU} + 1_{QU})(1_{WU} + \sigma ^+_{VU,QU}) = \sigma ^+_{VU,WU + QU} = \sigma ^+_{VU,(W+Q)U} \end{align*}
$\sigma ^+_{V,Q} \rtimes U = \sigma ^+_{VU,QU}$
for all monomials
$V$
, polynomials
$Q$
. We are now ready to prove the claim, which we do by induction on
$P$
. The base case is
$\sigma ^+_{0,Q} \rtimes U = 1_Q \rtimes U = 1_{QU} = \sigma ^+_{0U,QU}$
. For the inductive case, suppse
$\sigma ^+_{P,Q} \rtimes U = \sigma ^+_{PU,QU}$
. Then we have:and the claim follows.
\begin{align*} & \sigma ^+_{V+P,Q} \rtimes U = (1_V + \sigma ^+_{P,Q})(\sigma ^+_{V,Q} + 1_P) \rtimes U \\&\quad = (1_{VU} + \sigma ^+_{PU,QU})(\sigma ^+_{VU,QU} + 1_{PU}) = \sigma ^+_{VU + PU,QU} = \sigma ^+_{(V+P)U,QU} \end{align*}
-
(viii) By induction on
$Q$
. The base case is
$\eta _0 \rtimes U = 1_0 \rtimes U = 1_0 = \eta _0 = \eta _{0U}$
. For the inductive case, suppose
$\eta _Q \rtimes U = \eta _{QU}$
. Then we have:and the claim follows.
\begin{align*} & \eta _{V + Q} \rtimes U = (\eta _{V} + \eta _{Q})\rtimes U = (\eta _{V} \rtimes U) + (\eta _{Q} \rtimes U) = \eta _{VU} + \eta _{QU} = \eta _{(V+Q)U} \end{align*}
-
(ix) By induction on
$Q$
. The base case is
$\mu _0 \rtimes U = 1_0 \rtimes U = 1_0 = \mu _0 = \mu _{0U}$
. For the inductive case, suppose
$\mu _Q \rtimes U = \mu _{QU}$
. Then we have:and the claim follows.
\begin{align*} & \mu _{V+Q} \rtimes U = (1_V + \sigma ^+_{Q,V} + 1_Q)(\mu _V + \mu _Q) \rtimes U \\&\quad = (1_{VU} + \sigma ^+_{QU,VU} + 1_{QU})(\mu _{VU} + \mu _{QU}) \\&\quad = \mu _{VU+QU} = \mu _{(V+Q)U} \end{align*}
-
(x) By induction on
$Q$
. The base case is
$\mathsf{Tr}^0_{P,Q}(f) \rtimes U = f \rtimes U$
. For the inductive case, suppose
$\mathsf{Tr}^{R}_{P,Q}(f) \rtimes U = \mathsf{Tr}^{RU}_{PU,QU}(f \rtimes U)$
for all
$P,Q$
. Then we have:and the claim follows.
\begin{align*} & \mathsf{Tr}^{W+R}_{P,Q}(f) \rtimes U = \mathsf{Tr}^W_{P,Q}(\mathsf{Tr}^R_{P+W,Q+W}(f)) \rtimes U = \mathsf{Tr}^{WU}_{PU,QU}(\mathsf{Tr}^R_{P+W,Q+W}(f) \rtimes U) \\&\quad = \mathsf{Tr}^{WU}_{PU,QU}(\mathsf{Tr}^{RU}_{(P+W)U,(Q+W)U}(f \rtimes U)) = \mathsf{Tr}^{WU}_{PU,QU}(\mathsf{Tr}^{RU}_{PU+WU,QU+WU}(f \rtimes U)) \\&\quad = \mathsf{Tr}^{WU + RU}_{PU,QU}(f \rtimes U) = \mathsf{Tr}^{(W+R)U}_{PU,QU}(f \rtimes U) \end{align*}
The analogous properties of polynoimial whiskering are as follows:
Lemma B.4. For polynomial whiksering, we have:
\begin{align*} \begin{array}{r@{\quad}l@{\quad}r@{\quad}l} \displaystyle \text{(i)} & P \ltimes 1_Q = 1_{PQ} & \text{(ix)} & 1_Q \rtimes P = 1_{QP}\\ \displaystyle \text{(ii)} & (P \ltimes \sigma ^+_{Q,R})\delta ^l_{P,R,Q} = \delta ^l_{P,Q,R}\sigma ^+_{PQ,PR} & \text{(x)} & \sigma ^+_{P,Q} \rtimes R = \sigma ^+_{PR,QR}\\ \displaystyle \text{(iii)} & P \ltimes \eta _Q = \eta _{PQ} & \text{(xi)} & \eta _Q \rtimes P = \eta _{QP}\\ \displaystyle \text{(iv)} & P \ltimes \mu _Q = \delta ^l_{P,Q,Q}\mu _{PQ} & \displaystyle \text{(xii)} & \mu _Q \rtimes P = \mu _{QP}\\ \displaystyle \text{(v)} & P \ltimes \mathsf{Tr}^Q_{R,S}(f) = \mathsf{Tr}^{PQ}_{PR,PS}((\delta ^l_{P,R,Q})^{-1}(P \ltimes f)\delta ^l_{P,S,Q}) & \displaystyle \text{(xiii)} & \mathsf{Tr}^R_{P,Q}(f) \rtimes S = \mathsf{Tr}^{RS}_{PS,QS}(f \rtimes S)\\ \displaystyle \text{(vi)} & P \ltimes 1_0 = 1_0 & \text{(xiv)} & 1_0 \rtimes P = 1_0\\ \displaystyle \text{(vii)} & P \ltimes ts = (P \ltimes t)(P \ltimes s) & \text{(xv)} & ts \rtimes P = (t \rtimes P)(s \rtimes P)\\ \displaystyle \text{(viii)} & (P \ltimes t + s)\delta ^l_{P,Q_1,Q_2} = \delta ^l_{P,P_1,P_2}((P \ltimes t) + (P \ltimes s)) & \text{(xvi)} & t + s \rtimes P = (t \rtimes P) + (s \rtimes P)\\ \end{array} \end{align*}
Proof.
-
(i) By induction on P. The base case is
$0 \ltimes 1_Q = 1_0 = 1_{0Q}$
. For the inductive case, suppose
$P \ltimes 1_Q = 1_{PQ}$
. Then using Lemma B.3 we have:and the claim follows.
\begin{align*} & (U + P) \ltimes 1_Q = (U \ltimes 1_Q) + (P \ltimes 1_Q) = 1_{UQ} + 1_{PQ} = 1_{(U + P)Q} \end{align*}
-
(ii) By induction on
$P$
. The base case is
$(0 \ltimes \sigma ^+_{Q,R})\delta ^l_{0,R,Q} = 1_0 = \sigma ^+_{0,0} = \delta ^l_{0,Q,R}\sigma ^+_{0Q,0R}$
. For the inductive case, suppose
$(P \ltimes \sigma ^+_{Q,R})\delta ^l_{P,R,Q} = \delta ^l_{P,Q,R}\sigma ^+_{PQ,PR}$
. Then using Lemma B.3, we have:
\begin{align*} & ((U + P) \ltimes \sigma ^+_{Q,R})\delta ^l_{U + P,R,Q} \\&\quad = ((U \ltimes \sigma ^+_{Q,R}) + (P \ltimes \sigma ^+_{Q,R}))(1_{UR+UQ} + \delta ^l_{P,R,Q})(1_{UR} + \sigma ^+_{UQ,PR} + 1_{PQ}) \end{align*}
and the claim follows.
\begin{align*} &\quad = (\sigma ^+_{UQ,UR} + (P \ltimes \sigma ^+_{Q,R})\delta ^l_{P,R,Q})(1_{UR} + \sigma ^+_{UQ,PR} + 1_{PQ}) \\&\quad = (\sigma ^+_{UQ,UR} + \delta ^l_{P,Q,R}\sigma ^+_{PQ,PR})(1_{UR} + \sigma ^+_{UQ,PR} + 1_{PQ}) \\&\quad = (1_{UQ+UR} + \delta ^l_{P,Q,R})(1_{UQ} + \sigma ^+_{UR,PQ} + 1_{PR})\\&\quad \hspace {0.5cm}(1_{UQ} + \sigma ^+_{PQ,UR} + 1_{PR})(\sigma ^+_{UQ,UR} + \sigma ^+_{PQ,PR})(1_{UR} + \sigma ^+_{UQ,PR} + 1_{PQ}) \\&\quad = \delta ^l_{U+P,Q,R}\sigma ^+_{UQ+PQ,UR+PR} = \delta ^l_{U+P,Q,R}\sigma ^+_{(U+P)Q,(U+P)R} \end{align*}
-
(iii) By induction on
$P$
. The base case is
$0 \ltimes \eta _Q = 1_0 = \eta _0 = \eta _{0Q}$
. For the inductive case, suppose
$P \ltimes \eta _Q = \eta _{PQ}$
. Then using Lemma B.3, we have:and the claim follows.
\begin{align*} & (U + P) \ltimes \eta _Q = (U \ltimes \eta _Q) + (P \ltimes \eta _Q) = \eta _{UQ} + \eta _{PQ} = \eta _{(U+P)Q} \end{align*}
-
(iv) By induction on
$P$
. The base case is
$0 \ltimes \mu _Q = 1_0 = \mu _0 = \mu _{0Q}$
. For the inductive case, suppose
$P \ltimes \mu _Q = \delta ^l_{P,Q,Q}\mu _{PQ}$
. Then using Lemma B.3, we have:and the claim follows.
\begin{align*} & (U + P) \ltimes \mu _Q = (U \ltimes \mu _Q) + (P \ltimes \mu _Q) \\&\quad = \mu _{UQ} + \delta ^l_{P,Q,Q}\mu _{PQ} = (1_{UQ+UQ} + \delta ^l_{P,Q,Q})(\mu _{UQ} + \mu _{PQ}) \\&\quad = (1_{UQ+UQ} + \delta ^l_{P,Q,Q})(1_{UQ} + \sigma ^+_{UQ,PQ} + 1_{UQ})(1_{UQ} + \sigma ^+_{PQ,UQ} + 1_{PQ})(\mu _{UQ} + \mu _{PQ}) \\&\quad = \delta ^l_{U+P,Q,Q}\mu _{(U+P)Q} \end{align*}
-
(v) By induction on
$P$
. The base case is
$0 \ltimes \mathsf{Tr}^Q_{R,S}(f) = 1_0 = \mathsf{Tr}^0_{0,0}(1_0) = \mathsf{Tr}^{0Q}_{0R,0S}((\delta ^l_{0,R,Q})^{-1}(0 \ltimes f)\delta ^l_{0,S,Q})$
. For the inductive case, suppose
$P \ltimes \mathsf{Tr}^Q_{R,S}(f) = \mathsf{Tr}^{PQ}_{PR,PS}((\delta ^l_{P,R,Q})^{-1}(P \ltimes f)\delta ^l_{P,S,Q})$
. Then using Lemma B.3, we have:where the marked equation (
\begin{align*} & (U + P) \ltimes \mathsf{Tr}^{Q}_{R,S}(f) = (U \ltimes \mathsf{Tr}^{Q}_{R,S}(f)) + (P \ltimes \mathsf{Tr}^Q_{R,S}(f)) \\&\quad = \mathsf{Tr}^{UQ}_{UR,US}(U \ltimes f) + \mathsf{Tr}^{PQ}_{PR,PS}((\delta ^l_{P,R,Q})^{-1}(P \ltimes f)\delta ^l_{P,S,Q}) \\&\quad \stackrel {*}{=} \mathsf{Tr}^{UQ+PQ}_{UR+PR,US+PS}( (1_{UR} + \sigma ^+_{PR,UQ} + 1_{PQ})(1_{UR+UQ} + (\delta ^l_{P,R,Q})^{-1})\\&\quad \hspace {0.5cm}((U \ltimes f) + (P \ltimes f))(1_{US+UQ} + \delta ^l_{P,S,Q})(1_{US} + \sigma ^+_{UQ,PS} + 1_{PQ})) \\&\quad = \mathsf{Tr}^{(U+P)Q}_{(U+P)R,(U+P)S}((\delta ^l_{U+P,R,Q})^{-1}((U+P) \ltimes f)\delta ^l_{U+P,S,Q}) \end{align*}
$\stackrel {*}{=}$
) holds as in:The claim follows. -
(vi) By induction on
$P$
. The base case is
$0 \ltimes 1_0 = 1_0$
. For the inductive case, suppose
$P \ltimes 1_0 = 1_0$
. Then we have:and the claim follows.
\begin{align*} & (U + P) \ltimes 1_0 = (U \ltimes 1_0) + (P \ltimes 1_0) = 1_0 + 1_0 = 1_0 \end{align*}
-
(vii) By induction on P. The base case is
$0 \ltimes ts = 1_0 = (0 \ltimes t)(0 \ltimes s)$
. For the inductive case, suppose
$P \ltimes ts = (P \ltimes t)(P \ltimes s)$
. Then we have:and the claim follows.
\begin{align*} & (U + P) \ltimes ts = (U \ltimes ts) + (P \ltimes ts) = (U \ltimes t)(U \ltimes s) + (P \ltimes t)(P \ltimes s) \\&\quad = ((U \ltimes t) + (P \ltimes T))((U \ltimes s) + (P \ltimes S)) = ((U + P) \ltimes t)((U + P) \ltimes s) \end{align*}
-
(viii) By induction on
$P$
. The base case is
$(0 \ltimes (t + s))\delta ^l_{0,Q_1,Q_2} = 1_0 = 1_0 + 1_0 = \delta ^l_{0,P_1,P_2}((0 \ltimes t) + (0 \ltimes s))$
. For the inductive case, suppose
$(P \ltimes (t + s))\delta ^l_{P,Q_1,Q_2} = \delta ^l_{P,P_1,P_2}((P \ltimes t) + (P \ltimes s))$
. Then we have:and the claim follows.
\begin{align*} & ((U+P) \ltimes (t + s))\delta ^l_{U + P,Q_1,Q_2} \\&\quad = ((U \ltimes (t + s)) + (P \ltimes (t + s))\delta ^l_{P,Q_1,Q_2})(1_{UQ_1} + \sigma ^+_{UQ_2,PQ_1} + 1_{PQ_2}) \\&\quad = ((U \ltimes t) + (U \ltimes s) + \delta ^l_{P,P_1,P_2}((P \ltimes t) + (P \ltimes s)))(1_{UQ_1} + \sigma ^+_{UQ_2,PQ_1} + 1_{PQ_2}) \\&\quad = (1_{UP_1 + UP_2} + \delta ^l_{P,P_1,P_2})(1_{UP_1} + \sigma ^+_{UP_2,PP_1} + 1_{PP_2})((U \ltimes t) + (P \ltimes t) + (U \ltimes s) + (P \ltimes s)) \\&\quad = \delta ^l_{U+P,P_1,P_2}(((U+P) \ltimes t) + ((U+P) \ltimes s)) \end{align*}
-
(ix) By induction on
$P$
. The base case is
$1_Q \rtimes 0 = 1_0 = 1_{Q0}$
. For the inductive case, suppose
$1_Q \rtimes P = 1_{QP}$
. Then using Lemma B.3, we have:and the claim follows.
\begin{align*} & 1_Q \rtimes (U + P) = \delta ^l_{Q,U,P}( (1_Q \rtimes U) + (1_Q \rtimes P) )(\delta ^l_{Q,U,P})^{-1} \\&\quad = \delta ^l_{Q,U,P}(1_{QU} + 1_{QP})(\delta ^l_{Q,U,P})^{-1} = 1_{Q(U+P)} \end{align*}
-
(x) By induction on
$R$
. The base case is
$\sigma ^+_{P,Q} \rtimes 0 = 1_0 = \sigma ^+_{0,0} = \sigma ^+_{P0,Q0}$
. For the inductive case, suppose
$\sigma ^+_{P,Q} \rtimes R = \sigma ^+_{PR,QR}$
. Then using Lemma B.3, we have:and the claim follows.
\begin{align*} & \sigma ^+_{P,Q} \rtimes (W + R) = \delta ^l_{P+Q,W,R}((\sigma ^+_{P,Q} \rtimes W) + (\sigma ^+_{P,Q} \rtimes R))(\delta ^l_{Q+P,W,R})^{-1} \\&\quad = (\delta ^l_{P,W,R} + \delta ^l_{Q,W,R})(1_{PW} + \sigma ^+_{PR,QW} + 1_{QR})(\sigma ^+_{PW,QW} + \sigma ^+_{PR,QR})\\&\quad \hspace {0.5cm}(1_{QW} + \sigma ^+_{PW,QR} + 1_{PW})((\delta ^l_{Q,W,R})^{-1} + (\delta ^l_{P,W,R})^{-1}) \\&\quad = (\delta ^l_{P,W,R} + \delta ^l_{Q,W,R})\sigma ^+_{PW+PR,QW+QR}((\delta ^l_{Q,W,R})^{-1} + (\delta ^l_{P,W,R})^{-1}) \\&\quad = \sigma ^+_{P(W+R),Q(W+R)} \end{align*}
-
(xi) By induction on
$P$
. The base case is
$\eta _Q \rtimes 0 = 1_0 = \eta _0 = \eta _{Q0}$
. For the inductive case, suppose
$\eta _Q \rtimes P = \eta _{QP}$
. Then using Lemma B.3, we have:and the claim follows.
\begin{align*} & \eta _Q \rtimes (U+P) = \delta ^l_{0,U,P}((\eta _Q \rtimes U) + (\eta _Q \rtimes P))(\delta ^l_{Q,U,P})^{-1} \\&\quad = 1_0(\eta _{QU} + \eta _{QP})(\delta ^l_{Q,U,P})^{-1} = \eta _{QU + QP}(\delta ^l_{Q,U,P})^{-1} = \eta _{Q(U+P)} \end{align*}
-
(xii) By induction on
$P$
. The base case is
$\mu _Q \rtimes 0 = 1_0 = \mu _0 = \mu _{Q0}$
. For the inductive case, suppose
$\mu _Q \rtimes P = \mu _{QP}$
. Then using Lemma B.3, we have:and the claim follows.
\begin{align*} & \mu _Q \rtimes (U+P) = \delta ^l_{Q+Q,U,P}((\mu _Q \rtimes U) + (\mu _Q \rtimes P))(\delta ^l_{Q,U,P})^{-1} \\[2pt]&\quad = (\delta ^l_{Q,U,P} + \delta ^l_{Q,U,P})(1_{QU} + \sigma ^+_{QP,QU} + 1_{QP})(\mu _{QU} + \mu _{QP})(\delta ^l_{Q,U,P})^{-1} \\[2pt]&\quad = (\delta ^l_{Q,U,P} + \delta ^l_{Q,U,P})\mu _{QU+QP}(\delta ^l_{Q,U,P})^{-1} = \mu _{Q(U+P)}\delta ^l_{Q,U,P}(\delta ^l_{Q,U,P})^{-1} = \mu _{Q(U+P)} \end{align*}
-
(xiii) By induction on
$P$
. The base is
$\mathsf{Tr}^Q_{R,S}(f) \rtimes 0 = 1_0 \mathsf{Tr}^0_{0,0}(1_0) = \mathsf{Tr}^{Q0}_{R0,S0}(f \rtimes 0)$
. For the inductive case, suppose
$\mathsf{Tr}^Q_{R,S}(f) \rtimes P = \mathsf{Tr}^{QP}_{RP,SP}(f \rtimes P)$
. Then using Lemma B.3, we have:where the marked equation (
\begin{align*} & \mathsf{Tr}^Q_{R,S}(f) \rtimes (U + P) = \delta ^l_{R,U,P}((\mathsf{Tr}^Q_{R,S}(f) \rtimes U) + (\mathsf{Tr}^Q_{R,S}(f) \rtimes P))(\delta ^l_{S,U,P})^{-1} \\[2pt]&\quad = \delta ^l_{R,U,P}(\mathsf{Tr}^{QU}_{RU,SU}(f \rtimes U) + \mathsf{Tr}^{QP}_{RP,SP}(f \rtimes P))(\delta ^l_{S,U,P})^{-1} \\[2pt]&\quad \stackrel {*}{=} \mathsf{Tr}^{Q(U+P)}_{R(U+P),S(U+P)}( (\delta ^l_{R,U,P} + \delta ^l_{Q,U,P})(1_{RU} + \sigma ^+_{RP,QU} + 1_{QP})((f \rtimes U) + (f \rtimes P))\\[2pt]&\quad \hspace {0.5cm}(1_{SU} + \sigma ^+_{QU,SP} + 1_{QP})( (\delta ^l_{S,U,P})^{-1} + (\delta ^l_{Q,U,P})^{-1} )) \\[2pt]&\quad = \mathsf{Tr}^{Q(U+P)}_{R(U+P),S(U+P)}(\delta ^l_{R+Q,U,P}((f \rtimes U) + (f \rtimes P))(\delta ^l_{S+Q,U,P})^{-1}) \\[2pt]&\quad = \mathsf{Tr}^{Q(U+P)}_{R(U+P),S(U+P)}(f \rtimes (U+P)) \end{align*}
$\stackrel {*}{=}$
) holds as in:The claim follows. -
(xvi) By induction on
$P$
. The base case is
$1_0 \rtimes 0 = 1_0$
. For the inductive case, suppose
$1_0 \rtimes P = 1_0$
. Then we have:and the claim follows.
\begin{align*} & 1_0 \rtimes (U+P) = \delta ^l_{0,U,P}((1_0 \rtimes U) + (1_0 \rtimes P))(\delta ^l_{0,U,P})^{-1} = 1_0(1_0 + 1_0)1_0 = 1_0 \end{align*}
-
(xv) By induction on
$P$
. The base case is
$ts \rtimes 0 = 1_0 = 1_01_0 = (t \rtimes 0)(s \rtimes 0)$
. For the inductive case, suppose
$ts \rtimes P = (t \rtimes P)(s \rtimes P)$
. Then we have:where
\begin{align*} & ts \rtimes (U+P) = \delta ^l_{R,U,P}((ts \rtimes U) + (ts \rtimes P))(\delta ^l_{T,U,P})^{-1} \\[2pt]&\quad = \delta ^l_{R,U,P}((t \rtimes U)(s \rtimes U) + (t \rtimes P)(s \rtimes P))(\delta ^l_{T,U,P})^{-1} \\[2pt]&\quad = \delta ^l_{R,U,P}((t \rtimes U) + (t \rtimes P))(\delta ^l_{S,U,P})^{-1}\delta ^l_{S,U,P}((s \rtimes U) + (s \rtimes P))(\delta ^l_{T,U,P})^{-1} \\[2pt]&\quad = (t \rtimes (U+P))(s \rtimes (U+P)) \end{align*}
$t : R \to S$
and
$s : S \to T$
. The claim follows.
-
(xvi) By induction on
$P$
. The base case is
$(t + s) \rtimes 0 = 1_0 = 1_0 + 1_0 = (t \rtimes 0) + (s \rtimes 0)$
. For the inductive case, suppose
$(t + s) \rtimes P = (t \rtimes P) + (s \rtimes P)$
. Then we have:and the claim follows.
\begin{align*} & (t + s) \rtimes (U + P) = \delta ^l_{P_1 + P_2,U,P}(((t + s) \rtimes U) + ((t + s) \rtimes P))(\delta ^l_{Q_1 + Q_2,U,P})^{-1} \\&\quad = (\delta ^l_{P_1,U,P} + \delta ^l_{P_2,U,P})(1_{P_1U} + \sigma ^+_{P_1P,P_2U} + 1_{P_2P})((t \rtimes U) + (s \rtimes Y) + (t \rtimes P) + (s \rtimes P))\\&\quad \hspace {0.5cm}(1_{Q_1U} + \sigma ^+_{Q_2U,Q_1P} + 1_{Q_2P})((\delta ^l_{Q_1,U,P})^{-1} + (\delta ^l_{Q_2,U,P})^{-1}) \\&\quad = \delta ^l_{P_1,U,P}((t \rtimes U) + (t \rtimes P))(\delta ^l_{Q_1,U,P})^{-1} + \delta ^l_{P_2,U,P}((s \rtimes U) + (s \rtimes P))(\delta ^l_{Q_2,U,P})^{-1} \\&\quad = (t \rtimes (U+P)) + (s \rtimes (U + P)) \end{align*}
Next, we show that the distributors behave as they ought to:
Lemma B.5. We have:
-
(i)
$\delta ^l_{0,P,Q} = 1_0$
-
(ii)
$\delta ^l_{P,0,Q} = 1_{PQ}$
-
(iii)
$\delta ^l_{P,Q,0} = 1_{PQ}$
-
(iv)
$\delta ^l_{I,P,Q} = 1_{P + Q}$
-
(v)
$\delta ^l_{P+Q,R,S} = (\delta ^l_{P,R,S} + \delta ^l_{Q,R,S})(1_{PR} + \sigma ^+_{PS,QR} + 1_{QS})$
-
(vi)
$\delta ^l_{P,Q+R,S}(\delta ^l_{P,Q,R} + 1_{PS}) = \delta ^l_{P,Q,R+S}(1_{PQ} + \delta ^l_{P,R,S})$
-
(vii)
$\delta ^l_{PQ,R,S} = (P \ltimes \delta ^l_{Q,R,S})\delta ^l_{P,QR,QS}$
-
(viii)
$\delta ^l_{P,QS,RS} = \delta ^l_{P,Q,R} \rtimes S$
-
(xi)
$\delta ^l_{P,Q,R}((P \ltimes f) + (P \ltimes g)) = (P \ltimes f + g)\delta ^l_{P,Q',R'}$
for
$f : Q \to Q', g : R \to R'$
Proof.
-
(i) Immediate.
-
(ii) By induction on
$P$
. The base case is
$\delta ^l_{0,0,Q} = 1_0 = 1_{0Q}$
. For the inductive case, suppose
$\delta ^l_{P,0,Q} = 1_{PQ}$
. Then we have:and the claim follows.
\begin{align*} &\delta ^l_{U + P,0,Q} = (1_{U0 + UQ} + \delta ^l_{P,0,Q})(1_{U0} + \sigma ^+_{UQ,P0} + 1_{PQ}) \\&\quad = (1_{UQ} + 1_{PQ})(1_{UQ} + 1_{PQ}) = 1_{UQ + PQ} = 1_{(U + P)Q} \end{align*}
-
(iii) By induction on
$P$
. The base case is
$\delta ^l_{0,Q,0} = 1_0 = 1_{0Q}$
. For the inductive case, suppose
$\delta ^l_{P,Q,0} = 1_{PQ}$
. Then we have:and the claim follows.
\begin{align*} & \delta ^l_{U+P,Q,0} = (1_{UQ + U0} + \delta ^l_{P,Q,0})(1_{UQ} + \sigma ^+_{U0,PQ} + 1_{P0}) \\ &\quad = (1_{UQ} + 1_{PQ})(1_{UQ} + 1_{PQ}) = 1_{UQ + PQ} = 1_{(U+P)Q} \end{align*}
-
(iv)
$I$
is a monomial so we have
$\delta ^l_{I,P,Q} = 1_{IP + IQ} = 1_{P + Q}$
as required. -
(v) By induction on
$P$
. The base cases is
$\delta ^l_{0+Q,R,S} = \delta ^l_{Q,R,S} = (1_0 + \delta ^l_{Q,R,S})(1_0 + \sigma ^+_{0,QR} + 1_{QS}) = (\delta ^l_{0,R,S} + \delta ^l_{Q,R,S})(1_{0R} + \sigma ^+_{0S,QR} + 1_{QS})$
. For the inductive case, suppose
$\delta ^l_{P+Q,R,S} = $
$(\delta ^l_{P,R,S} + \delta ^l_{Q,R,S})(1_{PR} + \sigma ^+_{PS,QR} + 1_{QS})$
. Then we have:and the claim follows.
\begin{align*} & \delta ^l_{(U+P)+Q,R,S} = \delta ^l_{U+(P+Q),R,S} = (1_{UR+US} + \delta ^l_{P+Q,R,S})(1_{UR} + \sigma ^+_{US,PR+QR} + 1_{PS+QS}) \\&\quad = (1_{UR+US} + (\delta ^l_{P,R,S} + \delta ^l_{Q,R,S})(1_{PR} + \sigma ^+_{PS,QR} + 1_{QS}))(1_{UR} + \sigma ^+_{US,PR+QR} + 1_{PS+QS}) \\&\quad = (1_{UR+US} + \delta ^l_{P,R,S} + \delta ^l_{Q,R,S})(1_{UR} + \sigma ^+_{US,PR} + \sigma ^+_{PS,QR} + 1_{QS})(1_{UR+PR} + \sigma ^+_{US,QR} + 1_{PS+QS}) \\&\quad = ((1_{UR+US} + \delta ^l_{P,R,S})(1_{UR} + \sigma ^+_{US,PR} + 1_{PS}) + \delta ^l_{Q,R,S})(1_{UR+PR} + \sigma ^+_{US+PS,QR} + 1_{QS}) \\&\quad = (\delta ^l_{U+P,R,S} + \delta ^l_{Q,R,S})(1_{(U+P)R}+ \sigma ^+_{(U+P)S,QR} + 1_{QS}) \end{align*}
-
(vi) By induction on
$P$
. The base case is
$\delta ^l_{0,Q+R,S}(\delta ^l_{0,Q,R} + 1_{0S}) = 1_0 = \delta ^l_{0,Q,R+S}(1_{0Q} + \delta ^l_{0,R,S})$
. For the inductive case, suppose
$\delta ^l_{P,Q+R,S}(\delta ^l_{P,Q,R} + 1_{PS}) = \delta ^l_{P,Q,R+S}(1_{PQ} + \delta ^l_{P,R,S})$
. Then we have:
\begin{align*} & \delta ^l_{U+P,Q+R,S}(\delta ^l_{U+P,Q,R} + 1_{U+P}S) \\&\quad = (1_{UQ+UR+US} + \delta ^l_{P,Q+R,S})(1_{UQ+UR} + \sigma ^+_{US,P(Q+R)} + 1_{PS}) \\&\quad \hspace {0.5cm}(1_{UQ+UR} + \delta ^l_{P,Q,R} + 1_{US+PS})(1_{UQ} + \sigma ^+_{UR,PQ} + 1_{PR+US+PS}) \\&\quad = (1_{UQ+UR+US}+\delta ^l_{P,Q+R,S})(1_{UQ+UR+US}+\delta ^l_{P,Q,R}+1_{PS}) \\&\quad \hspace {0.5cm}(1_{UQ+UR} + \sigma ^+_{US,PQ+PR} + 1_{PS})(1_{UQ} + \sigma ^+_{UR,PQ} + 1_{PR+US+PS}) \\&\quad = (1_{UQ+UR+US} + \delta ^l_{P,Q+R,S}(\delta ^l_{P,Q,R} + 1_{PS}))(1_{UQ+UR} + \sigma ^+_{US,PQ} + 1_{PR,PS}) \\&\quad \hspace {0.5cm}(1_{UQ} + \sigma ^+_{UR,PQ} + \sigma ^+_{US,PR} + 1_{PS}) \\&\quad = (1_{UQ+UR+US} + \delta ^l_{P,Q,R+S}(1_{PQ} + \delta ^l_{P,R,S}))(1_{UQ+UR} + \sigma ^+_{US,PQ} + 1_{PR,PS}) \\&\quad \hspace {0.5cm}(1_{UQ} + \sigma ^+_{UR,PQ} + \sigma ^+_{US,PR} + 1_{PS}) \\&\quad = (1_{UQ+UR+US} + \delta ^l_{P,Q,R+S})(1_{UQ} + \sigma ^+_{UR+US,PQ} + 1_{P(R+S)}) \\&\quad \hspace {0.5cm}(1_{UQ+PQ+UR+US} + \delta ^l_{P,R,S})(1_{UQ+PQ+UR} + \sigma ^+_{US,PR} + 1_{PS}) \\&\quad = \delta ^l_{U+P,Q,R+S}(1_{(U+P)Q} + \delta ^l_{U+P,R,S}) \end{align*}
-
(vii) First, we show that for all monomials
$U$
we have
$\delta ^l_{UQ,R,S} = U \ltimes \delta ^l_{Q,R,S}$
. We do this by induction on
$Q$
. For the base case, we have
$\delta ^l_{U0,R,S} = 1_0 = U \ltimes 1_0 = U \ltimes \delta ^l_{0,R,S}$
. For the inductive case, suppose
$\delta ^l_{UQ,R,S} = U \ltimes \delta ^l_{Q,R,S}$
. Then we have:as required. We proceed to prove the main claim by induction on
\begin{align*} & \delta ^l_{U(V+Q),R,S} = \delta ^l_{UV+UQ,R,S} = (1_{UVR + UVS} + \delta ^l_{UQ,R,S})(1_{UVR} + \sigma ^+_{UVS,UQR} + 1_{UQS}) \\&\quad = ((U \ltimes 1_{VR+VS}) + (U \ltimes \delta ^l_{Q,R,S}))(U \ltimes (1_{VR} + \sigma ^+_{VS,QR} + 1_{RS})) = U \ltimes \delta ^l_{V+Q,R,S} \end{align*}
$P$
. The base case is
$\delta ^l_{0Q,R,S} = 1_0 = (0 \ltimes \delta ^l_{Q,R,S})\delta ^l_{0,QR,QS}$
. For the inductive case, suppose
$\delta ^l_{PQ,R,S} = (P \ltimes \delta ^l_{Q,R,S})\delta ^l_{P,QR,QS}$
. Then we have:and the claim follows.
\begin{align*} & ((U+P) \ltimes \delta ^l_{Q,R,S})\delta ^l_{U+P,QR,QS} \\&\quad = ((U \ltimes \delta ^l_{Q,R,S}) + (P \ltimes \delta ^l_{Q,R,S}))(1_{UQR+UQS} + \delta ^l_{P,QR,QS})(1_{UQR} + \sigma ^+_{UQS,PQR} + 1_{PQS}) \\&\quad = (\delta ^l_{UQ,R,S} + \delta ^l_{PQ,R,S})(1_{UQR} + \sigma ^+_{UQS,PQR} + 1_{PQS}) = \delta ^l_{UQ+PQ,R,S} = \delta ^l_{(U+P)Q,R,S} \end{align*}
-
(viii) By induction on
$P$
. The base case is
$\delta ^l_{0,QS,RS} = 1_0 = 1_0\rtimes S = \delta ^l_{0,P,Q} \rtimes S$
For the inductive case, suppose
$\delta _{P,Q,R} \rtimes S = \delta _{P,QS,RS}$
. Then we have:and the claim follows.
\begin{align*} & \delta ^l_{U+P,QS,RS} = (1_{UQS + URS} + \delta ^l_{P,QS,RS})(1_{UQS} + \sigma ^+_{URS,PQS} + 1_{PRS}) \\&\quad = (1_{UQS+URS} + (\delta ^l_{P,Q,R} \rtimes S))(1_{UQS} + (\sigma ^+_{UR,PQ} \rtimes S) + 1_{PRS}) \\&\quad = (1_{UQ+UR} + \delta ^l_{P,Q,R})(1_{UQ} + \sigma ^+_{UR,PQ} + 1_{PR}) \rtimes S = \delta ^l_{U+P,Q,R} \rtimes S \end{align*}
-
(xi) By induction on
$P$
. For the base case, we have
$\delta ^l_{0,Q,R}((0 \ltimes f) + (0 \ltimes g)) = 1_0 = (0 \ltimes f + g)\delta ^l_{P,Q',R'}$
. For the inductive case, suppose
$\delta ^l_{P,Q,R}((P \ltimes f) + (P \ltimes g)) = (P \ltimes f + g)\delta ^l_{P,Q',R'}$
. Then we have:and the claim follows.
\begin{align*} & \delta ^l_{U+P,Q,R}( ((U+P) \ltimes f) + ((U + P) \ltimes g) ) \\[3pt]&\quad = (\delta ^l_{U,Q,R} + \delta ^l_{P,Q,R})(1_{UQ} + \sigma ^+_{UR,PQ} + 1_{PR})((U \ltimes f) + (P \ltimes f) + (U \ltimes g) + (P \ltimes g)) \\[3pt]&\quad = (\delta ^l_{U,Q,R} + \delta ^l_{P,Q,R})((U \ltimes f) + (U \ltimes g) + (P \ltimes f) + (P \ltimes g))(1_{UQ'} + \sigma ^+_{UR',PQ'} + 1_{PR'}) \\[3pt]&\quad = (\delta ^l_{U,Q,R}((U \ltimes f) + (U \ltimes g)) + \delta ^l_{P,Q,R}((P \ltimes f) + (P \ltimes g)))(1_{UQ'} + \sigma ^+_{UR',PQ'} + 1_{PR'}) \\[3pt]&\quad = ((U \ltimes f + g)\delta ^l_{U,Q',R'} + (P \ltimes f + g)\delta ^l_{P,Q',R'})(1_{UQ'} + \sigma ^+_{UR',PQ'} + 1_{PR'}) \\[3pt]&\quad = ((U \ltimes f + g) + (P \ltimes f + g))\delta ^l_{U+P,Q,R} = ((U + P) \ltimes f + g)\delta ^l_{U+P,Q,R} \end{align*}
We establish a few more properties of the whiskering functors:
Lemma B.6.
For any morphism
$f : R \to S$
of
$\mathbb{A}$
and any monomials
$U,V$
, we have:
-
(i)
$UV \ltimes f = U \ltimes (V \ltimes f)$
-
(ii)
$f \rtimes UV = (f \rtimes U) \rtimes V$
-
(iii)
$(U \ltimes f) \rtimes V = U \ltimes (f \rtimes V)$
Proof.
Straightforward, by induction on
$f$
.
Lemma B.7.
For any morphism
$f : R \to S$
of
$\mathbb{A}$
and any polynomials
$P,Q$
, we have:
-
(i)
$I \ltimes f = f$
-
(ii)
$f \rtimes I = f$
-
(iii)
$PQ \ltimes f = P \ltimes (Q \ltimes f)$
-
(iv)
$f \rtimes PQ = (f \rtimes P) \rtimes Q$
-
(v)
$(P \ltimes f) \rtimes Q = P \ltimes (f \rtimes Q)$
Proof.
-
(i) By induction on
$f$
. We use in particular that
$I$
is monomial. The base cases are as follows:-
• (
$\mathsf{succ}$
): If
$f$
is
$\mathsf{succ}_{U,V}$
then we have
$I \ltimes \mathsf{succ}_{U,V} = \mathsf{succ}_{IU,V} = \mathsf{succ}_{U,V}$
. -
• (
$\mathsf{zero}$
): If
$f$
is
$\mathsf{zero}_{U,V}$
then we have
$I \ltimes \mathsf{zero}_{U,V} = \mathsf{zero}_{IU,V} = \mathsf{zero}_{U,V}$
. -
• (
$\mathsf{pred}$
): If
$f$
is
$\mathsf{pred}_{U,V}$
then we have
$I \ltimes \mathsf{pred}_{U,V} = \mathsf{pred}_{IU,V} = \mathsf{pred}_{U,V}$
. -
• (
$1$
): If
$f$
is
$1_U$
then we have
$I \ltimes 1_U = 1_{IU} = 1_{U}$
. -
• (
$\eta$
): If
$f$
is
$\eta _U$
then we have
$I \ltimes \eta _U = \eta _{IU} = \eta _{U}$
. -
• (
$\mu$
): If
$f$
is
$\mu _U$
then we have
$I \ltimes \mu _U = \mu _{IU} = \mu _U$
. -
• (
$0$
): If
$f$
is
$1_0$
then we have
$I \ltimes 1_0 = 1_0$
. -
• (
$\sigma$
): If
$f$
is
$\sigma ^+_{U,V}$
then we have
$I \ltimes \sigma ^+_{U,V} = \sigma ^+_{IU,IV} = \sigma ^+_{U,V}$
.
For the inductive cases, suppose
$I \ltimes f = f$
and
$I \ltimes g = g$
. Then we have:-
• (
$\circ$
):
$I \ltimes fg = (I \ltimes f)(I \ltimes g) = fg$
-
• (
$+$
):
$I \ltimes (f+g) = (I \ltimes f) + (I \ltimes g) = f + g$
-
• (
$\mathsf{Tr}$
):
$I \ltimes \mathsf{Tr}^W_{P,Q}(f) = \mathsf{Tr}^{IW}_{IP,IQ}(I \ltimes f) = \mathsf{Tr}^{W}_{P,Q}(f)$
The claim follows.
-
-
(ii) Similar to (i).
-
(iii) We begin by showing that for any monomial
$U$
we have
$U \ltimes (Q \ltimes f) = UQ \ltimes f$
, which we do by induction on
$Q$
. The base case is
$U \ltimes (0 \ltimes f) = 1_0 = U0 \ltimes f$
. For the inductive case suppose
$U \ltimes (Q \ltimes f) = UQ \ltimes f$
. Then we have:as required. We are now ready to prove the primary claim, which we do by induction on
\begin{align*} & U \ltimes ((V + Q) \ltimes f) = U \ltimes ((V \ltimes f) + (Q \ltimes f)) = (U \ltimes (V \ltimes f)) + (U \ltimes (Q \ltimes f)) \\&\quad = (UV \ltimes f) + (UQ \ltimes f) = (UV + UQ)\ltimes f = U(V+Q) \ltimes f \end{align*}
$P$
. The base case is
$0 \ltimes (Q \ltimes f) = 1_0 = 0Q \ltimes f$
. For the inductive case suppose
$P \ltimes (Q \ltimes f) = PQ \ltimes f$
. Then we have:The claim follows.
\begin{align*} & (U+P) \ltimes (Q \ltimes f) = (U \ltimes (Q \ltimes f)) + (P \ltimes (Q \ltimes f)) = (UQ \ltimes f) + (UP \ltimes f) \\&\quad = (UQ + PQ) \ltimes f = (U+P)Q \ltimes f \end{align*}
-
(iv) We begin by showing that for any monomial
$U$
, we have
$(f \rtimes U) \rtimes Q = f \rtimes UQ$
, which we do by induction on
$Q$
. The base case is
$(f \rtimes U) \rtimes 0 = 1_0 = f \rtimes U0$
. For the inductive case suppose
$(f \rtimes U) \rtimes Q = f \rtimes UQ$
. Then we have:as required. We are now ready to prove the primary claim, which we do by induction on
\begin{align*} & (f \rtimes U) \rtimes (V+Q) = \delta ^l_{RU,V,Q}(((f \rtimes U) \rtimes V) + ((f \rtimes U) \rtimes Q))(\delta ^l_{SU,V,Q})^{-1} \\&\quad = (R \ltimes \delta ^l_{U,V,Q})\delta ^l_{R,UV,UQ}((f \rtimes UV) + (f \rtimes UQ))(\delta ^l_{S,UV,UQ})^{-1}(S \ltimes (\delta ^l_{U,V,Q})^{-1}) \\&\quad = (R \ltimes 1_{UV+UQ})(f \rtimes (UV+UQ))(S \ltimes 1_{UV+UQ}) = f \rtimes U(V+Q) \end{align*}
$P$
. The base case is
$(f \rtimes 0) \rtimes Q = 1_0 = f \rtimes 0Q$
. For the inductive case suppose
$(f \rtimes P) \rtimes Q = f \rtimes PQ$
. Then we have:The claim follows.
\begin{align*} & (f \rtimes (U+P)) \rtimes Q = (\delta ^l_{R,U,P}((f \rtimes U) + (f \rtimes P))(\delta ^l_{S,U,P})^{-1}) \rtimes Q \\&\quad = (\delta ^l_{R,U,P} \rtimes Q)(((f \rtimes U) \rtimes Q) + ((f \rtimes P) \rtimes Q))((\delta ^l_{S,U,P})^{-1} \rtimes Q) \\&\quad = \delta ^l_{R,UQ,PQ}((f \rtimes UQ) + (f \rtimes PQ))(\delta ^l_{S,UQ,PQ})^{-1} \\&= f \rtimes (UQ + PQ) = f \rtimes (U+P)Q \end{align*}
-
(v) We begin by showing that for any monomial
$V$
,
$(P \ltimes f) \rtimes V = P \ltimes (f \rtimes V)$
, which we do by induction on
$P$
. The base case is
$(0 \ltimes f) \rtimes V = 1_0 = 0 \ltimes (f \rtimes V)$
. For the inductive case suppose
$(P \ltimes f) \rtimes V = P \ltimes (f \rtimes V)$
. Then we have:as required. We are now ready to prove the primary claim, which we do by induction on
\begin{align*} & ((U+P) \ltimes f) \rtimes V = ((U \ltimes f) + (P \ltimes f)) \rtimes V = ((U \ltimes f) \rtimes V) + ((P \ltimes f) \rtimes V) \\&\quad = (U \ltimes (f \rtimes V)) + (P \ltimes (f \rtimes V)) = (U+P) \ltimes (f \rtimes V) \end{align*}
$Q$
. The base case is
$(P \ltimes f) \rtimes 0 = 1_0 = P \ltimes (f \rtimes 0)$
. For the inductive case suppose
$(P \ltimes f) \rtimes Q = P \ltimes (f \rtimes Q)$
. Then we have:The claim follows.
\begin{align*} & (P \ltimes f) \rtimes (V+Q) = \delta ^l_{PR,V,Q}(((P \ltimes f) \rtimes V) + ((P \ltimes f) \rtimes Q))(\delta ^l_{PS,V,Q})^{-1} \\&\quad = \delta ^l_{PR,V,Q}((P \ltimes + (f \rtimes V)) + (P \ltimes (f \rtimes Q)))(\delta ^l_{PS,V,Q})^{-1} \\&\quad = \delta ^l_{PR,V,Q}(\delta ^l_{P,RV,RQ})^{-1}(P \ltimes ((f \rtimes V) + (f \rtimes Q)))\delta ^l_{P,SV,SQ}(\delta ^l_{PS,V,Q})^{-1} \\&\quad = (P \ltimes \delta ^l_{R,V,Q})(P \ltimes ((f \rtimes V) + (f \rtimes Q)))(P \ltimes (\delta ^l_{S,V,Q})^{-1}) \\&\quad = P \ltimes (\delta ^l_{R,V,Q}((f \rtimes V) + (f \rtimes Q))(\delta ^l_{S,V,Q})^{-1}) \\&\quad = P \ltimes (f \rtimes (V+Q)) \end{align*}
At long last, we are able to show that left and right whiskering interchange in the necessary manner:
Lemma B.8.
For all
$f : P \to Q$
and
$g : R \to S$
of
$\mathbb{A}$
,
$(f \rtimes R)(Q \ltimes g) = (P \ltimes g)(f \rtimes S)$
.
Proof.
By induction on
$f$
and
$g$
. The base cases are split into two groups. First, in case both
$f$
and
$g$
are instances of
$\mathsf{succ}$
,
$\mathsf{zero}$
, or
$\mathsf{pred}$
we have:
-
• (
$\mathsf{succ}$
-
$\mathsf{succ}$
): If
$f$
is
$\mathsf{succ}_{U,V} : UNV \to UNV$
and
$g$
is
$\mathsf{succ}_{U',V'} : U'NV' \to U'NV'$
then [N3] gives:as required.
\begin{align*} & (\mathsf{succ}_{U,V} \rtimes U'NV')(UNV \ltimes \mathsf{succ}_{U',V'}) = \mathsf{succ}_{U,VU'NV'}\mathsf{succ}_{UNVU',V'} \\&\quad = \mathsf{succ}_{UNVU',V'}\mathsf{succ}_{U,VU'NV'} = (UNV \ltimes \mathsf{succ}_{U',V'})(\mathsf{succ}_{U,V} \rtimes U'NV') \end{align*}
-
• (
$\mathsf{succ}$
-
$\mathsf{zero}$
): If
$f$
is
$\mathsf{succ}_{U,V} : UNV \to UNV$
and
$g$
is
$\mathsf{zero}_{U',V'} : U'V' \to U'NV'$
then [N4] gives:
\begin{align*} & (\mathsf{succ}_{U,V} \rtimes U'V')(UNV \ltimes \mathsf{zero}_{U',V'}) = \mathsf{succ}_{U,VU'V'}\mathsf{zero}_{UNVU',V'} \\&\quad = \mathsf{zero}_{UNVU',V'}\mathsf{succ}_{U,VU'NV'} = (UNV \ltimes \mathsf{zero}_{U',V'})(\mathsf{succ}_{U,V} \rtimes U'V') \end{align*}
-
• (
$\mathsf{zero}$
-
$\mathsf{succ}$
): If
$f$
is
$\mathsf{zero}_{U,V} : UV \to UNV$
and
$g$
is
$\mathsf{succ}_{U',V'} : U'NV' \to U'NV'$
then [N5] gives:as required.
\begin{align*} & (\mathsf{zero}_{U,V} \rtimes U'NV')(UNV \ltimes \mathsf{succ}_{U',V'}) = \mathsf{zero}_{U,VU'NV'}\mathsf{succ}_{UNVU',V'} \\&\quad = \mathsf{succ}_{UVU',V'}\mathsf{zero}_{U,VU'NV'} = (UV \ltimes \mathsf{succ}_{U',V'})(\mathsf{zero}_{U,V} \rtimes U'NV') \end{align*}
-
• (
$\mathsf{zero}$
-
$\mathsf{zero}$
): If
$f$
is
$\mathsf{zero}_{U,V} : UV \to UNV$
and
$g$
is
$\mathsf{zero}_{U',V'} : U'V' \to U'NV'$
then [N6] gives:
\begin{align*} & (\mathsf{zero}_{U,V} \rtimes U'V')(UNV \ltimes \mathsf{zero}_{U',V'}) = \mathsf{zero}_{U,VU'V'}\mathsf{zero}_{UNVU',V'} \\&\quad = \mathsf{zero}_{UVU',V'}\mathsf{zero}_{U,VU'NV'} = (UV \ltimes \mathsf{zero}_{U',V'})(\mathsf{zero}_{U,V} \rtimes U'NV') \end{align*}
-
• (
$\mathsf{succ}$
-
$\mathsf{pred}$
): If
$f$
is
$\mathsf{succ}_{U,V} : UNV \to UNV$
and
$g$
is
$\mathsf{pred}_{U',V'} : U'NV' \to U'V' + U'NV'$
then [N7] gives:as required.
\begin{align*} & (\mathsf{succ}_{U,V} \rtimes U'NV')(UNV \ltimes \mathsf{pred}_{U',V'}) = \mathsf{succ}_{U,VU'NV'}\mathsf{pred}_{UNVU',V'} \\&\quad = \mathsf{pred}_{UNVU',V'}(\mathsf{succ}_{U,VU'V'} + \mathsf{succ}_{U,VU'NV'}) \\&\quad = (UNV \ltimes \mathsf{pred}_{U',V'})((\mathsf{succ}_{U,V} \rtimes U'V') + (\mathsf{succ}_{U,V} \rtimes U'NV')) \\&\quad = (UNV \ltimes \mathsf{pred}_{U',V'})(\mathsf{succ}_{U,V} \rtimes U'V' + U'NV') \end{align*}
-
• (
$\mathsf{zero}$
-
$\mathsf{pred}$
): If
$f$
is
$\mathsf{zero}_{U,V} : UV \to UNV$
and
$g$
is
$\mathsf{pred}_{U',V'} : U'NV' \to U'V' + U'NV'$
then [N8] gives:as required.
\begin{align*} & (\mathsf{zero}_{U,V} \rtimes U'NV')(UNV \ltimes \mathsf{pred}_{U',V'}) = \mathsf{zero}_{U,VU'NV'}\mathsf{pred}_{UNVU',V'} \\&\quad = \mathsf{pred}_{UVU',V'}(\mathsf{zero}_{U,VU'V'} + \mathsf{zero}_{U,VU'NV'}) \\&\quad = (UV \ltimes \mathsf{pred}_{U',V'})( (\mathsf{zero}_{U,V} \rtimes U'V') + (\mathsf{zero}_{U,V} \rtimes U'NV')) \\&\quad = (UV \ltimes \mathsf{pred}_{U',V'})(\mathsf{zero}_{U,V} \rtimes U'V' + U'NV') \end{align*}
-
• (
$\mathsf{pred}$
-
$\mathsf{succ}$
): If
$f$
is
$\mathsf{pred}_{U,V} : UNV \to UV + UNV$
and
$g$
is
$\mathsf{succ}_{U',V'} : U'NV' \to U'NV'$
then
$\textbf {[N9]}$
gives:as required.
\begin{align*} & (\mathsf{pred}_{U,V} \rtimes U'NV')((UV + UNV) \ltimes \mathsf{succ}_{U',V'}) \\&\quad = (\mathsf{pred}_{U,V} \rtimes U'NV')((UV \ltimes \mathsf{succ}_{U',V'}) + (UNV + \ltimes \mathsf{succ}_{U',V'})) \\&\quad = \mathsf{pred}_{U,VU'NV'}(\mathsf{succ}_{UVU',V'} + \mathsf{succ}_{UNVU',V'}) = \mathsf{succ}_{UNVU',V'}\mathsf{pred}_{U,VU'NV'} \\&\quad = (UNV \ltimes \mathsf{succ}_{U',V'})(\mathsf{pred}_{U,V} \rtimes U'NV') \end{align*}
-
• (
$\mathsf{pred}$
-
$\mathsf{zero}$
): If
$f$
is
$\mathsf{pred}_{U,V} : UNV \to UV + UNV$
and
$g$
is
$\mathsf{zero}_{U',V'} : U'V' \to U'NV'$
then
$\textbf {[N10]}$
gives:as required.
\begin{align*} & (\mathsf{pred}_{U,V} \rtimes U'V')((UV + UNV) \ltimes \mathsf{zero}_{U',V'}) = \mathsf{pred}_{U,VU'V'}(\mathsf{zero}_{UVU',V'} + \mathsf{zero}_{UNVU',V'}) \\&\quad = \mathsf{zero}_{UNVU',V'}\mathsf{pred}_{U,VU'NV'} = (UNV \ltimes \mathsf{zero}_{U',V'})(\mathsf{pred}_{U,V} \rtimes U'NV') \end{align*}
-
• (
$\mathsf{pred}$
-
$\mathsf{pred}$
): If
$f$
is
$\mathsf{pred}_{U,V} : UNV \to UV + UNV$
and
$g$
is
$p_{U',V'} : U'NV' \to U'V' + U'NV'$
then
$\textbf {[N11]}$
gives:as required.
\begin{align*} & (\mathsf{pred}_{U,V} \rtimes U'NV')((UV + UNV) \ltimes \mathsf{pred}_{U',V'}) \\&\quad = \mathsf{pred}_{U,VU'NV'}((UV \ltimes \mathsf{pred}_{U',V'}) + (UNV \ltimes \mathsf{pred}_{U',V'})) \\&\quad = \mathsf{pred}_{U,VU'NV'}(\mathsf{pred}_{UVU',V'} + \mathsf{pred}_{UNVU',V'}) \\&\quad = \mathsf{pred}_{UNVU',V'}(\mathsf{pred}_{U,VU'V'} + \mathsf{pred}_{U,VU'NV'})(1_{UVU'V'} + \sigma ^+_{UVU'NV',UNVU'V'} + 1_{UNVU'NV'}) \\&\quad = (UNV \ltimes \mathsf{pred}_{U',V'})\delta ^l_{UNV,U'V',U'NV'}((\mathsf{pred}_{U,V} \rtimes U'V') \\&\qquad + (\mathsf{pred}_{U,V} \rtimes U'NV'))(\delta ^l_{UV+UNV,U'V',U'NV'})^{-1} \\&\quad = (UNV \ltimes \mathsf{pred}_{U',V'})(\mathsf{pred}_{U,V} \rtimes U'V' + U'NV') \end{align*}
Next, in case neither
$f$
nor
$g$
is an instance of
$\mathsf{succ}$
,
$\mathsf{zero}$
, or
$\mathsf{pred}$
we have:
-
• (
$1$
-
$g$
): If
$f$
is
$1_U : U \to U$
and
$g : R \to S$
then we have:as required.
\begin{align*} & (1_U \rtimes R)(U \ltimes g) = 1_{UR}(U \ltimes g) = (U \ltimes g)1_{US} = (U \ltimes g)(1_U \rtimes S) \end{align*}
-
• (
$f$
-
$1$
): If
$f : R \to S$
and
$g$
is
$1_U : U \to U$
then we have:as required.
\begin{align*} & (f \rtimes U)(S \ltimes 1_U) = (f \rtimes U)1_{SU} = 1_{RU}(f \rtimes U) = (R \ltimes 1_U)(f \rtimes U) \end{align*}
-
• (
$\eta$
-
$g$
): If
$f$
is
$\eta _U : 0 \to U$
and
$g : R \to S$
then we have:as required.
\begin{align*} & (\eta _U \rtimes R)(U \ltimes g) = \eta _{UR}(U \ltimes g) = \eta _{US} = 1_0\eta _{US} = (0 \ltimes g)(\eta _U \rtimes S) \end{align*}
-
• (
$f$
-
$\eta$
): If
$f : R \to S$
and
$g$
is
$\eta _U : 0 \to U$
then we have:as required.
\begin{align*} & (f \rtimes 0)(S \ltimes \eta _U) = 1_0\eta _{SU} = \eta _{SU} = \eta _{RU}(f \rtimes U) = (R \ltimes \eta _U)(f \rtimes U) \end{align*}
-
• (
$\mu$
-
$g$
): If
$f$
is
$\mu _U : U + U \to U$
and
$g : R \to S$
then we have:as required.
\begin{align*} & (\mu _U \rtimes R)(U \ltimes g) = \mu _{UR}(U \ltimes g) = ((U \ltimes g) + (U \ltimes g))\mu _{US} = ((U+U) \ltimes g)(\mu _U \rtimes S) \end{align*}
-
• (
$f$
-
$\mu$
): If
$f : R \to S$
and
$g$
is
$\mu _U : U+U \to U$
then we have:as required.
\begin{align*} & (f \rtimes (U+U))(S \ltimes \mu _U) = \delta ^l_{R,U,U}((f \rtimes U) + (f \rtimes U))(\delta ^l_{S,U,U})^{-1}\delta ^l_{S,U,U}\mu _{SU} \\[3pt]&\quad = \delta ^l_{R,U,U}\mu _{RU}(f \rtimes U) = (R \ltimes \mu _U)(f \rtimes U) \end{align*}
-
• (
$0$
-
$g$
): If
$f$
is
$1_0 : 0 \to 0$
and
$g : R \to S$
then we have:as required.
\begin{align*} & (1_0 \rtimes R)(0 \ltimes g) = 1_0 = (0 \ltimes g)(1_0 \rtimes S) \end{align*}
-
• (
$f$
-
$0$
): If
$f : R \to S$
and
$g$
is
$1_0 : 0 \to 0$
then we have:as required.
\begin{align*} & (f \rtimes 0)(S \ltimes 1_0) = 1_0 = (R \ltimes 1_0)(f \rtimes 0) \end{align*}
-
• (
$\sigma$
-
$g$
): If
$f$
is
$\sigma ^+_{U,V} : U+V \to V+U$
and
$g : R \to S$
then we have:as required.
\begin{align*} & (\sigma ^+_{U,V} \rtimes R)((V+U) \ltimes g) = \sigma ^+_{UR,VR}((V \ltimes g) + (U \ltimes g)) \\[3pt]&\quad = ((U \ltimes g) + (V \ltimes g))\sigma ^+_{US,VS} = ((U+V) \ltimes g)(\sigma ^+_{U,V} \rtimes S) \end{align*}
-
• (
$f$
-
$\sigma$
): If
$f : R \to S$
and
$g$
is
$\sigma ^+_{U,V} : U+V \to V+U$
then we have:as required.
\begin{align*} & (f \rtimes (U+V))(S \ltimes \sigma ^+_{U,V}) = \delta ^l_{R,U,V}((f \rtimes U) + (f \rtimes V))(\delta ^l_{S,U,V})^{-1}(S \ltimes \sigma ^+_{U,V}) \\[3pt]&\quad \!= \delta ^l_{R,U,V}((f \rtimes U) + (f \rtimes V))\sigma ^+_{SU,SV}(\delta ^l_{S,V,U})^{-1} = \delta ^l_{R,U,V}\sigma ^+_{RU,RV}((f \rtimes U) + (f \rtimes V))(\delta ^l_{S,V,U})^{-1} \\[3pt]&\quad \!= (R \ltimes \sigma ^+_{U,V})\delta ^l_{R,V,U}((f \rtimes V) + (f \rtimes U))(\delta ^l_{S,V,U})^{-1} = (R \ltimes \sigma ^+_{U,V})(f \rtimes (V+U)) \end{align*}
Finally, the inductive cases are as follows:
-
• (
$\mathsf{Tr}$
-
$g$
): Given
$\mathsf{Tr}^U_{P,Q}(f) : P \to Q$
and
$g : R \to S$
for some
$f : P+U \to Q+U$
such that
$(f \rtimes R)((Q+U) \ltimes g) = ((P+U) \ltimes g)(f \rtimes S)$
we have:and so by the uniformity axiom we have
\begin{align*} & (f \rtimes R)((Q \ltimes g) + (U \ltimes g)) = (f \rtimes R)((Q+U) \ltimes g) \\[3pt]&\quad = ((P+U) \ltimes g)(f \rtimes S) = ((P \ltimes g) + (U \ltimes g))(f \rtimes S) \end{align*}
\begin{equation*} \mathsf{Tr}^{UR}_{PR,QR}(f \rtimes R)(Q \ltimes g) = (P \ltimes g)\mathsf{Tr}^{US}_{PS,QS}(f \rtimes S) \end{equation*}
as in:
which in turn gives:
as required.
\begin{align*} & (\mathsf{Tr}^U_{P,Q}(f) \rtimes R)(Q \ltimes g) = \mathsf{Tr}^{UR}_{PR,QR}(f \rtimes R)(Q \ltimes g) \\[3pt]&\quad = (P \ltimes g)\mathsf{Tr}^{US}_{PS,QS}(f \rtimes S) = (P \ltimes g)(\mathsf{Tr}^U_{P,Q}(f) \rtimes S) \end{align*}
-
• (
$f$
-
$\mathsf{Tr}$
): Given
$f : R \to S$
and
$\mathsf{Tr}^{U}_{P,Q}(g) : P \to Q$
for some
$g$
with
$(f \rtimes (P+U))(S \ltimes g) = $
$(R \ltimes g)(f \rtimes (Q+U))$
we have:and so by the uniformity axiom we have:
\begin{align*} & (\delta ^l_{R,P,U})^{-1}(R \ltimes g)\delta ^l_{S,Q,U}((f \rtimes Q) + (f \rtimes U)) = (\delta ^l_{R,P,U})^{-1}(R \ltimes g)(f \rtimes (Q+U))\delta ^l_{S,Q,U} \\[3pt]&\quad = (\delta ^l_{R,P,U})^{-1}(f \rtimes (P+U))(S \ltimes g)\delta ^l_{S,Q,U} = ((f \rtimes P) + (f \rtimes U))(\delta ^l_{S,P,U})^{-1}(S \ltimes g)\delta ^l_{S,Q,U} \end{align*}
as in:
\begin{equation*} \mathsf{Tr}^{RU}_{RP,RQ}((\delta ^l_{R,P,U})^{-1}(R \ltimes g)\delta ^l_{R,Q,U})(f \rtimes Q) = (f \rtimes P)\mathsf{Tr}^{SU}_{SP,SQ}((\delta ^l_{S,P,U})^{-1}(S \ltimes g)\delta ^l_{S,Q,U}) \end{equation*}
which in turn gives:
as required.
\begin{align*} & (f \rtimes P)(S \ltimes \mathsf{Tr}^U_{P,Q}(g)) = (f \rtimes P)\mathsf{Tr}^{SU}_{SP,SQ}((\delta ^l_{S,P,U})^{-1}(S \ltimes g)\delta ^l_{S,Q,U}) \\[3pt]&\quad = \mathsf{Tr}^{RU}_{RP,RQ}((\delta ^l_{R,P,U})^{-1}(R \ltimes g)\delta ^l_{R,Q,U})(f \rtimes Q) = (R \ltimes \mathsf{Tr}^U_{P,Q}(g))(f \rtimes Q) \end{align*}
-
• (
$\circ$
-
$g$
): Given
$f_1 : P \to T$
,
$f_2 : T \to Q$
, and
$g : R \to S$
such that
$(f_1 \rtimes R)(T \ltimes g) = (P \ltimes g)(f_1 \rtimes S)$
and
$(f_2 \rtimes R)(Q \ltimes g) = (T \ltimes g)(f_2 \rtimes S)$
, we have:as required.
\begin{align*} & (f_1f_2 \rtimes R)(Q \ltimes g) = (f_1 \rtimes R)(f_2 \rtimes R)(Q \ltimes g) \\[3pt]&\quad = (f_1 \rtimes R)(T \ltimes g)(f_2 \rtimes S) = (P \ltimes g)(f_1f_2 \rtimes S) \end{align*}
-
• (
$f$
-
$\circ$
): Given
$f : R \to S$
,
$g_1 : P \to T$
, and
$g_2 : T \to Q$
such that
$(f \rtimes P)(S \ltimes g_1) = (R \ltimes g_1)(f \rtimes T)$
and
$(f \rtimes T)(S \ltimes g_2) = (R \ltimes g_2)(f \rtimes Q)$
, we have:as required.
\begin{align*} & (f \rtimes P)(S \ltimes g_1g_2) = (f \rtimes P)(S \ltimes g_1)(S \ltimes g_2) \\[3pt]&\quad = (R \ltimes g_1)(f \rtimes T)(S \ltimes g_2) = (R \ltimes g_1g_2)(f \rtimes Q) \end{align*}
-
• (
$+$
-
$g$
): Given
$f_1 + f_2 : P_1 + P_2 \to Q_1 + Q_2$
and
$g : R \to S$
such that
$(f_1 \rtimes R)(Q_1 \ltimes g) = $
$(P_1 \ltimes g)(f_1 \rtimes S)$
and
$(f_2 \rtimes R)(Q_2 \ltimes g) = (P_2 \ltimes g)(f_2 \rtimes S)$
, we have:as required.
\begin{align*} & ((f_1 + f_2) \rtimes R)((Q_1 + Q_2) \ltimes g) = ((f_1 \rtimes R) + (f_2 \rtimes R))((Q_1 \ltimes g) + (Q_2 \ltimes g)) \\&\quad = (f_1 \rtimes R)(Q_1 \ltimes g) + (f_2 \rtimes R)(Q_2 \ltimes g) = (P_1 \ltimes g)(f_1 \rtimes S) + (P_2 \ltimes g)(f_2 \rtimes S) \\&\quad = ((P_1 + P_2) \ltimes g) + ((f_1 + f_2) \rtimes S) \end{align*}
-
• (
$f$
-
$+$
): Given
$f: R \to S$
and
$g_1 + g_2 : P_1 + P_2 \to Q_1 + Q_2$
such that
$(f \rtimes P_1)(S \ltimes g_1) = $
$(R \ltimes g_1)(f \rtimes Q_1)$
and
$(f \rtimes P_2)(S \ltimes g_2) = (R \ltimes g_2)(f \rtimes Q_2)$
, we have:
\begin{align*} & (f \rtimes (P_1 + P_2))(S \ltimes (g_1 + g_2)) \\&\quad = \delta ^l_{R,P_1,P_2}((f \rtimes P_1) + (f \rtimes P_2))(\delta ^l_{S,P_1,P_2})^{-1}\delta ^l_{S,P_1,P_2}((S \ltimes g_1) + (S \ltimes g_2))(\delta ^l_{S,Q_1,Q_2})^{-1} \\&\quad = \delta ^l_{R,P_1,P_2}((f \rtimes P_1)(S \ltimes g_1) + (f \rtimes P_2)(S \ltimes g_2))(\delta ^l_{S,Q_1,Q_2})^{-1} \\&\quad = \delta ^l_{R,P_1,P_2}((R \ltimes g_1)(f \rtimes Q_1) + (R \ltimes g_2)(f \rtimes Q_2))(\delta ^l_{S,Q_1,Q_2})^{-1} \\&\quad = \delta ^l_{R,P_1,P_2}((R \ltimes g_1) + (R \ltimes g_2))(\delta ^l_{R,Q_1,Q_2})^{-1}\delta ^l_{R,Q_1,Q_2}((f \rtimes Q_1) + (f \rtimes Q_2))(\delta ^l_{S,Q_1,Q_2})^{-1} \\&\quad = (R \ltimes (g_1 + g_2))(f \rtimes (Q_1 + Q_2)) \end{align*}
and the claim follows by induction.
This allows us to prove that our proposed multiplicative monoidal structure on
$\mathbb{A}$
does in fact define a monoidal category:
Lemma B.9.
$(\mathbb{A},\otimes ,I)$
is a strict monoidal category with
$- \otimes - : \mathbb{A} \times \mathbb{A} \to \mathbb{A}$
defined on arrows
$f : P \to Q$
and
$g : R \to S$
of
$\mathbb{A}$
as in:
\begin{equation*} f \otimes g = (f \rtimes R)(Q \ltimes g) \end{equation*}
Proof.
We begin by showing
$-\otimes -$
is a functor. It preserves identities as in:
\begin{align*} & 1_P \otimes 1_Q = (1_P \rtimes Q)(P \ltimes 1_Q) = 1_{PQ}1_{PQ} = 1_{PQ} = 1_{P \otimes Q} \end{align*}
and given
$f : P \to Q$
,
$g : R \to S$
,
$h : Q \to T$
,
$k : S \to H$
we have that
$-\otimes -$
preserves composition as in:
\begin{align*} & (f \otimes g)(h \otimes k) = (f \rtimes R)(Q \ltimes g)(h \rtimes S)(T \ltimes k) \\&\quad = (f \rtimes R)(h \rtimes R)(T \ltimes g)(T \ltimes k) \\&\quad = (hf \rtimes R)(T \ltimes gk) = hf \otimes gk \end{align*}
Moreover, we have that
$-\otimes -$
is associative as in:
\begin{align*} & (f \otimes g) \otimes h = ((f \otimes g) \rtimes T)(QS \ltimes h) \\&\quad = ((f \rtimes R)(Q \ltimes g) \rtimes T)(QS \ltimes h) \\&\quad = ((f \rtimes R) \rtimes T)((Q \ltimes g) \rtimes T)(Q \ltimes (S \ltimes h)) \\&\quad = ((f \rtimes R) \rtimes T)(Q \ltimes (g \rtimes T))(Q \ltimes (S \ltimes h)) \end{align*}
\begin{align*} &\quad = (f \rtimes RT)(Q \ltimes (g \rtimes T)(S \ltimes h)) \\&\quad = (f \rtimes RT)(Q \ltimes (g \otimes h)) = f \otimes (g \otimes h) \end{align*}
and finally we have that
$-\otimes -$
is unital as in:
\begin{equation*} f \otimes 1_I = (f \rtimes I)(Q \ltimes 1_I) = f1_Q = f \end{equation*}
and
\begin{equation*} 1_I \otimes f = (1_I \rtimes P)(I \ltimes f) = 1_Pf = f \end{equation*}
The claim follows.
From here it is easy to see that
$\otimes$
distributes over
$+$
:
Lemma B.10.
$(\mathbb{A},(+,0,\sigma ^+),(\otimes ,I),(\mu ,\eta ),(1,1),(\delta ^l,1))$
is a right-strict distributive monoidal category.
Proof.
We have already seen that
$(\mathbb{A},\otimes ,I)$
is a strict monoidal category (Lemma B.9), and we know that
$(\mathbb{A},+,0,\sigma ^+)$
is a symmetric strict monoidal category. To see that
$\delta ^l$
is a natural transformation, suppose
$f : P \to P'$
,
$g : Q \to Q'$
, and
$h : R \to R'$
in
$\mathbb{A}$
. Then we have:
\begin{align*} & \delta ^l_{P,Q,R}((f \otimes g) + (f \otimes h)) = \delta ^l_{P,Q,R}( (f \rtimes Q)(P' \ltimes g) + (f \rtimes R)(P' \ltimes h)) \\&\quad = \delta ^l_{P,Q,R} ((f \rtimes Q) + (f \rtimes R))((P' \ltimes g) + (P' \ltimes h)) \\&\quad = \delta ^l_{P,Q,R} ((f \rtimes Q) + (f \rtimes R))(\delta ^l_{P',Q,R})^{-1}\delta ^l_{P',Q,R}((P' \ltimes g) + (P' \ltimes h)) \\&\quad = (f \rtimes (Q+R))(P' \ltimes (g + h))\delta ^l_{P',Q',R'} = (f \otimes (g + h))\delta ^l_{P',Q',R'} \end{align*}
and so
$\delta ^l$
is natural, as required. Next, for right dsitributivity we have:
\begin{align*} & (f + g) \otimes h = ((f + g) \rtimes R)((P' + Q') \ltimes h) \\&\quad = ((f \rtimes R) + (g \rtimes R))((P' \ltimes h) + (Q' \ltimes h)) \\&\quad = (f \rtimes R)(P' \ltimes h) + (g \rtimes R)(Q' \ltimes h) = (f \otimes h) + (g \otimes h) \end{align*}
and for left and right annihilation we have:
\begin{equation*} f \otimes 1_0 = (f \rtimes 0)(P' \ltimes 1_0) = 1_01_0 = 1_0 \end{equation*}
and
\begin{equation*} 1_0 \otimes f = (1_0 \rtimes P)(0 \ltimes f) = 1_01_0 = 1_0 \end{equation*}
Of the remaining conditions,
$\mathbb{A}$
must satisfy to be a right-strict distributive monoidal category, all but one are shown to hold in Lemma B.5. For the final condition, we have
$\sigma ^+_{PR,QR} = \sigma ^+_{P,Q} \rtimes R = \sigma ^+_{P,Q} \otimes 1_R$
via Lemma B.4. The claim follows.
Now since
$\textbf {[N1]}$
and
$\textbf {[N2]}$
give an isomorphism
$I+N \cong N$
, we may conclude:
Theorem B.11.
$(\mathbb{A},(+,0,\sigma ^+),(\otimes ,I),(\mu ,\eta ),\mathsf{Tr},(1,1),(\delta ^l,1),(N,\iota ))$
is a right-strict Elgot category.
Open access
