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.
1 to 20 of 20
Does anybody have to hand any examples of closed symmetric monoidal categories in which we have for any objects , , ? I am interested in as much strictness as possible, but feel free to use as much or little as you wish. Any ideas as to what the free such gadget on one object, say, would look like?
In case anybody’s interested, I am ruminating a little on a categorification of the RSA algorithm (or similar), and whether in some such categorification with the property I am asking about, one might naturally be able to construct a ’fully homomorphic’ encryption functor of RSA type.
What is ?
I would be interested in either of the following two situations, and possibly others as well:
1) categories equipped with a closed symmetric monoidal structure (feel free to weaken to non-strict);
2) categories equipped with two monoidal structures and (again, feel free to weaken) such that the former is symmetric and latter is closed, and the latter was the one with respect to which I was defining exponentiation.
The was just because of the symmetry requirement, and to make the analogy with number theory a little more suggestive. I am not assuming any kind of additivity (but feel free to give such examples!).
Probably in case 2) we’d ask for distributivity between the two kinds of monoidal structure. But feel free to play about with the requirements.
Higher/Multiple categories, or any other kind of models for this kind of syntax, are equally welcome :-).
Well, one class of examples is if is the cartesian product, and is arbitrary and closed. Then arguing representably we have
so that by the Yoneda lemma. I can’t think of any other examples offhand.
Thanks very much, Mike, this looks very promising. I will continue thinking about it, as I am still doing about the question about factorisation that I asked about a little earlier.
On a different note, and just out of curiosity, does anybody happen to know what the free cartesian closed (or (symmetric/braided) monoidal closed) category on one object is? If one drops the closedness, the answer is well known in all of these cases.
does anybody happen to know what the free cartesian closed (or (symmetric/braided) monoidal closed) category on one object is?
Both are a bit complicated, but the free symmetric monoidal closed category on one object was essentially the subject of my thesis. The problem of deciding equality of morphisms (“the coherence problem” for this doctrine) can be solved by using proof nets augmented by certain edges for units, subject to a strong and confluent normalization algorithm expressed in terms of “directed rewirings”.
My thesis is unpublished, but you can get an idea of this for the case of the free -autonomous category on one object by looking at the paper by Blute-Cockett-Seely-Trimble, where the language of rewirings is used. I am happy to explain further here, including what I mean by “directed rewirings” (which are unavailable for the -autonomous case).
As for the doctrine of cartesian closed categories, Jim Dolan and I once gave a description in terms of what he called “holodeck games”. John Baez gave an informal description of this here, and I wrote up something more formal which John has archived here. I haven’t thought about them much since that time. Some other people who I think may have studied this problem are Dominic Hughes, Robin Houston, and Djordje Cubric (not sure of the spelling of the last), and maybe Martin Hyland as well. Dominic warned me that we (Jim and I) would have a hard time describing composition of morphisms in the holodeck games representation.
Thank you very much, Todd, this looks most interesting. For the moment, it is a little bit away from things I am directly thinking about, so I am probably not the best person to ask you for details, but I hope someone else does so!
I have a quick question: what is a quick way to see that a free category of this kind even exists? Cartesian closed or (symmetric/braided/unsymmetric) monoidal categories can certainly be described algebraically, so one will have a free construction on a directed graph. But this is not the free construction that we are discussing. I am guessing that some kind of 2-monadic stuff can be used, but I’d be interested in seeing how this can be carefully justified.
I would be especially interested in the analogue of the theorems Todd referred to for the braided monoidal case. It would be fascinating to know whether the connection to knot theory remains in the closed setting, and if so, what that connection is.
I don’t understand; isn’t the free category of some sort on one object the same as the free one on the directed graph with one vertex and no edges?
Let us take a concrete example. The free braided monoidal category on one object is, as it happens, also the free strict braided monoidal category on one object. The latter notion is, I agree with you, the same as the free one on the directed graph you mention. However, I do not think the universal property of the latter construction gives an explanation for why the free strict braided monoidal category on one object is in fact also the free (not necessarily strict) braided monoidal category on one object; I think that one will need to make use of some 2-categorical notion of an algebraic theory, such as a 2-monad, to explain this. Do you not agree?
Non-strict braided monoidal categories are also algebraic over directed graphs, so they have free objects as well for the same reasons. The free non-strict braided monoidal category is not isomorphic to the free strict braided monoidal category, but they are equivalent, which is essentially the (nontrivial) coherence theorem for braided monoidal categories. Can you say explicitly and precisely what universal property you are interested in?
The universal property of the free braided monoidal category on one object that I am thinking of is: take any braided monoidal category , then there is an equivalence of categories between the category of braided monoidal functors from to sending to , where is the unit of .
It is not actually clear to me that (not necessarily strict) braided monoidal categories are algebraic over directed graphs. Certainly as objects braided monoidal categories can be described by a finite limit sketch. But the arrows of the category of models look incorrect to me.
Even if this sketch does in fact give the correct category of models, it is not at all clear to me what the free such object looks like, and it is not at all clear to me that it is actually a useful object. In particular, I don’t see how it can possibly take into account the 2-categorical layer of the universal property I described; hence why I keep mentioning 2-theories :-).
Yes, the morphisms that you’ll get from considering braided monoidal categories as algebraic over directed graphs are strict braided monoidal functors.
Here is one way to construct free braided monoidal categories with a 2-categorical universal property with respect to non-strict functors. Give a presentation of a 2-monad on with generators and relations that describe exactly the structure of a (non-strict) braided monoidal category. A description of how to give presentations of 2-monads is in this paper. Then identify the pseudo -morphisms with ordinary non-strict braided monoidal functors; this is not immediately obvious since they are unbiased while the usual ones are biased, but you can use the technique of mapping into special monads described in Steve’s paper, or else Bourke’s monadicity theorem for pseudo morphisms. Finally, Blackwell-Kelly-Power proved that for any accessible 2-monad on a complete and cocomplete 2-category , the strictly free algebras , which have the strict universal property with respect to strict maps , are also weakly free with respect to pseudo morphisms .
These kind of details would be worth recording at the nLab.
Thanks Mike, lots of interesting stuff there. A lot of it I was aware of, but even though I have dipped into Lack’s paper many times, I had not fully appreciated the way to construct presentations of 2-monads.
I find myself speculating whether there is some mechanical way that the 2-category of braided monoidal categories can be seen to be ’algebraic’. Could one imagine for instance an algorithm for going from a sketch of a strict algebraic structure to some presentation of a 2-monad that captures the weak one? I know that this is an old idea. In particular, I believe that Barwick had some ideas around something similar, but I’m not sure they got/have got far.
Well, a strict structure doesn’t determine the weak one strictly: you can weaken strict monoidal categories in the usual biased nullary+binary way, or in a totally unbiased way, or lots of different ways in between. The most “canonical” of these is the totally unbiased, and for those there is a mechanical procedure: just consider pseudo-algebras for the same 2-monad. Since accessible 2-monads are themselves the algebras for a 2-monad, and pseudo-algebras for a 2-monad are particular pseudo-morphisms of 2-monads out of it, the pseudo-morphism-classifier for a 2-monad has the property that pseudo -algebras coincide with strict -algebras. So unbiased pseudo-algebras for a 2-monad are the strict algebras for a different 2-monad, hence equally algebraic.
a strict structure doesn’t determine the weak one strictly
Indeed, good point! I would be satisfied with any reasonable weak notion, as long as it can be produced mechanically.
The most “canonical” of these is the totally unbiased
I do think that unbiased structures are very important, and under-appreciated.
for those there is a mechanical procedure: just consider pseudo-algebras for the same 2-monad.
I was mainly thinking about going from the kind of definition which one usually writes down to a 2-monad. I guess this is more or less algorithmic, but there might nevertheless be some interesting questions. Can one for instance tell ’at a glance’ (i.e. ’type-check it’) whether or not a given definition is algebraic? Can we formulate ’coherence condition’ in a precise way?
I was also thinking about an algorithm which one could crank up in higher dimensions. So begin with the axioms for a monoid (in ). Interpret it in to get the notion of a strict monoidal category. Crank the machine to get the usual weak notion. In the commutative case, it might crank out all flavours of ’commutative’ monoidal category. Interpret in to get the notion of a fully strict monoidal 2-category. Crank the machine to get all the flavours of weak notions. Etc. Keep going and going.
I realise that this seems at least as hard as defining, say, weak -categories. But maybe it gives a little bit of a different angle on the question; in particular, there are a plethora of lower dimensional examples which any algorithm could be tested against.
I also think that this might have something to do with being able to work with -categories effectively. Nobody really wants to work with coherence conditions explicitly!
But thanks very much for your further thoughts, which are definitely very important to keep in mind.
Can one for instance tell ’at a glance’ (i.e. ’type-check it’) whether or not a given definition is algebraic?
I don’t know whether there is a type-checking algorithm that will check all possible algebraic (i.e. monadic) definitions (e.g. compact hausdorff spaces?), but if you have something definable by an operad or Lawvere theory then certainly yes: just read the operations and equations as generators and relations for the operad. And once you have an operad in , just interpret it as an operad in or to get a categorified version for which you can talk about pseudo-algebras.
Interesting! I’m not quite sure that one can get more than one level of weakness this way though. Pseudo-algebras on a monad interpreted in will not be able to capture the fully weak notions of monoidal 2-category, I would think? Probably one would need some kind of weak algebras for a 3-monad, but, apart from the obvious difficulty of even defining these reasonably, I don’t know if there is a mechanical way to progressively weaken from strict to weak to even weaker. This was the kind of thing I was speculating about; some kind of machine for generating coherence conditions. In other words, even if it is extraordinarily tedious to write them down explicitly, it would be nice if there were an algorithm which told us in principle what to do.
It actually seems do-able to me. That is to say, it does seem do-able to me to give a computer some (small amount of) initial data from which it could re-produce the existing definitions of a fully weak 3-category or 4-category for instance. What do others think?
Well, an -space, which is a fully weak monoidal -groupoid, is the same as a pseudo-algebra for the same nonsymmetric operad in whose algebras in are ordinary monoids. So I don’t see any reason to disbelieve that in some contexts at least the appropriate kind of pseudoalgebra gives you the right weakening.
1 to 20 of 20