Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Functoriality of quotients of algebraic theories

Ralph Sarkis (Sep 30 2020 at 14:02):

For any algebraic theory $T$ and additional equations $E$ over the same signature, there is a clear embedding $\mathbf{A}(T+E) \hookrightarrow \mathbf{A}(T)$, where $\mathbf{A}(\cdot)$ denotes the category of algebras and morphisms over the theory given in argument. The natural way to go in the opposite direction is via quotients. I have not really dealt with all the details but using the usual notion of quotients via equivalence classes generated by the equations in $E$ should lead to a functor which is a left inverse of the embedding. Is there any source that shows this is a functor?

Ralph Sarkis (Sep 30 2020 at 14:02):

I don't believe functor embeddings always have a left inverse, but since they are monomorphisms, they are "close" to having one. I was wondering if we are in a sufficiently nice context that the emebeddings above always have a left inverse (without needing the explicit construction). My intuition is that since we are working with concrete categories, and monomorphisms split in $\textbf{Set}$, we might be able to use this.

Ralph Sarkis (Sep 30 2020 at 14:02):

Providing a bit more context, my original question is on the monad side of this picture. Let $M$ and $M'$ be monads, does an embedding $U: \text{EM}(M') \hookrightarrow \text{EM}(M)$ always have a left inverse (where $\text{EM}$ denotes the Eilenberg-Moore category)? What if $U = U^{m} := (A, \alpha) \mapsto (A, \alpha \circ m_A)$ where $m: M \Rightarrow M'$ is an epic monad map (i.e.: something akin to a quotient of theories)? ($U^m$ is a functor by Theorem 6.3 in Toposes, Triples and Theories and an embedding by surjectivity of each $m_A$.)

Nathanael Arkor (Sep 30 2020 at 14:10):

For any map of Lawvere theories $f : T \to T'$, there is an induced adjoint pair $f^* : \mathrm{Mod}(T', \mathbf{Set}) \leftrightarrows \mathrm{Mod}(T, \mathbf{Set}) : f_!$, where $f^*$ is given by precomposition with $f$. In your case, $T \to T_E$ is a coprojection, and so you have a left adjoint as expected.

Reid Barton (Sep 30 2020 at 15:03):

And when we only add extra equations (and not extra operations or sorts), the forgetful functor $f^*$ is fully faithful by definition (I guess this is what you mean by "embedding"), and therefore its left adjoint $f_!$ is the reflection into a reflective subcategory, and in particular the counit is a natural isomorphism--I guess this is your "left inverse".

Reid Barton (Sep 30 2020 at 15:06):

But the construction of the left adjoint ultimately relies on an argument similar to the one you are imagining involving quotients by some inductively defined equivalence relation generated by $E$. For totally arbitrary monads $M$ and $M'$ (i.e., not finitary and not even accessible) I don't think there's a reason to expect this left adjoint to exist.

Ralph Sarkis (Sep 30 2020 at 15:51):

That's some great insights, thank you! I thought there would be a nicer situation, but having a (reflective) subcategories is already enough for me.

John Baez (Sep 30 2020 at 21:39):

Nathanael Arkor said:

For any map of Lawvere theories $f : T \to T'$, there is an induced adjoint pair $f^* : \mathrm{Mod}(T', \mathbf{Set}) \leftrightarrows \mathrm{Mod}(T, \mathbf{Set}) : f_!$, where $f^*$ is given by precomposition with $f$. In your case, $T \to T_E$ is a coprojection, and so you have a left adjoint as expected.

Yes, this is nice.

Ralph phrased the question in terms of monads, and you answered it in terms of Lawvere theories, so there's a bit of a disconnect here. Of course finitary monads are "the same" as Lawvere theories, so there's not problem at all for those.

$\kappa$-ary monads for some larger cardinal $\kappa$ are similarly "the same" as $\kappa$-ary Lawvere theories: the sort of obvious generalization of Lawvere theories to theories that allow operations of infinite arity as long as the arity is $\le \kappa$. And I believe there's still a left adjoint in this case. So what Ralph wants should still work for
$\kappa$-ary monads.

If you don't put any bound on the arity, things can get nasty, and I'm reluctant to guess what happens then.

John Baez (Sep 30 2020 at 21:45):

Ralph was looking for a reference, though... for the case of plain old Lawvere theories the existence of the desired left adjoint should be "classical", but where was it first proved?

There's a proof here:

• Todd Trimble, Multisorted Lawvere theories.

It's Theorem 3.3. This does a more general case! It does the case of multisorted Lawvere theories, and looks at their models not just in Set but in any "CMC": cartesian monoidally cocomplete category, i.e. a category with products and small colimits, where products distribute over colimits. Furthermore, it handles not just the case of getting one Lawvere theory from another by adding extra equations, but a general map of Lawvere theories.

So this is simultaneously more than what Ralph wanted, and less - since it only handles finitary monads on Set (aka ordinary Lawvere theories), not those of higher arity.

Nathanael Arkor (Sep 30 2020 at 21:52):

or the case of plain old Lawvere theories the existence of the desired left adjoint should be "classical", but where was it first proved?

The result in the one-sorted setting goes all the way back to Lawvere's thesis. The result for non-finitary algebraic theories is proven by Linton in Some Aspects of Equational Categories.

John Baez (Sep 30 2020 at 21:53):

Cool, thanks. If you knew all that, what was your question about? :upside_down:

Nathanael Arkor (Sep 30 2020 at 21:53):

It wasn't my question :grinning_face_with_smiling_eyes:

John Baez (Sep 30 2020 at 21:54):

Oh, whoops - sorry. Well, that solves that mystery. If only all were so easily solved!

John Baez (Sep 30 2020 at 22:04):

My problem is that I don't yet have a good mental model of what the main people posting here know about. That seems to be my main way of keeping track of names!

John Baez (Sep 30 2020 at 22:04):

Bad, bad.

Ralph Sarkis (Oct 01 2020 at 05:43):

To be honest, I only vaguely know about Lawvere theories, but I was able to understand all your answers after a quick dive in the nLab. Especially since I was interested in finitary monads. I could also have been more precise in my question, but I don't mind more complicated answers; this is why I spend some of my time reading the discussions here.

John Baez (Oct 01 2020 at 16:54):

If you like finitary monads you'll love Lawvere theories. A Lawvere theory is the practical way to specify a finitary monad on Set by specifying a bunch of operations obeying a bunch of equations.