Re: String diagrams, adjunction and autonomous categories.

Re: String diagrams, adjunction and autonomous categories.

[André Joyal]

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/ ]

String diagrams, adjunction and autonomous categories.

[John Baez]

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/ ]

Re: String diagrams, adjunction and autonomous categories.

[Peter Selinger]

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/ ]

Re: String diagrams, adjunction and autonomous categories.

[John Baez]

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/ ]

Re: String diagrams, adjunction and autonomous categories.

[Michael Shulman]

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/ ]

Re: String diagrams, adjunction and autonomous categories.

[Dusko Pavlovic]

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/ ]

Re: String diagrams, adjunction and autonomous categories.

[jim stasheff]

   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/ ]

String diagrams, adjunction and autonomous categories.

[David Leduc]

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/ ]

Re: String diagrams, adjunction and autonomous categories.

[Micah Blake McCurdy]

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/ ]