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: theory: category theory

Topic: enriched algebraic theories & monads


view this post on Zulip Nathanael Arkor (Jun 05 2020 at 00:30):

@Rory Lucyshyn-Wright: if you don't mind my asking here, I recently came across your paper "Enriched algebraic theories and monads for a system of arities" and I was wondering if you know how it relates to Bourke & Garner's "Monads and theories" (https://arxiv.org/abs/1805.04346). They both seem like very general frameworks, but it's not immediately clear to me how much overlap there is. Thank you!

view this post on Zulip Nathanael Arkor (Jun 05 2020 at 00:34):

Theorem 7.8, and its suggestive relationship to Kleisli bicategories, seems particularly evocative to me, but I haven't had a chance to read the paper in depth yet.

view this post on Zulip Nathanael Arkor (Jun 05 2020 at 00:37):

I'm surprised I haven't come across this paper sooner; it looks fascinating.

view this post on Zulip fosco (Jun 07 2020 at 09:46):

I'm assuming you're the varkor that answered my question on MO. Would you like to go through the paper together? :-) I'm looking forward to study it in depth, and I work better in good company.

view this post on Zulip Soichiro Fujii (Jun 08 2020 at 00:39):

Sounds interesting... I also wanted to study these papers.

view this post on Zulip Nathanael Arkor (Jun 08 2020 at 01:23):

I'd certainly be interested in studying the paper; however, I won't be able to start immediately, as I currently have a talk to prepare :)

view this post on Zulip Joe Moeller (Jun 08 2020 at 01:40):

I'd also like to study the paper. I'v recently thought I could use it, but I need to study it more.

view this post on Zulip Philip Saville (Jun 08 2020 at 08:30):

I'd also like to study these papers, if there's a group forming - they seem interesting but I've never managed to set aside the time to go through them properly

view this post on Zulip Kenji Maillard (Jun 08 2020 at 10:04):

I really should look into this paper too, in particular I'm wondering what's the connection with Monads with arities and their associated theories by Melliès, Weber and Berger

view this post on Zulip fosco (Jun 08 2020 at 14:50):

As far as I understood, Bourke-Garner's "Monads and theories" and Lucyshyn-Wright's "Enriched algebraic theories" generalise the classical Lawvere-style definition of algebraic theory in two different directions and at different degrees of abstraction.

Both starts with an "arity", i.e. a dense subcategory A\mathcal A of a V-category E\mathcal E, with a functor j:AEj : \mathcal A \hookrightarrow \mathcal E. Just one caveat: [LW] never considers other cases than E=V\mathcal E=\mathcal V.

[BG] defines an adjunction between monads on E\mathcal E and "pretheories", i.e. identity on objects functors p:AopL p : \mathcal A^{op} \to \mathcal L with domain Aop\mathcal A^{op}. This adjunction restricts to an equivalence between "theories", and "nervous monads", i.e. monads on V\mathcal V "whose arity is A\mathcal A" in the sense of Mellies-Weber-Berger.

Theories are pretheories for which all representable functors are "models", in a sense that mimicks Power's treatment of enriched algebraic theories, and Lawvere classical treatment; the condition of being a model for a theory pp is stated in terms of a strict Cat\mathsf{Cat}-enriched pullback, namely

Mod(L)ι[L,V]pVNJ[A,V]\begin{array}{ccc} \text{Mod}(\mathcal L) & \overset{\iota}\to & [\mathcal L, \mathcal V] \\\downarrow && \downarrow p^*\\\mathcal V &\underset{N_J}\to & [\mathcal A,\mathcal V]\end{array}

and a pretheory is a theory if and only if the Yoneda embedding of L\mathcal L factors through ι\iota.

Theories and monads are equivalent simply because they can be characterised as fixed points of the above adjunction PreThMnd{\sf PreTh} \leftrightarrows {\sf Mnd}. Thus, the result is as sharp as it can be, there are no other sensible notions of theory defined through the given arity j:AE j : \mathcal A \hookrightarrow \mathcal E and left outside this characterisation.

view this post on Zulip fosco (Jun 08 2020 at 15:00):

[LW] instead concentrates on the equivalence between algebraic theories and promonads on the domain of the arity; the whole paper builds on the notion of "eleutheric" arity, i.e. an arity j:JVj : \mathcal J \to \mathcal V that exhibits V\mathcal V as the free cocompletion of J\mathcal J under weighted colimits of the form Nj(A)_N_j(A)\star \_. In the terminology of Bourke-Garner, a weight of the form Nj(A)=V(j_,A)N_j(A)=\mathcal V(j\_,A) is called a "jj-nerve", so let's call weighted colimits of the form Nj(A)_N_j(A)\star \_ ... jj-phrenic, mostly for lack of a better name.

