Theorems Into Coffee

May 4, 2008

Posted by John Baez

$MathML-enabled post (click for more details).$

As the famous quote goes, “a mathematician is a machine for turning coffee into theorems”. But every chemical reaction is reversible, at least under the right conditions. So, there’s got to be some way turn theorems into coffee!

And now you can do it here.

$MathML-enabled post (click for more details).$

I haven’t quite worked out the details. I’d like to harness your competitive spirit and yearning for coffee, but also the marvelous cooperative spirit of this blog. I’m not sure how yet, but let’s just dive in and see how it goes.

I’ll send a $15 Starbucks gift certificate to anybody who gives me, in LaTeX, a well-written rigorous proof of the following theorem:

Let $Mat(\mathbb{N})$ be the category whose objects are natural numbers and whose morphisms $f : n \to m$ are $m \times n$ matrices of natural numbers, with composition being given by matrix multiplication. Think of $Mat(\mathbb{N})$ as a symmetric monoidal category in the obvious way where the tensor product of objects $n$ and $m$ is $n + m$ , and the tensor product of morphisms is direct sum of matrices.

Theorem: $Mat(\mathbb{N})$ is the PROP for bicommutative bialgebras.

More explanations: a symmetric monoidal category whose objects are just natural numbers, with addition as the tensor product of objects, is called a PROP. We can talk about the models (also known as ‘algebras’ ) of a PROP in any symmetric monoidal category $C$ . I’m claiming that the category of models of $Math(\mathbb{N})$ in $C$ is equivalent to the usual category of ‘bicommutative bialgebras’ in $C$ . You might prefer to call these ‘bicommutative bimonoids’ in $C$ : they’re commutative monoid objects that are also cocommutative comonoid objects, where the monoid operations are required to be comonoid homomorphisms. (Or, equivalently: the comonoid operations are required to be a monoid homomorphisms!)

I haven’t worked out what I’ll do if I get multiple responses, or responses that don’t quite satisfy me. For now, let me say I’ll give the coffee to the first person who gives me a satisfactory proof in LaTeX. Posting a link on this blog is best; if you can’t manage that, send it via email.

But in fact, I have a bunch of theorems I’d like proved, and I’d like to evolve a system where groups of people could collaborate to prove them and jointly receive a reward. That seems a lot more fun than a kind of race to be first. But I don’t know to organize it — suggestions?

I haven’t fully worked out the issue of credit and publishing rights, but let’s say this. If you collect the gift certificate, that means you give me the right to use your LaTeX source code in future work — for example, an expository paper, wiki, or book on higher-dimensional algebra. But I will certainly credit you, and I’ll certainly let you publish this work elsewhere.

Of course, the last part only matters much if the “Theorems into Coffee” idea catches on — the above theorem is just one of a collection of similar results, and they’re probably more publishable en masse than one at a time.

I haven’t worked out what I’ll do if someone posts a reference to an existing proof of the theorem. Let’s say for now that I’ll give you the same reward regardless of whether the theorem has been proved, if you write up a self-contained clear proof.

I also haven’t worked out what to do if someone outside the US collects the award — for example, Robin Houston or Tom Leinster or Eugenia Cheng. The Starbucks card system I know seems designed to work best inside the US… but I haven’t even tried it yet. Let’s say this: if it turns out to be a nuisance to send you a Starbucks card, or you don’t want a Starbucks card, I’ll send you a check for $15. Or, if I bump into you during my travels this summer, I’ll be glad to pay you the approximate equivalent in local currency.

(Frankly the check option looks simpler than the Starbucks card; you just need to promise to spend it on coffee. Or tea, if you’re a wimp. Something that helps you do math, anyway!)

There are probably lots of other things I haven’t worked out.

But for starters, let’s see if anybody tackles this theorem.

Posted at May 4, 2008 11:48 PM UTC

TrackBack URL for this Entry: https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/1670

16 Comments & 3 Trackbacks

Re: Theorems Into Coffee

If a Mathematician is a machine for turning coffee into theorems, then isn’t a co-mathematician a co-machine for turning theorems into ffee?

Posted by: Jonathan Vos Post on May 5, 2008 6:07 AM | Permalink | Reply to this

Re: Theorems Into Coffee

You’re almost right — except for one slip: it’s not theorems that they turn into into ffee; it’s cotheorems. A cotheorem is like a theorem except you start from the conclusions and reason backwards until you prove the assumptions.

