Algebraic Theory

Categorical Definition

Following Algebraic Theories: A Categorical Introduction to General Algebra, an algebraic theory is simply a Category $\mathcal{T}$ that has Finite Products. This rather general definition aims to capture the calculus of Simultaneous Substitutions that arise from the syntactic definition of algebraic theories. Moreover, algebraic functors are functors that preserve finite products; this gives rise to a Bicategory (or 2-Category, depending on the strictness involved).

Note that an algebraic theory $\mathcal{T}$ may carry additional structure, but this structure is not guaranteed to be preserved by algebraic functors.

As noted in by Adamek et al, this bicategory looks a lot like the Category of Modules over a Commutative Semiring:

• It has Biproducts: the product $\mathcal{A}\times\mathcal{B}$ of categories with finite products is also a coproduct, with inclusions $\iota_{1}:\mathcal{A}\to\mathcal{A}\times\mathcal{B},\iota_{2}:\mathcal{B}\to \mathcal{A}\times\mathcal{B}$ given by $\iota_{1}(A)=(A,\top_{B})$ and $\iota_{2}(B)=(\top_{A},B)$. Moreover, for each pair of algebraic functors $F:\mathcal{A}\to\mathcal{C}$ and $G:\mathcal{B}\to\mathcal{C}$, there is a unique algebraic functor $[F,G]:\mathcal{A}\times\mathcal{B}\to\mathcal{C}$ with $[F,G]\circ\iota_{1}\cong F$ and $[F,G]\circ\iota_{2}\cong G$ given by:

  • $[F,G](A,B)=F(A)\times G(B)$

  • $[F,G](f,g)=F(f)\times G(g)$

  To see that $[F,G]$ is product preserving, recall that finite products in $\mathcal{A}\times\mathcal{B}$ are given componentwise; EG:

  • $\prod_{i:[n]}(A_{i},B_{i})=\left(\prod_{i:[n]}A_{i},\prod_{i:[n]}B_{i}\right)$

  This means that by definition

  • $[F,G]\left(\prod_{i:[n]}(A_{i},B_{i})\right)=F\left(\prod_{i:[n]}A_{i}\right) \times G\left(\prod_{i:[n]}B_{i}\right)$

  To show that $[F,G]$ is product preserving, we need to show that the diagram formed by

  • $F(\pi_{i})\times G(\pi_{i}):F\left(\prod_{i:[n]}A_{i}\right)\times G\left( \prod_{i:[n]}B_{i}\right)\to F(A_{i})\times G(B_{i})$

  is a product diagram in $\mathcal{C}$.

  Let $C:\mathcal{C}$ be an object in $\mathcal{C}$ equipped with maps $f_{i}:\mathcal{C}\to F(A_{i})\times G(B_{i})$. By the universal property of products in $\mathcal{C}$, to construct a map

  $\par C\to F\left(\prod_{i:[n]}A_{i}\right)\times G\left(\prod_{i:[n]}B_{i} \right)\par$

  it suffices to give a pair of maps

  • $C\to F\left(\prod_{i:[n]}A_{i}\right)$

  • $C\to G\left(\prod_{i:[n]}B_{i}\right)$

  However, $F$ and $G$ are both product preserving, so it further suffices to give families of maps

  • $C\to F(A_{i})$

  • $C\to G(B_{i})$

  which we can get from $f_{i}$.

  Note that biproducts take an $S$-sorted theory and an $S^{\prime}$-sorted theory to an $S+S^{\prime}$-sorted theory.

• It is Symmetric Monoidal: much like we can consider Bilinear (and more generally, Multilinear Maps) between (bi)modules, we can consider bilinear and multilinear maps of algebraic theories. These are bifunctors $F:\mathcal{A}\times\mathcal{B}\to\mathcal{C}$ that preserve products "separately" in each variable; EG, for each $A:\mathcal{A}$, the functor $F(A,-)$ is algebraic and for each $B:\mathcal{B}$, $F(-,B)$ is algebraic.

  It's worth pausing to unfold exactly what this is saying. For the sake of concreteness, consider the theories $\mathcal{T}_{\mathrm{Grp}}$ and $\mathcal{T}_{\mathrm{Mon}}$, and a bifunctor $F:\mathcal{T}_{\mathrm{Grp}}\times\mathcal{T}_{\mathrm{Mon}}\to\mathrm{Sets}{.}$. If $F$ preserved products in $\mathcal{T}_{\mathrm{Grp}}\times\mathcal{T}_{\mathrm{Mon}}$, then we could $\eta$-expand it to $[F\circ\iota_{1},F\circ\iota_{2}]$ by the previous section. This means that $F$ is forced to send a pair of contexts $(\Gamma:\mathcal{T}_{\mathrm{Grp}},\Delta:\mathcal{T}_{\mathrm{Mon}})$ to the product $F(\Gamma,\bullet)\times F(\bullet,\Delta)$; EG: a pair of sets. Moreover, $F$ will equip the set $F(x:\star,\bullet)$ with the structure of a group, and $F(\bullet,x:\star)$ with the structure of a monoid.

  Now, consider the case where $F$ only preserves products separately. Let's unfold what exactly that condition means:

  • For all $A:\mathcal{A}$, the diagram formed by $F(mathrm{id}{ifx..lse\par i},\pi_{i}):F\left(A,\prod_{i:[n]}B_{i}\right)\to F (A,B_{i})$ is a product diagram in $\mathcal{C}$.

  • For all $B:\mathcal{B}$, the diagram formed by $F(\pi_{i},mathrm{id}{ifx..lse\par i}):F\left(\prod_{i:[n]}A_{i},B\right)\to F (A_{i},B)$ is a product diagram in $\mathcal{C}$.

  According to a remark by Lawvere there is a classifying object for these bilinear algebraic functors, but the details on this are scarce.

• It is Symmetric Closed: the Functor Category $[\mathcal{A},\mathcal{B}]$ of finite product-preserving functors is itself a finite-product category, with the product of functors $F,G:\mathcal{A}\to\mathcal{B}$ given by taking pointwise products in $\mathcal{B}$. Recall that models of algebraic theories are product preserving functors, so the functor category describes the algebraic theory of models of $\mathcal{A}$ in $\mathcal{B}$.