Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Somebody named Adam left a comment box a while ago at premonoidal category saying that naturality of the associator requires three naturality squares. I believe that this is true when phrased explicitly in terms of one-variable functors, but the slick approach using the “funny tensor product” allows us to rephrase it as a single natural transformation between functors . I’ve edited the page accordingly. I also added the motivating example (the Kleisli category of a strong monad) and a link to sesquicategory.
There is a comment on the page that “It may be possible to weaken the above make a symmetric monoidal 2-category, in which a monoid object is precisely a premonoidal category”. However, the Power-Robinson paper says that “We remark that is not a 2-functor,” which seems to throw some cold water on the obvious approach to that idea. Was the thought to define a different 2-categorical structure on than the usual one, e.g. using unnatural transformations? It seems that at least one would still have to explicitly require centrality of the coherence isomorphisms.
The page premonoidal category claims
There’s been a lot of discussion of this on the n-Category Café — someone find it and cite it!
But my google-fu is insufficient to find any such discussion. Can someone tell me where to look?
Hehe, yes, I did actually find that tiny mention.
Are you suggesting that maybe whoever wrote that claim at the page premonoidal category was thinking instead of promonoidal categories?
Whoever wrote that claim was Adam again.
Okay, well then maybe I’ll remove it.
(Not that something written by Adam should be any less reliable, just that he seems unlikely to turn up here to explain what he was thinking of.)
I’m pretty sure this Adam is the MO contributor that I interacted with here.
Totally off-topic, but his MO avatar used to be different: a picture of some mathematician or logician perhaps. Anyone remember that, and if so, who it was a picture of? Not knowing was driving me nuts (tried to ask him at MO, but he never replied).
I remember the picture, but never recognised it.
Ah, thanks so much, Sridhar! I get strangely obsessed with mysteries I can’t solve :-)
I added a brief part about how Kleisli catgories of strong monads get premonoidal structure to the idea section (since it is the motivation for the entire concept).
Also, someone (Mike I think) had a remark that the center is maybe adjoint to the inclusion of monoidal categories into premonoidal categories, and this is true using the definition of premonoidal functor given in Power-Robsinson, because premonoidal functors there were required to preserve central morphisms. Whether or not that is the natural definition of premonoidal functor given the definition using the funny tensor product I don’t know.
Whether or not that is the natural definition of premonoidal functor given the definition using the funny tensor product I don’t know.
I don’t see how it could be. Preserving central morphisms is the sort of thing that never follows from preserving “algebraic structure”, since the universal quantifier in the notion of centrality in the codomain ranges over more things than in the domain.
However, that suggests to me another approach to defining premonoidal categories. Consider the 2-category of M-categories, whose morphisms are -functors (preserving tight and loose morphisms), and whose 2-cells are -natural transformations, i.e.\ transformations with tight components that are natural even with respect to loose morphisms. Now if and are -categories, there is an -category whose objects are functors , whose tight morphisms are -natural transformations, and whose loose morphisms are unnatural transformations with loose components that are natural with respect to tight morphisms. If is another -category, an -functor consists of:
The second and third data consist essentially of an extension of the function to -functors for each , such that the bifunctoriality square for in and in commutes if either or is tight.
By general nonsense, there should now be a tensor product of -categories that is left adjoint to , which I believe should make into a symmetric monoidal 2-category. And it seems, though I have not checked the details, that a pseudomonoid in this monoidal 2-category should be (almost?) the same as a non-strict premonoidal category equipped with a specified class of central morphisms (the tight morphisms) that contains the associators and unitors. (In particular, the above description of bimorphisms means that all the tight morphisms are central.)
Note that the main example of Kleisli categories does come equipped with a specified class of central morphisms (those that factor through the unit of the monad).
Has anyone considered putting the Kleisli construction in a purely premonoidal world? That is, define what we mean by a strong monad on a premonoidal category and show that its Kleisli category (suitably defined) is again premonoidal? It seems like a natural thing to do when thinking about composites and transformers of monads. If so, I bet that could be expressed in terms of too.
#12 looks pretty promising to me. IIUC, the -funny tensor product of should be given by the pushout of , similar to the ordinary funny tensor, where is the -cat that has ’s tight morphisms as loose morphisms and tight morphisms.
This seems like a good level of generality to understand presentations of call-by-value languages that explicitly separate values and expressions as the internal language of the sort of generalized multicategory given by the “free cartesian-premonoidal -category” monad on some virtual equipment of -cats, where cartesian-premonoidal means the you have a premonoidal structure on loose morphisms that restricts to cartesian on tight morphisms.
Playing with that a bit it looks like this would axiomatize the 2 different kinds of composition for call-by-value expressions: let-binding which explicitly sequentializes terms (because the premonoidal structure is only functorial in each argument) and substitution of values into expressions. The inclusion of the tight morphisms into loose morphisms relates the 2 and in particular gives you the basic computation rule let x = ret v in t == t[v/x].
Has anyone considered putting the Kleisli construction in a purely premonoidal world?
I haven’t found anything like this.
Hello, Sorry to come late, just to add a couple of points in case it is helpful.
First: I think the original definitions of Freyd category by Power and Thielecke were in terms of premonoidal categories (they are almost just a premonoidal category with a given centre).
Second: as monoidal categories are to multicategories, so premonoidal categories are to “non-commutative” multicategories. By this I mean, when you formulate “multicategory” as Lambek using the circle-i formulation, you have associativity, identity and commutativity laws – drop the commutativity ones. Paul Levy and I called these “premulticategories” in our paper “Universal properties for impure programming languages” (it may have already been known or blindingly obvious).
I could add these sorts of thing to the wiki but I am cautious about adding things which relate directly to my own papers.
I could add these sorts of thing to the wiki but I am cautious about adding things which relate directly to my own papers.
We are small enough of a community that we can afford not to adopt the “neutral point of view” of Wikipedia and instead make good use of available expertise of members of our small community. If you know what you are doing and have something relevant and useful to add to an Lab entry then, by all means, please do add it!
Urs is right; except that I wouldn’t say it has anything to do with the community size, it’s just that the nLab has a different purpose than WP. (Admittedly it might be harder to maintain quality this way with a larger community, but I don’t think if the community got larger we would change our purpose.)
Right. I suppose a small size of a community of contributors means that problematic contributors can be dealt with jointly in a case-by-case basis by informal community action. As we have done a handful of times in the past.
But another aspect that helps us is that, large or small, we are a community in the culture of modern mathematics.
It is hard to over-estimate the immense cultural accomplishment in mathematics, that people have a means to agree on the truth and to appreciate the truth seen by others. Just make a small step out of mathematics into other disciplines, and this ability vanishes rapidly.
This is a key reason why places like Wikipedia don’t allow contrinbutors to contribute their personal insights. In mathematics personal insight is universal, elsewhere personal insight can’t safely be distinguished from personal agenda.
That’s very true. Although even mathematicians have personal agendas about plenty of things just below the level of truth – but there we have the nPOV to guide us.
As you know, I find that ’personal agenda’ aspect very interesting for its not being so readily settled whether one POV supersedes/complements/runs contrary to another. But this is made more interesting as it takes place against a backdrop of ready agreement as to correctness of proof.
Thanks, I have had a go at Freyd categories for now. I think wikipedia is also different because it serves a different purpose, perhaps as an introduction for the lay person, which means that wikipedia should probably follow the prevailing point of view even if that is arguably not the best route for the future (I had plenty of trouble with this a long time ago!)
Nice, thanks! (Link for other readers: Freyd category.)
Of course, a colimit-preserving monad on a presheaf category is the same as a monad in Prof, which is the same as a bijective-on-objects functor. So I guess the point is that the monad is strong iff the functor is a Freyd category?
Thanks, I put a remark at Freyd category to this effect, which also makes a link to the work of Jacobs-Heunen-Hasuo and Asada which is all about profunctors and Freyd categories. What always bothered me about this is that there I don’t know a very nice familiar way to describe the strength of the monad from the profunctor perspective. I mean, a strong cocontinuous monad on a presheaf category is a (what?) monad in Prof. (Not to say you can’t do it, and people have, but just that it is unfamiliar.)
I presumed that the undefined designates the identity-on-objects functor so I stuck it in.
Shouldn’t you be able to define a “strong monad” on a pseudomonoid in any monoidal 2-category?
1 to 31 of 31