A statement that easily leads to the proof of a cotheorem is called a ‘rollary’.

Posted by: John Baez on May 5, 2008 8:14 AM | Permalink | Reply to this

Re: Theorems Into Coffee

I think there’s a hidden assumption here that cocoffee is isomorphic to ffee. That may be true for finite dimensional coffee but what about the infinite dimensional case?

Posted by: Dan Piponi on May 5, 2008 6:02 PM | Permalink | Reply to this

Hilbert Coffee; Re: Theorems Into Coffee

Hilbert coffee is a coffee vector space H with an inner product (f,g) such that the norm defined by

|f|=sqrt((f,f))

turns H into a coffee complete metric space.

This is not to be confused with Adam Gussow and Charlie Hilbert - “Coffee Break” (2000). Not to be confused with Hilbert Uniformization of Moduli Space | The String Coffee Table.

I would have to tap into my transfinite bank account to buy infinite dimensional coffee.

Oh, and it is possible to buy a ceramic coffee mug emphasing the Hilbert family crest.

Posted by: Jonathan Vos Post on May 5, 2008 10:39 PM | Permalink | Reply to this

Re: Theorems Into Coffee

Would the co-converse of a co-theorem be the nverse? And something falsifying a co-conjecture be a unterexample?

Posted by: Kerry Soileau on September 2, 2008 4:32 AM | Permalink | Reply to this

Re: Theorems Into Coffee

I am writing this over a cup (well, a bucket) of morning coffee. There are no Starbuck’s in Slovenia, thank god, so I do not need the gift certificate for the following non-answer.

The category you are describing is just the category (in the sense of Lawvere’s functorial semantics of equational theories) which you get if you consider the theory of a commutative semiring with unit (no subtraction) and form the syntactic category out of it. The symmetric monoidal structure is given by products. The product-preserving functors into a category with products correspond to models, which are precisely commutative semirings with unit. I do not know at the moment what happens if we map by a strict monoidal functor, though. Presumably something similar.

We should figure out whether I am talking abot the same thing as you are. A good question is this: this tensor product m+n, it has projections too, does it not? So the symmetric monoidal structure is actually given by the categorical products.

Posted by: Andrej Bauer on May 5, 2008 6:30 AM | Permalink | Reply to this

Re: Theorems Into Coffee

$MathML-enabled post (click for more details).$

Andrej wrote:

I am writing this over a cup (well, a bucket) of morning coffee. There are no Starbuck’s in Slovenia, thank god, so I do not need the gift certificate for the following non-answer.

The singular is Starbucks and the plural is presumably Starbucki. The lack of Starbucki in Slovenia suggests that this country has not yet fallen under American domination, perhaps because our president was not yet informed about it.

Enjoy this while it lasts!

We should figure out whether I am talking about the same thing as you are.

Yes, we should. But I’m a little tired right now, as you can see from my dazed, silly reply above. So, my answer will be brief and possibly wrong.

We should figure out whether I am talking about the same thing as you are. A good question is this: this tensor product $m+n$ , it has projections too, does it not? So the symmetric monoidal structure is actually given by the categorical products.

That sounds right. The symmetrical monoidal category $Mat(\mathbb{N})$ is just a skeleton of the symmetric monoidal category of finitely generated free $\mathbb{N}$ -modules. Indeed, this sentence should remain true if we replace $\mathbb{N}$ by any commutative rig $R$ . (A ‘rig’ is what you’re calling a ‘semiring with unit’.)

This is gives a more conceptual way of thinking about $Mat(\mathbb{N})$ . The natural number $n$ corresponds to the free module $\mathbb{N}^n$ . The tensor product $m + n$ corresponds to $\mathbb{N}^n \oplus \mathbb{N}^m$ . So, unless I’m too tired, this is both the categorical product and categorical coproduct.

So, we can think of $Mat(\mathbb{N})$ either as a Lawvere theory or as a PROP. However, its algebras as a PROP should be the bicommutative bimonoids, while its algebras as Lawvere theory should be the commutative monoids.

Here I’m using some stuff about the adjunction between Lawvere theories and PROPs — see pages 51-59 in these notes.

If you ever decide to prove theorems for coffee I will be glad to pay you in worthless American dollars rather than Starbucks gift certificates.

Posted by: John Baez on May 5, 2008 8:08 AM | Permalink | Reply to this

