String diagrams, adjunction and autonomous categories.
As shown by Baez, in an autonomous category the isomorphism hom(A (X) B, C) = hom (B, A -o C), when drawn as a string diagram, is like the bending of the input wire A to make it an output. Now one can also draw string diagrams to represent the zigzag equations between the adjoint pair of functors _ (X) B and B -o _. How does the latter diagram relate to the former one? [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Hallo! In an autonomous category, the functor B -o _ is "representable" in the sense that it can be written as B* (x) _ for some object B*. If k is the unit for (x), then there are maps "unit" : k ----> B* (x) B and "counit" : B (x) B* ---> k which satisfy triangle identities, usually written graphically as zig-zags which equal identities. The isomorphism you mention in your first paragraph is obtained by appending the unit for A. So, the bends in the wires are the same in both paragraphs. Incidentally, although I'm not sure that I'm familiar with the work of Baez to which you refer, I would imagine that the use of string diagrams to describe units and counits in an autonomous category is considerably older, at least as far back as "Planar Diagrams and Tensor Algebra" by Joyal and Street (available on the website of the latter) from 1988. Cheers, Micah On Sun, Aug 29, 2010 at 2:48 AM, David Leduc <david.leduc6@googlemail.com>wrote:
As shown by Baez, in an autonomous category the isomorphism hom(A (X) B, C) = hom (B, A -o C), when drawn as a string diagram, is like the bending of the input wire A to make it an output.
Now one can also draw string diagrams to represent the zigzag equations between the adjoint pair of functors _ (X) B and B -o _.
How does the latter diagram relate to the former one?
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Micah wrote: Incidentally, although I'm not sure that I'm familiar with the work of Baez
to which you refer, I would imagine that the use of string diagrams to describe units and counits in an autonomous category is considerably older, at least as far back as "Planar Diagrams and Tensor Algebra" by Joyal and Street (available on the website of the latter) from 1988.
He was probably talking about these popularizations: A prehistory of n-categorical physics, with Aaron Lauda http://arxiv.org/abs/0908.2469 Physics, logic, computation and topology: a Rosetta stone, with Mike Stay http://arxiv.org/abs/0903.0340 which cite the work of Joyal and Street, though sadly not the paper you mention. Best, jb [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
On the other hand, am I right that you (John) have also written about string diagrams in closed (non-autonomous) monoidal categories? Those are a bit subtler, and I don't recall them in the work of Joyal and Street (am I wrong?). The original question used the word "autonomous" but the notation used suggested a merely closed monoidal category, so perhaps that's what he had in mind. Mike On Mon, Aug 30, 2010 at 10:06 PM, John Baez <baez@math.ucr.edu> wrote:
Micah wrote:
Incidentally, although I'm not sure that I'm familiar with the work of Baez
to which you refer, I would imagine that the use of string diagrams to describe units and counits in an autonomous category is considerably older, at least as far back as "Planar Diagrams and Tensor Algebra" by Joyal and Street (available on the website of the latter) from 1988.
He was probably talking about these popularizations:
A prehistory of n-categorical physics, with Aaron Lauda http://arxiv.org/abs/0908.2469
Physics, logic, computation and topology: a Rosetta stone, with Mike Stay http://arxiv.org/abs/0903.0340
which cite the work of Joyal and Street, though sadly not the paper you mention.
Best, jb
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Mike Shulman wrote: On the other hand, am I right that you (John) have also written about
string diagrams in closed (non-autonomous) monoidal categories?
Right.
Those are a bit subtler, and I don't recall them in the work of Joyal and Street (am I wrong?).
I think you're right - they're subtler, and I haven't seen anyone else using them. I never proved any *theorems* about them. But I used them extensively in my course on "Classical versus quantum computation", starting here: http://math.ucr.edu/home/baez/qg-fall2006/index.html#computation I wanted to explain how beta-reduction in the lambda calculus is like "straightening a zig-zag". There's a quick summary of this material in that "Rosetta Stone" paper with Mike Stay, mentioned earlier: http://arxiv.org/abs/0903.0340
The original question used the word "autonomous" but the notation used suggested a merely closed monoidal category, so perhaps that's what he had in mind.
Oh, okay. Yeah, I was sort of disappointed that Micah credited me for string diagrams in the autonomous case, where I didn't invent them, instead of the closed case, where maybe I did. Best, jb [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
I agree that string diagrams for closed monoidal categories are quite a bit subtler than those for autonomous categories. Of course, because of the forgetful functor from autonomous categories to closed monoidal categories, there's a unique functor from the free closed monoidal category (over some generators) to the free autonomous category (over the same generators), i.e., string diagrams. So one can say, without doing any technical work, that morphisms of the free closed monoidal category are "certain" string diagrams, possibly with additional structure. The technical questions then are: which diagrams are "certain" ones (i.e., what's the image of this functor), and what, if anything, is the additional structure? One obvious piece of extra structure is that there are two binary connectives instead of one, namely, tensor and '-o'. In the Rosetta Stone paper (p.30), Baez and Stay use "clasps" to bind two strings together, to indicate an object A -o B. I am not sure how this will work for nested operations, such as (((A tensor B) -o C) tensor D) -o ((E -o F) tensor G). As John has already pointed out, the paper does not give details or theorems. On the other hand, the question of such string diagrams has been very extensively studied by logicians under the name "proof nets for linear logic". It turns out that one usually needs a condition logicians call a "correctness criterion" (originally invented by Girard) to identify the string diagrams that actually correspond to legal morphisms. Alternatively, it is possible to just draw a box around every operation (as done by Baez and Stay), and say that the legal diagrams are those built up using the operations of closed monoidal categories. But that is really just a graphical way of displaying the original term, together with its forgetful image in string diagrams. Most work on proof nets is for classical linear logic (corresponding to *-autonomous categories). Looking for the case of closed monoidal categories only, we need to look for intuitionistic linear logic. By googling "proof nets for intuitionistic linear logic", I found this 2008 paper by Lamarche (based on a 1994 technical report), which seems to contain the answer, with theorems: http://hal.inria.fr/docs/00/34/73/36/PDF/prfnet1.pdf That paper actually contains a bit more than just the monoidal closed case; it also shows how to extend the diagrams to cartesian product (in addition to tensor), and it adds the exponential operator "!" of linear logic, in the presence of which one can then have diagrams for *cartesian* closed categories as well. I think an even earlier version of such string diagrams may already appear in Regnier's 1992 thesis (http://iml.univ-mrs.fr/~regnier/articles/these.ps.gz). So I guess the point is that one can save some time by exploiting what logicians have already done, using the connections between logic, category theory, and string diagrams, rather than re-inventing the wheel. Which is also precisely the point of the Baez/Stay "Rosetta Stone" paper. -- Peter John Baez wrote:
Mike Shulman wrote:
On the other hand, am I right that you (John) have also written about
string diagrams in closed (non-autonomous) monoidal categories?
Right.
Those are a bit subtler, and I don't recall them in the work of Joyal and Street (am I wrong?).
I think you're right - they're subtler, and I haven't seen anyone else using them. I never proved any *theorems* about them. But I used them extensively in my course on "Classical versus quantum computation", starting here:
http://math.ucr.edu/home/baez/qg-fall2006/index.html#computation
I wanted to explain how beta-reduction in the lambda calculus is like "straightening a zig-zag".
There's a quick summary of this material in that "Rosetta Stone" paper with Mike Stay, mentioned earlier:
http://arxiv.org/abs/0903.0340
The original question used the word "autonomous" but the notation used suggested a merely closed monoidal category, so perhaps that's what he had in mind.
Oh, okay. Yeah, I was sort of disappointed that Micah credited me for string diagrams in the autonomous case, where I didn't invent them, instead of the closed case, where maybe I did.
Best, jb
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Dear Peter, If I recall it right, string diagrams were first introduced by Kelly and MacLane as a visual device for analysing the structure of the arrows of a free monoidal closed category. The device was not perfect but was giving some real insights. Max Kelly showed later that it was a complete description in the compact case. I believe that Penrose was inspired by Feynman's diagrams when he introduced his graphical tensor calculus (sometimes later). I have first learned about Penrose's diagram from Max, in the late 70's. One of the best way to learn something is to reinvent it. Mathematics need to be constantly reinvented to stay alive and prosper. Every new generation is reinventing mathematics. Category theorists are permanently reinventing mathematics. I guess we also need to remember the past. Best, andre Le 10-09-05 à 22:05, Peter Selinger a écrit :
I agree that string diagrams for closed monoidal categories are quite a bit subtler than those for autonomous categories.
Of course, because of the forgetful functor from autonomous categories to closed monoidal categories, there's a unique functor from the free closed monoidal category (over some generators) to the free autonomous category (over the same generators), i.e., string diagrams. So one can say, without doing any technical work, that morphisms of the free closed monoidal category are "certain" string diagrams, possibly with additional structure.
The technical questions then are: which diagrams are "certain" ones (i.e., what's the image of this functor), and what, if anything, is the additional structure? One obvious piece of extra structure is that there are two binary connectives instead of one, namely, tensor and '-o'. In the Rosetta Stone paper (p.30), Baez and Stay use "clasps" to bind two strings together, to indicate an object A -o B. I am not sure how this will work for nested operations, such as (((A tensor B) -o C) tensor D) -o ((E -o F) tensor G). As John has already pointed out, the paper does not give details or theorems.
On the other hand, the question of such string diagrams has been very extensively studied by logicians under the name "proof nets for linear logic". It turns out that one usually needs a condition logicians call a "correctness criterion" (originally invented by Girard) to identify the string diagrams that actually correspond to legal morphisms. Alternatively, it is possible to just draw a box around every operation (as done by Baez and Stay), and say that the legal diagrams are those built up using the operations of closed monoidal categories. But that is really just a graphical way of displaying the original term, together with its forgetful image in string diagrams.
Most work on proof nets is for classical linear logic (corresponding to *-autonomous categories). Looking for the case of closed monoidal categories only, we need to look for intuitionistic linear logic. By googling "proof nets for intuitionistic linear logic", I found this 2008 paper by Lamarche (based on a 1994 technical report), which seems to contain the answer, with theorems:
http://hal.inria.fr/docs/00/34/73/36/PDF/prfnet1.pdf
That paper actually contains a bit more than just the monoidal closed case; it also shows how to extend the diagrams to cartesian product (in addition to tensor), and it adds the exponential operator "!" of linear logic, in the presence of which one can then have diagrams for *cartesian* closed categories as well. I think an even earlier version of such string diagrams may already appear in Regnier's 1992 thesis (http://iml.univ-mrs.fr/~regnier/articles/these.ps.gz).
So I guess the point is that one can save some time by exploiting what logicians have already done, using the connections between logic, category theory, and string diagrams, rather than re-inventing the wheel. Which is also precisely the point of the Baez/Stay "Rosetta Stone" paper.
-- Peter
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Dear Peter, If I recall it right, string diagrams were first introduced by Kelly and MacLane as a visual device for analysing the structure of the arrows of a free monoidal closed category. The device was not perfect but was giving some real insights. Max Kelly showed later that it was a complete description in the compact case. I believe that Penrose was inspired by Feynman's diagrams when he introduced his graphical tensor calculus (sometimes later). I have first learned about Penrose's diagram from Max, in the late 70's. One of the best way to learn something is to reinvent it. Mathematics need to be constantly reinvented to stay alive and prosper. Every new generation is reinventing mathematics. Category theorists are permanently reinventing mathematics. I guess we also need to remember the past. Best, andre Le 10-09-05 à 22:05, Peter Selinger a écrit :
I agree that string diagrams for closed monoidal categories are quite a bit subtler than those for autonomous categories.
Of course, because of the forgetful functor from autonomous categories to closed monoidal categories, there's a unique functor from the free closed monoidal category (over some generators) to the free autonomous category (over the same generators), i.e., string diagrams. So one can say, without doing any technical work, that morphisms of the free closed monoidal category are "certain" string diagrams, possibly with additional structure.
The technical questions then are: which diagrams are "certain" ones (i.e., what's the image of this functor), and what, if anything, is the additional structure? One obvious piece of extra structure is that there are two binary connectives instead of one, namely, tensor and '-o'. In the Rosetta Stone paper (p.30), Baez and Stay use "clasps" to bind two strings together, to indicate an object A -o B. I am not sure how this will work for nested operations, such as (((A tensor B) -o C) tensor D) -o ((E -o F) tensor G). As John has already pointed out, the paper does not give details or theorems.
On the other hand, the question of such string diagrams has been very extensively studied by logicians under the name "proof nets for linear logic". It turns out that one usually needs a condition logicians call a "correctness criterion" (originally invented by Girard) to identify the string diagrams that actually correspond to legal morphisms. Alternatively, it is possible to just draw a box around every operation (as done by Baez and Stay), and say that the legal diagrams are those built up using the operations of closed monoidal categories. But that is really just a graphical way of displaying the original term, together with its forgetful image in string diagrams.
Most work on proof nets is for classical linear logic (corresponding to *-autonomous categories). Looking for the case of closed monoidal categories only, we need to look for intuitionistic linear logic. By googling "proof nets for intuitionistic linear logic", I found this 2008 paper by Lamarche (based on a 1994 technical report), which seems to contain the answer, with theorems:
http://hal.inria.fr/docs/00/34/73/36/PDF/prfnet1.pdf
That paper actually contains a bit more than just the monoidal closed case; it also shows how to extend the diagrams to cartesian product (in addition to tensor), and it adds the exponential operator "!" of linear logic, in the presence of which one can then have diagrams for *cartesian* closed categories as well. I think an even earlier version of such string diagrams may already appear in Regnier's 1992 thesis (http://iml.univ-mrs.fr/~regnier/articles/these.ps.gz).
So I guess the point is that one can save some time by exploiting what logicians have already done, using the connections between logic, category theory, and string diagrams, rather than re-inventing the wheel. Which is also precisely the point of the Baez/Stay "Rosetta Stone" paper.
-- Peter
John Baez wrote:
Mike Shulman wrote:
On the other hand, am I right that you (John) have also written about
string diagrams in closed (non-autonomous) monoidal categories?
Right.
Those are a bit subtler, and I don't recall them in the work of Joyal and Street (am I wrong?).
I think you're right - they're subtler, and I haven't seen anyone else using them. I never proved any *theorems* about them. But I used them extensively in my course on "Classical versus quantum computation", starting here:
http://math.ucr.edu/home/baez/qg-fall2006/index.html#computation
I wanted to explain how beta-reduction in the lambda calculus is like "straightening a zig-zag".
There's a quick summary of this material in that "Rosetta Stone" paper with Mike Stay, mentioned earlier:
http://arxiv.org/abs/0903.0340
The original question used the word "autonomous" but the notation used suggested a merely closed monoidal category, so perhaps that's what he had in mind.
Oh, okay. Yeah, I was sort of disappointed that Micah credited me for string diagrams in the autonomous case, where I didn't invent them, instead of the closed case, where maybe I did.
Best, jb
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
On Thu, 2 Sep 2010, Michael Shulman wrote:
On the other hand, am I right that you (John) have also written about string diagrams in closed (non-autonomous) monoidal categories? Those are a bit subtler, and I don't recall them in the work of Joyal and Street (am I wrong?).
speaking of coherence in closed categories, i was always under the impression that kelly and maclane, while writing their 1971 JPAA paper, and the later one (1979?) secretly drew string diagrams on the side, and then translated them into categorical diagrams. at least for counterexamples, this works. and in the kelly-laplaza paper about compact/autonomous categories: the free construction is expressed in terms of strings, but i guess at the time it was easier to describe them in words, than to wait for the publisher to typeset your stings for you. maybe i am projecting back. or maybe category theory has grown so old that some things are easier to reconstruct than to remember :) -- dusko [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
On 9/3/10 9:38 PM, Dusko Pavlovic
speaking of coherence in closed categories, i was always under the impression that kelly and maclane, while writing their 1971 JPAA paper, and the later one (1979?) secretly drew string diagrams on the side, and then translated them into categorical diagrams. at least for counterexamples, this works. and in the kelly-laplaza paper about compact/autonomous categories: the free construction is expressed in terms of strings, but i guess at the time it was easier to describe them in words, than to wait for the publisher to typeset your stings for you.
In the earlier 60s, it wasn't conceivable to include even tree diagrams in anything to be published hence my inidicial approach to the formulas for A_\infty structures jim [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
participants (8)
-
André Joyal -
David Leduc -
Dusko Pavlovic -
jim stasheff -
John Baez -
Micah Blake McCurdy -
Michael Shulman -
selinger＠mathstat.dal.ca