Now there is an equivalence between

  1. Theories for an eleutheric arities j:JVj : \mathcal J \to \mathcal V, i.e. an identity on object functor p:JopLp : \mathcal J ^{op}\to \mathcal L that preserves cotensors for objects in J\mathcal J;
  2. promonads t:JJ\mathfrak t : \mathcal J \rightsquigarrow \mathcal J for which there exists a functor T:JVT : \mathcal J \to \mathcal V with the property that tV(j_,T_)\mathfrak t \cong \mathcal V(j\_, T\_);
  3. Monads S:VVS : \mathcal V \to \mathcal V that preserve colimits weighted by jj-phrenic weights.

view this post on Zulip fosco (Jun 08 2020 at 15:16):

It is evident that the two approaches meet in the middle; in familiar cases monads that preserve colimits by jj-phrenic weights are monads with arity, and in the classical case of finitary monads one gets Lawvere theories back as cartesian promonads over cartesian categories, i.e. identity on objects p:JopLp : \mathcal J^{op}\to \mathcal L.

But there is more in this story! And that's why I would like to go deeper in this study.

Lucyshyn-Wright proves the following result:

Suppose that V\mathcal V is cocomplete, and let K\mathcal K be a small V\mathcal V-category. Then we have an isomorphism

MonadsV-Prof(K)K ⁣/V-CAT(Ob(K))\text{Monads}_{\mathcal V\text{-Prof}}(\mathcal K) \cong \mathcal K \!/ \mathcal V\text{-CAT}(Ob(\mathcal K))

between the category of monads on K\mathcal K in V-Prof\mathcal V\text{-Prof} and the coslice category under K\mathcal K in V-CAT(Ob(K))\mathcal V\text{-CAT}(Ob(\mathcal K)). Given an object (A,E:KA)(\mathcal A,E:\mathcal K \rightarrow \mathcal A) of the given coslice category, the associated V\mathcal V-profunctor is A(E,E):KK\mathcal A(E-,E-):\mathcal K \rightsquigarrow \mathcal K.

Here, V-CAT(Ob(K))\mathcal V\text{-CAT}(Ob(\mathcal K)) are identity-on-objects functors out of categories with the same objects as K\mathcal K, and the coslice just keep the domain fixed.

The meat of this construction is that If you start imposing conditions on the idonob functors p:KAp : \mathcal K \to \mathcal A, e.g. preserving limits, a monoidal structure, or else, what you get on the other side of the correspondence is less promonads, more structured the more the requests on pp become structured.

For example, the following conditions are equivalent, if S:CatCatS : {\sf Cat} \to {\sf Cat} is the "free monoid" 2-monad and S~:ProfProf\tilde S : {\sf Prof} \to {\sf Prof} its lifting to profunctors, and p:ABp : {\mathcal A} \to {\mathcal B} is a profunctor between S~\tilde S-algebras.

  1. pp is a pseudo-S~\tilde S-algebra morphism
  2. the induced left adjoint p^:PBPA\hat p : P{\mathcal B} \to P{\mathcal A} between presheaf categories is a pseudo-SS-algebra morphism

(I phrased the statement in order for it to hold for every 2-monad on Cat that has a distributive law with the presheaf construction, i.e. a lifting to the Kleisli bicategory of PP).

Unwinding these definitions, you see that a strong monoidal functor between presheaf categories PA,PBP\mathcal A, P\mathcal B, when these are endowed with certain monoidal structures A,B\otimes_A, \otimes_B, induces a profunctor between the (Cauchy completion of) the domains of said presheaf categories, and such profunctor is a "promonoidal profunctor", i.e. it preserves, in a suitable sense, the promonoidal structures induced on A,B\mathcal A,\mathcal B by restricting A,B\otimes_A, \otimes_B to representables in the well-known way.

Of course, this construction respects representable promonoidal structures: if the promonoidal structure is induced by Day convolution from genuine monoidal structures, the profunctor p^\hat p is strong monoidal if and only if its restriction to representable BPA\mathcal B \to P\mathcal A is monoidal.

view this post on Zulip fosco (Jun 08 2020 at 15:38):