Re: Theorems Into Coffee

“Eats, leaves and shoots”
a book worth reaidng ;-)

jim

Posted by: jim stasheff on May 5, 2008 1:06 PM | Permalink | Reply to this

Re: Theorems Into Coffee

I haven’t encountered that book before; is it about pandas?

Posted by: Andrew Stacey on May 5, 2008 3:20 PM | Permalink | Reply to this

Re: Theorems Into Coffee

$MathML-enabled post (click for more details).$

Jim, I guess you mean Eats, Shoots & Leaves, Lynne Truss’s book on punctuation.

Posted by: Simon Willerton on May 5, 2008 4:42 PM | Permalink | Reply to this

Re: Theorems Into Coffee

$MathML-enabled post (click for more details).$

Yes, it’s called “Eats, Shoots and Leaves” — a title showing how a misplaced comma can change a peaceful panda into a tough customer out of a nasty cowboy movie.

I found the rest of the book a bit anticlimactic after that title.

Posted by: John Baez on May 5, 2008 8:53 PM | Permalink | Reply to this

Re: Theorems Into Coffee

Your table of contents on HDA does not have a section on symmetric moniodal 2-categories. I’d like to have a go at writing a bit about this. I will be including some of it in a book on sphere eversions that I am working on, but the subject is a stand alone. Also since immersed surfaces are easier to understand than knotted surfaces, such a description might be helpful as an intro the the section by you and Laurel.

Rather than a full commitment, I will send JB the text if and when it is finished. We can work out copyright issues later —which is to say that I want to keep the rights, AND I also want to allow the material to be used
as freely as possible.

All: please spare me the lecture about copylefting.

Posted by: Scott Carter on May 5, 2008 12:50 PM | Permalink | Reply to this

Re: Theorems Into Coffee

$MathML-enabled post (click for more details).$

Sounds like an interesting idea!

Work on this book of mine has proceeded at a glacial pace. In fact, in these days of global warming, I only wish glaciers moved so slow.

I’ve almost given up hope that I’ll ever write it… but my latest plan is to write it on the forthcoming $n$ -category wiki, so other people can help out.

Unfortunately getting this wiki started has been very slow as well, due to technical difficulties. Feeling too incompetent to set it up myself, I’ve been relying on someone else — and since we’re both busy doing other things, it usually takes a month for each problem to get solved. It still doesn’t work, at least not for me.

When it finally does work, we should be able to write in it using LaTeX, and then reuse that LaTeX source code for papers and books. That’s the idea, anyway.

It uses Jacques Distler’s version of Instiki, which amusingly stands for ‘instant’ wiki. I’ve been trying to get it to work for 5 months (albeit in a very desultory way).

Since symmetric monoidal 2-categories are really special 6-categories, I had not included them in my outline of the section The Dimensional Ladder. In that section I was planning to give nuts-and-bolts descriptions of weak $n$ -categories up to $n = 4$ . These ‘tetracategories’ should have braided monoidal 2-categories as a special case.

Of course this highly systematic approach is rather ambitious, and potentially very tiring. It might be good to ‘cheat’ and do sylleptic and symmetric monoidal 2-categories on a more ad hoc basis.

In my ambitious outline, I had planned to redo and improve the proof that 2-tangles are described by a braided monoidal 2-category, following suggestions by Todd Trimble based in part on the improved definition of braided monoidal 2-category given by Day and Street.

Needless to say this would be most fun with lots of pictures! Even better, of course, would be actual movies of the movie moves.

But, puncturing the hot air balloon of fantasy and falling back to reality:

I suppose the sensible approach is to coax you and other people to write cool explanations of $n$ -categorical stuff, meanwhile try to get the wiki working, and worry about organizing it all later.

Posted by: John Baez on May 5, 2008 9:14 PM | Permalink | Reply to this

Re: Theorems Into Coffee

$MathML-enabled post (click for more details).$

I can’t prove this — but I could if I could prove this other result.

Conjecture. In a symmetric monoidal category, let $(A,m,u)$ be a commutative monoid and $(A,k,v) _\times$ be a cocommutative comonoid which together form a commutative bialgebra structure. Then given two morphisms $f,g:A ^{\otimes n} \to A ^{\otimes m}$ which are finitely built from the symmetric monoidal structure and the morphisms $m$ , $u$ , $k$ and $v$ , the morphisms $f$ and $g$ are the same IF AND ONLY IF, when drawn as graphs (or ‘string diagrams’) using the graphical calculus, each gives the same number of ways to pass from a given element of the product $A ^{\otimes n}$ to the given element of the product $A ^{\otimes m}$ .

