Merging single-sorted and multi-sorted theories

Question

The general theory of single-sorted (say, algebraic) theories is very similar to the general theory of multi-sorted (algebraic) theories. Each variable gets a sort, but apart from that nothing really changes (at least, in those results that I am familar with right now).

Single-sorted theories are based on $\mathbf{Set}$, whereas multi-sorted theories are based on $\mathbf{Set}^S$, where $S$ is the set of sorts. Both of these categories are very special (for example, Grothendieck toposes), so this begs the question: For which categories $\mathcal{M}$ (of "models") can we easily develop the notion of a (say, algebraic) theory $\mathcal{T}$ relative to $\mathcal{M}$? In particular we should get a category $\mathbf{Alg}(\mathcal{T})$ of $\mathcal{T}$-algebras with a monadic accessible functor to $\mathcal{M}$. Some results which hold for $\mathbf{Set}^S$ (for example, the existence of regular-projective generators in $\mathbf{Alg}(\mathcal{T})$) should be adjusted since $\mathcal{M}$ should not necessarily be generated by projectives.

I assume this must be standard. Where can I read more about that?

Since it was asked in the comments: I am mainly thinking of theories via their presentations. So a classical algebraic theory consists of a signature of operation symbols and a bunch of equations between them. So the single-sorted case has an evident generalization: an operation symbol has an arity, which is a (finitely presentable) object $n \in \mathcal{M}$. This will be realized then as a morphism $X^n \to X$ for $\mathcal{M}$-cotensored categories. But that is not the correct choice for multi-sorted theories, and I don't want to make a separate definition for these.

Answer 1

The answer to your question really depends on just how closely you want the theory of "algebraic theories relative to $\mathcal M$" to mirror the theory of classical ($S$-sorted) algebraic theories.

Perhaps the fundamental theorem of algebraic theories is the correspondence between finitary algebraic theories and finitary monads on the category of sets (or between infinitary algebraic theories and arbitrary monads on the category of sets). If we take this correspondence as being characteristic of "algebraic" theories (e.g. as opposed, say, to essentially algebraic theories), then there is a good general theory that recovers many of the classical theorems of algebraic theories.

There have been many frameworks for monad–theory correspondences to date, but the most general framework is that presented in Chapters 5 – 7 of Arkor's thesis Monadic and Higher-Order Structure (a comparison with previous frameworks may be found in Chapter 7). In this framework, an algebraic theory is specified relative to an arbitrary dense functor $j : \mathcal A \to \mathcal E$.

Definition (6.2.1). Let $j : \mathcal A \to \mathcal E$ be a dense functor. A $j$-theory is an identity-on-objects functor from $\mathcal A$ that admits a right $j$-relative adjoint.

