This question (as the title obviously suggests) is similar to, or a continuation of, this question that was asked years ago on MO by a different user.
The present question, though, is different from the old one in some ways:
-
The old question focussed on reference request. My question instead, while clear and readable references are welcome, is more focussed on getting some quick and dirty intuitive understanding. Most probably what I'm looking for is already buried in Tom Leinster's comprehensive monograph Higher operads, higher categories, but currently I'm not planning on reading it (or going in a detailed way through other technical material on the topic).
-
I already have an idea of how algebraic theories (also called Lawvere theories) and monads differ from each other. I would also like to understand how operads fit into this picture.
-
In the old question the semantic aspect was not considered (yes, there's the expression "model of theories" in that question, but just in the sense of "way of understanding the notion of mathematical algebraic theory", not in the more technical sense of semantics).
In what follows I may be missing some hypothesis: let me know or just add them if necessary.
Here is what I remember about the algebraic theories vs monads relationship. Algebraic theories correspond one-to-one to finitary monads on $\mathbf{Set}$, and the correspondence is an equivalence of categories. If one wants to recover an equivalence on the level of all monads on the category of sets, then one has to relax the finitary condition on the other side, so getting a generalization of the notion of Lawvere theory to some notion of "infinitary Lawvere theory". Furthermore, given a (just plain old, or possibly non-finitary) Lawvere theory $\mathcal L$ and the corresponding monad $\mathscr T$, a model of (also called algebra for) $\mathcal L$ in $\mathbf{Set}$ corresponds to a $\mathscr{T}$-algebra (necessarily in $\mathbf{Set}$), and this correspondence extends to an equivalence of the categories of algebras
$$\mathrm{Alg}^{\mathcal{L}}(\mathbf{Set}):=\mathrm{Hom}_{\times}(\mathcal{L},\mathbf{Set})\simeq \mathrm{Alg}^{\mathscr T}(\mathbf{Set})=:\mathbf{Set}^{\mathscr T}\,.$$
There is also the variant with arities. While usual Lawvere theories / finitary monads have finite ordinals as arities, and the corresponding non-finitary versions have sets as arities, one can introduce the notions of Lawvere theory with arities from a category $\mathfrak{A}$ and monads with arities from $\mathfrak{A}$, and again one has an equivalence between these notions, and an equivalence between the algebras in $\mathbf{Set}$.
a) How do operads fit into all this? Are operads somehow more general or less general objects than monads/theories (with all bells and whistles)?
There is an asymmetry between the notion of semantics for Lawvere theories and for monads (In what follows I will drop the finitary assumption). Namely, every Lawvere theory $\mathcal{L}$, as remarked above, is essentially a monad $\mathscr{T}_{\mathcal{L}}$ on $\mathbf{Set}$; though it can have models in every (suitable) category $\mathcal C$: just define the category of models of $\mathcal L$ in $\mathcal C$ to be $\mathrm{Hom}_{\times}(\mathcal L,\mathcal C)$. On the other hand, a monad $\mathscr T$ on $\mathbf{Set}$, by definition, only has models (aka algebras) in $\mathbf{Set}$. To remedy this, one introduces $\mathcal{V}$-enriched monads $\mathscr T$, where $\mathcal{V}$ is a given monoidal category, and $\mathscr T$-algebras are now objects of $\mathcal{V}$ (endowed with some further structure). If I get it correct, there is now an equivalence of categories $\mathrm{Hom}_{\otimes}(\mathcal{L},\mathcal V)\simeq \mathcal{V}^{\mathscr{T}}$.
But models of $\mathcal L$ are related to each other: you can take, again if I get it correct, (nonstrict?) $\otimes$-functors $\mathcal{V}\to\mathcal{V}'$ intertwining the (strict?) tensor functors $\mathcal{L}\to\mathcal{V}$ and $\mathcal{L}\to\mathcal{V}'$.
b) Can we read these "inter-model" relationships in the language of (enriched) monads?
c) How does the above semantic aspect go for operads and how, roughly, does the translation go from there to monads/theories (and viceversa)?
d Is there a "natural" symultaneous generalization of all the three things (theories, monads, and operads)? Does also the notions of semantics have a "natural" common generalization?
Edit. I had written the above (comprising questions a),…,d) ) some time ago, and just posted it now. But I forgot that I also wrote essentially the same questions in a perhaps more systematic way! I'm now going to post it below, without deleting the above paragraphs.
Q.1 What is the most general monads/theories equivalence to date? (possibly taking into account at the same time: arities, enrichment, and maybe sorts)
Q.2 What is the most general monads/algebras adjunction? (again, possibly throwing arities, enrichment, and maybe sorts, simultaneously into the mix)
$$\mathrm{Free}^T:\mathcal{E}\rightleftarrows \mathrm{Alg}^T(\mathcal{E})=:\mathcal{E}^T:U^T$$
where $T$ is a monad on $\mathcal{E}$, $U^T$ is a forgetful functor and $\mathrm{Free}^T$ a "free $T$-algebra" functor.
Q.3 Which is the relation between the different notions of semantics (for monads and theories)? Can enrichment "cure" this asymmetry?
This question was further explained a bit in question b) above.
Q.4 How far are operads from being algebraic theories?
There's an article by Leinster in which it is shown that the natural functor
$$G:\mathbf{Opd}\to \mathbf{Mnd}(\mathbf{Set}),\quad P\mapsto T_P$$
where
$$T_P(X):=\amalg_{n\in \mathbb{N}}P(n)\times X^{\times n}$$
is not an equivalence, and it is shown that the essential image of $G$ is given by "strongly regular finitary monads" on $\mathbf{Set}$, or equivalently by those Cartesian monads $T$ admitting a Cartesian monad morphism to the "free monoid monad". In the case of symmetric operads, $G$ becomes an equivalence.
So, question Q.4 is about such a functor $G$ in the most general setting (arities, enrichment,…), and can be seen as asking: which properties does such a functor $G$ have? What is a characterization of its essential image? What is the (essential) fiber of $G$ over a $T\in G(\mathbf{Opd})$?
Q.5 How does the notion of semantics for operads (well, it's algebras for an operad) relate to the notion of semantics for monads?
(this is similar to question Q.3, but featuring operads instead)
Q.6 In the light of the above, what is an operad, intuitively?
An operad $P$ has, in general, "more structure" than its associated monad $T_P$ ($G$ not injective). Also, $P$ is "more rigid" an object than $T_P$ ($G$ not full). So what do these extra things amount to? This must be some sort of detail, because clearly both monads and operads "want" to be a formalization of the intuitive notion of "algebraic theory".
Q.7 Do all the above considerations naturally extend to the case of $T$-categories instead of $T$-algebras? Maybe one has to consider colored operads? Or sorts?
Q.8 Which further structure on a monad/theory describes an equational theory? Same question in arities, enriched, or sorts, flavor.
This is about the distinction between e.g. the (logical formal) equational theory of groups and the Lawvere theory of groups (or, equivalently, the corresponding monad). So, what further structure on a theory/monad can be seen as a "presentation" of it.
Also, which properties does the functor
$$\{ \textrm{equational theories}\}\to \mathbf{Mnd}$$
have? Ess. surjective? Full? (I think not). Faithful? (again, no…).
Best Answer
Lawvere theories can be thought of as "cartesian operads." That is, we have an analogy
$$\text{Lawvere theories} : \text{cartesian monoidal categories} :: \text{operads} : \text{symmetric monoidal categories}.$$
Consider the 2-category of symmetric monoidal cocomplete categories (where the monoidal structure distributes over colimits in both variables), or SMCCs for short, which you can think of as a flavor of categorified commutative rings (where colimits categorify addition and the symmetric monoidal structure categorifies multiplication). Examples include quasicoherent sheaves on some scheme or stack, in particular modules over a commutative ring.
The free such thing on a point is the symmetric monoidal category $S = \text{Psh}(\text{FinSet}^{\times})$ of combinatorial species equipped with the symmetric monoidal structure given by Day convolution starting from disjoint union, which you can think of as a categorified polynomial / power series ring. (Exercise: show that $\text{FinSet}^{\times}$ with disjoint union is the free symmetric monoidal category on a point.)
Now, if $C$ is any other SMCC, we have an equivalence $C \cong [S, C]$ of categories (where $[-, -]$ denotes homs in this 2-category: symmetric monoidal cocontinuous functors). It follows that every SMCC admits a canonical action by the monoid $[S, S] \cong S$ under composition, which is again combinatorial species, but now equipped with a new (no longer symmetric) monoidal structure, the sustitution product, which categorifies composition of power series.
This is a nice exercise. The significance of this observation is that the action of $S$ on every SMCC means that monoids in $S$ correspond to natural families of monads acting on every SMCC: explicitly, if $O_n$ is an operad, the corresponding family of monads acting on every SMCC has underlying functor the corresponding "power series"
$$X \mapsto \bigsqcup_n O_n \times_{S_n} X^{\otimes n}.$$
Hence:
Now you can tell exactly the same story with "monoidal" instead of "symmetric monoidal," and you will get not-necessarily-symmetric operads. You can also tell exactly the same story with "cartesian monoidal" instead of "symmetric monoidal," and you will get Lawvere theories. In more detail:
Now consider the 2-category of cartesian monoidal cocomplete categories (where products distribute over colimits in both variables), or CMCCs for short. Examples include any Grothendieck topos. The free such thing on a point is the cartesian monoidal category $F = \text{Psh}(\text{FinSet}^{op})$, which for the same reasons as above also has a substitution product. (Exercise #1: show that $\text{FinSet}^{op}$ is the free cartesian monoidal category on a point.) (Exercise #2: show that $\text{Psh}(\text{FinSet}^{op}) \cong [\text{FinSet}, \text{Set}]$, with the substitution product, is monoidally equivalent to the monoidal category of finitary endofunctors of $\text{Set}$, with the composition product.)
As above, $F$ acts on every CMCC, so Lawvere theories correspond to natural families of monads acting on every CMCC: explicitly, if $L_n$ is a Lawvere theory, the corresponding family of monads has underlying functor
$$X \mapsto \int^n L_n \times X^n$$
where the coend is indexed over the category of finite sets. (The above formula for operads is also a coend.) Hence:
You might object a little to this story because you can talk about algebras over operads and models of Lawvere theories without requiring the existence of colimits, just a symmetric monoidal or cartesian monoidal structure respectively. But this isn't much of an issue in practice: just pass to the presheaf category.
Todd Trimble has written about this circle of ideas on the nLab, for example here.
This story admits very clean generalizations. For example you can try talking about braided monoidal cocomplete categories and you will get a notion of "braided operad"; you can enrich everything in sight; generally you can talk about natural families of endofunctors on any kind of category with extra structure (these correspond to endomorphisms of the forgetful functor from categories-with-extra-structure to categories), and from there you can talk about natural families of monads.