Elements from the product $A ^{\otimes n}$ just correspond to the ‘input wires’ in the graphical calculus, and similarly elements of the product $A ^{\otimes m}$ correspond to ‘output wires’. We ‘pass from an input wire to an output wire’ by moving forwards through the diagram, going wherever we like when we get to a junction, except that we’re not allowed to go backwards.

This is a bit difficult to explain without pictures, so if I’ve failed to convey anything in the previous paragraph, draw a picture of the ‘interesting’ bialgebra equation, the one involving the multiplication, the comultiplication and a crossing. Note that there is exactly one way to get from each input wire to each output wire; by the above conjecture, this means they must evaluate to the same morphism.

Unfortunately, I don’t know how to show that the bialgebra equations being satisfied is enough to prove the conjecture. Maybe this is a standard result in topology?

This can be applied to John’s problem by taking a natural-valued matrix like

(1)

{\left(\array{ a & b \\ c & d}\right)}

and turning it into a graph of the type described above, with $a$ ways to pass from the 1st input wire to the 1st output wire, $b$ ways to pass from the 1st input wire to the 2nd output wire, and so on. This construction gives us a way to turn a commutative bialgebra in C into a strict monoidal functor $\mathrm{Mat}(\mathbb{N}) \to \mathbf{C}$ , and this construction is actually an equivalence of categories.

There’s a nice modification of this result for commutative Frobenius algebras. We can generalise it to allow duals — that is, wires that are allowed to bend back on themselves — but we have to restrict to connected diagrams. Two graphs are then equal in the category if and only if there is the same number of ways to pass from any wire, input or output, to any other wire, input or output — except now you ARE allowed to go backwards, and not just along the ‘antiwires’ introduced by the duals! Also, you’re not allowed to use the same part of each wire more than once for each journey from an input wire to an output wire. Try it by using it to prove the Frobenius identity.

I think of commutative bialgebras as ‘classical’ and commutative Frobenius algebras as ‘quantum’, because you can solve their graph equality problems by imagining ‘classical’ or ‘quantum’ particles moving along the graphs.

I should point out that I can’t prove any of this stuff; it’s just the intuition I’ve come up with for working with these objects. If any of it’s false, I would really like to know!

Posted by: Jamie Vicary on May 6, 2008 3:07 AM | Permalink | Reply to this

Re: Theorems Into Coffee

$MathML-enabled post (click for more details).$

Jamie wrote:

I can’t prove this — but I could if I could prove this other result.

I’m glad someone is trying to prove the claimed theorem instead of just joking about ‘coffee’, ‘eat shoots and leaves’, and the like. (I have a grad student who is trying to prove it, but he’s not an expert on PROPs, so I bet someone else can beat him to it.) I think you deserves a few cupfuls of coffee just for proposing this strategy.

Indeed, your sort of string diagram reasoning is one of the things that makes me sure the claimed theorem is true. We can think of $Mat(\mathbb{N})$ as a slightly decategorifed version of the bicategory of spans of finite sets. I believe that string diagrams built from unit, counit, multiplication and comultiplication, modulo the bicommutative bimonoid axioms, can always be reshuffled so the comultiplications and counits all come before the multiplications and units. In this ‘normal form’, any such string diagram can be read as a span of finite sets going from the set of input wires to the set of output wires.

But, making this into a rigorous proof seems to involve work. It’s quite possible that the ‘royal road’ to proving the theorem avoids the detour through string diagrams, spans and the like.

For example, it might be easier to show that: 1) regarded as an algebraic theory in Lawvere’s sense, $Mat(\mathbb{N})$ is the theory for commutative monoids; 2) applying the functor that takes algebraic theories to their underlying PROPs, we obtain the PROP for bicommutative bimonoids. Evidence for part 2) appears in pp. 51-59 of these lecture notes. However, I should warn you that proofs of the claimed theorems in these notes have not been written up! So, this approach too would require some work.

If a bunch of people wish to collaborate and prove this theorem, I will split the coffee. I have at least one other conjecture that might be proved a similar way, which I will announce soon… so, the rewards will gradually go up.

Posted by: John Baez on May 6, 2008 4:57 AM | Permalink | Reply to this