The whole point of this story is that an algebraic theory is usually either a syntax, or a semantics, or a monoid object. For the classical case of Lawvere theories p:FinopLp : \text{Fin}^{op} \to \mathcal L there are equivalences between

  1. Lawvere theories, indeed, i.e. identity on object functors pp that commute with finite products I⨿JI\amalg J in Finop\text{Fin}^{op} to products in L\mathcal L.
  2. Finitary monads T:SetSetT : \text{Set} \to \text{Set}, i.e. monads that commute with 0\aleph_0-filtered colimits.
  3. promonads on Finop\text{Fin}^{op} that are algebras for the representable promonoidal structure induced by the cartesian category structure on Finop\text{Fin}^{op} induced by coproducts.
  4. cartesian operads on [Fin,Set][\text{Fin}, \text{Set}]
  5. monads on [Fin,Set][\text{Fin}, \text{Set}] that commute with colimits and with the convolution product on [Fin,Set][\text{Fin}, \text{Set}] induced by the cartesian structure of Finop\text{Fin}^{op}.
  6. Algebraic categories, obtained as categories of algebras for monads in point 2, or as categories of models for theories of point 1, or as Kleisli categories for monads of point 5, or algebras for operads... well, you see where this is going :D

view this post on Zulip Christian Williams (Jun 08 2020 at 18:55):

Thanks for writing this up! I've been reading through some of Monads and Theories. The distinction between pretheory and theory is somewhat mysterious to me; though I see in Example 8 they give an explanation about "noncanonicity of presentation". How do you think about the this definition of theory?

view this post on Zulip Christian Williams (Jun 08 2020 at 19:01):

It is evident that the two approaches meet in the middle; in familiar cases monads that preserve colimits by jj-phrenic weights are monads with arity.

Can you elaborate on this? Are you saying that a J\mathscr{J}-theory of LW is usually equivalent to a "nervous monad" of BG?

view this post on Zulip Christian Williams (Jun 08 2020 at 19:05):

The example with Day convolution is very interesting. @Nathanael Arkor @vikraman @Younesse Kaddar and I have been talking about generalizing Day convolution from free moncat to other pseudomonads, though that's a conversation for another time.

view this post on Zulip Christian Williams (Jun 08 2020 at 19:06):

In a similar vein, could you elaborate on #3 in your list? That's one that I'm not yet familiar with.

view this post on Zulip Nathanael Arkor (Jun 08 2020 at 22:53):

Thanks for this, @fosco! I'll need to spend a little time digesting. There are many suggestive relationships here and building up a complete picture will take some thought (probably a lot).

view this post on Zulip Ben MacAdam (Jun 08 2020 at 23:36):

Just to chime in, I've found that the eleutheric systems of arities approach works quite well in practice. It's relatively easy to show that most systems of arities you can think of are eleutheric, and if your enriching category is locally presentable it's not too tough to generate an enriched sketch.

view this post on Zulip fosco (Jun 11 2020 at 14:50):

I would be glad to start brainstorming with some/all of you

view this post on Zulip Ben MacAdam (Jun 12 2020 at 17:48):

Christian Williams said:

The example with Day convolution is very interesting. Nathanael Arkor vikraman Younesse Kaddar and I have been talking about generalizing Day convolution from free moncat to other pseudomonads, though that's a conversation for another time.

Would this be about the interaction of Yoneda structures (or more generally an interaction with the hom-functor [,X][-,X] for a suitably nice XX) and pseudo-algebras of a pseudomonad?

view this post on Zulip Nathanael Arkor (Jun 13 2020 at 00:18):

Something like establishing distributive laws for KZ doctrines over an appropriate class of pseudomonads (for some definition of "appropriate"), which would correspond to lifting the KZ doctrines to the 2-categories of pseudoalgebras.

view this post on Zulip Ben MacAdam (Jun 16 2020 at 04:14):

Nathanael Arkor said:

Something like establishing distributive laws for KZ doctrines over an appropriate class of pseudomonads (for some definition of "appropriate"), which would correspond to lifting the KZ doctrines to the 2-categories of pseudoalgebras.

Is this in the same vein as Charles Walker's work on KZ doctrines and pseudomonads (Marmolejo and Wood also did some work in this area)? I would be interested in seeing particular examples of these pseudomonads induced by a enriched Lawvere theories.
Edit: Walkers's paper https://arxiv.org/abs/1706.09575, there's also a reference to Marmolejo and Wood's work in there.

view this post on Zulip Nathanael Arkor (Jun 16 2020 at 11:33):

Yes, the aim is essentially to give a wider range of examples (extending Example 4.3, for instance), to which Walker's results, or Fiore–Gambino–Hyland–Winskel's, could be applied.