Under suitable assumptions (see Chapter 3 of the thesis), the relative adjointness condition is equivalent to a colimit-preservation condition: for instance, classical finitary algebraic theories are precisely theories relative to the inclusion $\mathrm{FinSet} \to \mathrm{Set}$ (note that with this convention, algebraic theories are categories with finite coproducts, as in Lawvere's original convention, rather than categories with finite products).

Besides capturing the examples of interest, the theorem that justifies this definition is the following.

Theorem (6.2.2). The category of $j$-theories is equivalent to the category of $j$-relative monads.

This may seem a weaker result at first than expected, because not every relative monad is induced by a monad. However, it turns out that $j$-relative monads are equivalent to certain monads on $\mathcal E$ under mild cocompleteness assumptions on $\mathcal E$.

Theorem (5.4.7). Suppose that $\mathcal E$ admits all (pointwise) left extensions along $j$. Then the category of $j$-theories is equivalent to the category of $j$-ary monads on $\mathcal E$.

In particular, the requisite left extensions exist if and only if the forgetful functor from the category of algebras for every $j$-relative monad admits a left adjoint (rather than simply a left $j$-relative adjoint).

For example, if we take $j$ to be the inclusion $\mathrm{FinSet}[S] \to \mathrm{Set}^S$ of category of finite $S$-sorted sets into the category of $S$-sorted sets, we obtain the expected classical result.

Corollary. For every set $S$, the category of $(\mathrm{FinSet}[S] \to \mathrm{Set}^S)$-theories is equivalent to the category of (strongly) finitary monads on $\mathrm{Set}^S$.

While the monad–theory correspondence justifies to a certain extent this definition, we should like other classical results to carry across to this setting. A nice consequence of the definitions is that, just as the theory of classical algebraic theories can be seen as consequences of the theory of (finitary) monads on the category of sets, the theory of $j$-theories can be seen as consequences of the theory of $j$-relative monads. So, for instance, we can observe that the forgetful functor from the category of models for a $j$-theory (which is equivalent to the category of algebras for the corresponding (relative) monad) is accessible under mild assumptions on $j$.

Theorem (3.2.5). Let $j \colon \mathcal A \to \mathcal E$ exhibit the free cocompletion of $\mathcal A$ under a class $\Phi$ of colimits. Then the corresponding monad (and hence the forgetful functor) is $\Phi$-cocontinuous.

We can also obtain a generalisation of the fact that algebraic functors (i.e. those functors between categories of models induced by morphisms of algebraic theories) admit left adjoints, under some cocompleteness assumptions. For simplicity, I will state it under stronger assumptions than are strictly necessary, but are usually present in examples (see Corollary 6.7 of Arkor–McDermott's Relative monadicity for a precise statement); the following is a consequence of Example 2.13 of The nerve theorem for relative monads.

Theorem. Let $\Psi$ be a sound class of weights and let $j \colon \mathcal A \to \mathcal E$ exhibit the free cocompletion of a $\Psi$-cocomplete category $\mathcal A$ under $\Psi$-flat colimits. Then the category of models for every $j$-theory is locally $\Psi$-presentable, and every morphism of $j$-theories induces a $\Psi$-accessible monadic right adjoint between their categories of models.

Another result worth mentioning is that we may characterise the categories of models of $j$-theories in terms of their forgetful functors, via a relative analogue of the classical monadicity theorem; this is the main result of Relative monadicity.

Theorem. Let $U \colon \mathcal X \to \mathcal E$ be a functor. Then $U$ exhibits the category of models for a $j$-theory if and only if $U$ admits a left $j$-relative adjoint and creates $j$-absolute colimits.

In concrete examples, one may typically characterise the $j$-absolute colimits to obtain sharper statements (as is the case for classical algebraic theories, for instance).

Since this answer is already quite long, I will end here, but am happy to prove further references, e.g. for analogues of other classical theorems about algebraic theories in this setting, if you mention the specific results in which you are interested. I should also mention that all of the above holds more generally for enrichment in a monoidal category (or even in a bicategory); in fact, the works I have mentioned take place in the setting of formal category theory, so hold even more generally for internal algebraic theories, etc.

Addendum. In the comments, Martin Brandenburg mentioned they were interested in presentations for theories. In that vein, I should mention the work of Lucyshyn-Wright and Parker, e.g. Diagrammatic presentations of enriched monads and varieties for a subcategory of arities, which develops a notion of presentation at a similar level of generality (at least in the setting of enriched categories) to that mentioned above.

Answer 2

I was about to write a long answer, but varkor stole the scene. I think his answer is pretty good and I'd like to complement it with a bunch of references that I find relevant.

The general mood of the references below is that a monad over Set is, in particular, an enriched monad over Set. This is not irrelevant when it comes to the interpretation of monads as theories. Of course, in the spirit of nervous monads (and relative monads in general), one can still develop a lot the theory. But when we take a more Yoneda-point of view, say in the spirit of a completeness-like theorem, enrichment starts to matter.

• Rosický, Metric monads.
• Rosický, Discrete equational theories.
• Adámek et al, Quantitative Algebras and a Classification of Metric Monads.
• Adámek, Varieties of quantitative algebras as categories.

The papers above were all inspired by recent developments initiated by Plotkin et al on the general topic of quantitative algebras, but (especially Rosický's work) cover a lot of other cases providing great intuition.

I should stress that Quantitative Algebras and a Classification of Metric Monads stresses on the gap between enriched monads and general monads, clarifying (or I should say hinting) the difference in the two approaches when it comes to logical repercussions.

There is also a nice talk by Adámek on youtube given at the Brno Algebra Seminar where he discusses this issue.

Answer 3

A more syntactic kind of presentation is available if the generality of the categories $\mathcal{M}$ is more restricted. Specifically, Leena Subramaniam's thesis From dependent type theory to higher algebraic structures shows that if $\mathcal{M}$ is a presheaf category $\mathrm{Set}^{C^{\mathrm{op}}}$ where $C$ is a direct category, then finitary monads on $\mathcal{M}$ are equivalent to a subclass of generalized algebraic theories, there called "dependently typed algebraic theories", where the generating types and their dependencies are specified by $C$.