Read the post Theorems Into Coffee II
Weblog: The n-Category Café
Excerpt: Another coffee challenge: prove that matrices of integers are morphisms in the PROP for commutative and cocommutative Hopf algebras!
Tracked: May 6, 2008 5:36 AM

Re: Theorems Into Coffee

$MathML-enabled post (click for more details).$

I think I can prove this but am too lazy to write it up carefully, so in the interests of co-operation, I’ll post a sketch of my proof here.

There are three things we need to check:

A bicommutative bialgebra defines an algebra over our PROP
Every algebra over our PROP is a bicommutative bialgebra
Morphisms of algebras over our PROP are precisely bialgebra homomorphisms

It seems to me that (1) is the hardest part of this.

Let’s do (2) first quickly. Suppose that $F:Mat(\mathbb{N})\rightarrow \mathcal{C}$ is a strict monodial functor. We set $A=F(1)$ , $\mu=F((1 1))$ , and $u=F(0:0\rightarrow 1)$ . Then $A$ is an commutative monoid with respect to $\mu$ and with unit $u$ .

To see this, one just observes that each of the axioms for a commutative monoid just corresponds to a matrix equation in our PROP

Unfortunately at this point I can’t make the matrix environment work to illustrate this clearly.

To see the comonoid structre on $A$ it now suffices to apply the contravariant functor from our PROP to itself given by transpose operation on matrices. The proof is then just dual to the above, with $\Delta=F((1 1)^t)$ .

Finally to check that the comultiplication is an monoid homomophism just corresponds to another matrix equation.

The real meat of the problem is in (1) above. Let’s suppose that we have an bicommutative bialgebra $A\in\mathcal{C}$ . We want to make $A$ into an algebra over our PROP.

The key idea in my proof is that our PROP is generated as a category with Hom sets enriched over $\mathbb{N}$ by matrices with only zero entries except for one $1$ . To make this work we need to define an additive structre on maps $A^{\otimes n}\rightarrow A^{\otimes m}$ .<\p>

To this end we define maps $\mu_n:A^{\otimes 2n}\rightarrow A^{\otimes n}$ and $\Delta_m:A^{\otimes 2m}\rightarrow A^{\otimes m}$ .

$\Delta_m$ is the map $Delta^{\otimes m}$ composed with the map that swaps the factors in $A^{\otimes 2m}$ by the permutation that results in the ordering $(1, 3, \ldots, 2n-1, 2, 4, \ldots 2n)$ .

Similarly $\mu_n$ is the map that permutes the factors of $A^{2n}$ by the permutation that results in the ordering $(1, n+1, 2, n+2, \ldots, n, 2n)$ composed with $mu^{otimes n}$ .

Now we have two maps $f,g:A^{\otimes n}\rightarrow A^{\otimes m}$ we define $f+g$ by $\mu_m(f\otimes g)\Delta_n$ .

That this addition is associative follows from the biassociativity of $A$ . That it commutative follows from the bicommutativity of $A$ .

Now to define the functor from our PROP to $\mathcal{C}$ defining $A$ it suffices to define $F(E_{ij}^{nm})$ where $E_{ij}^{nm}$ is the $n\times m$ matrix with a $1$ in the $ij$ th entry and $0$ ’s elsewhere. But this is just given by

(1)

u^{\otimes i-1}\otimes id\otimes u^{\otimes m-i})(\epsilon^{\otimes j-1}\otimes id\otimes\epsilon^{\otimes n-j}).

With the algebraic structure we have imposed on maps this determines F(f) uniquely for all $f$ , and the usual properties of matrices such as distributivity makes checking we really do get a functor straightforward.

Time prevents me from explaining (3) but requires no new ideas.

Posted by: Simon Wadsley on May 6, 2008 12:59 PM | Permalink | Reply to this

Read the post Theorems Into Coffee III
Weblog: The n-Category Café
Excerpt: What is the symmetric monoidal category of finite sets and partially defined functions the PROP for? Prove your answer and win some coffee!
Tracked: May 16, 2008 6:31 PM

Read the post Theorems Into Coffee IV
Weblog: The n-Category Café
Excerpt: The first Theorems into Coffee prize is awarded. Read about Steve Lack's work on PROPs, and try your hand at the latest Theorems into Coffee challenge.
Tracked: July 12, 2008 2:11 PM

The n-Category Café

Skip to the Main Content

May 4, 2008