From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/5240 Path: news.gmane.org!not-for-mail From: Vaughan Pratt Newsgroups: gmane.science.mathematics.categories Subject: Lambek's lemma Date: Wed, 11 Nov 2009 23:07:30 -0800 Message-ID: Reply-To: Vaughan Pratt NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1258046914 20055 80.91.229.12 (12 Nov 2009 17:28:34 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Thu, 12 Nov 2009 17:28:34 +0000 (UTC) To: categories list Original-X-From: categories@mta.ca Thu Nov 12 18:28:27 2009 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from mailserv.mta.ca ([138.73.1.1]) by lo.gmane.org with esmtp (Exim 4.50) id 1N8dSz-0001cM-DC for gsmc-categories@m.gmane.org; Thu, 12 Nov 2009 18:28:17 +0100 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1N8cy4-00005d-Gt for categories-list@mta.ca; Thu, 12 Nov 2009 12:56:20 -0400 Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:5240 Archived-At: Lambek's lemma holds that every initial algebra is an isomorphism (and dually for every final coalgebra). With how small a diagram can you prove this? Here's an argument with five arrows. TA --a--> A | | |Tf |f | | v v TTA -Ta-> TA . \ . \a . \ . _\| . . A Here f is the unique T-homomorphism from the initial T-algebra A to the T-algebra TA, while the a arrow at lower right whiskers (1-categorically) the square witnessing that f is a T-homomorphism. This whisker creates another commutative square, namely afa = aTaTf = aT(af). The latter square therefore witnesses a homomorphism af: A --> A. But by initiality there is only one such homomorphism, the identity, whence af = 1. Hence fa = TaTf (commutative diagram) = T(af) = T(1) = 1, whence f and a are mutual inverses. I showed this argument to Peter Freyd in 1998 and his first response was an argument with seven arrows that he felt was needed to make the argument stick. I suggested that his argument was simply a blow-up of mine, which he agreed to half an hour later. Lambek's lemma is somewhat reminiscent of Proposition 5 of Book I of Euclid's *Elements*, that if two sides of a triangle are equal then their opposite angles are equal. This is the celebrated *Pons Asinorum* or Bridge of Asses. Applied here, the ability to prove Lambek's lemma is a litmus test of whether you can think categorically. (Personally I consider the uniqueness of the free algebra on a given set as an adequate test.) Until recently Proposition 5 was always proved along the lines in Euclid, cf. http://aleph0.clarku.edu/~djoyce/java/elements/bookI/propI5.html . Then someone's computer program noticed that the triangles ABC and ACB (A being the apex, with |AB| = |AC|) were congruent, from which the result followed trivially. Such a result would register about 2 on the New York Times' Richter scale of earthshaking mathematical results, were it not for the fact that it was first noticed by a computer (so the story went). The sad thing is that even if this five-arrow proof of Lambek's lemma had been first found by a computer, the New York Times could not have whipped up the same enthusiasm for it as for the Pons Asinorum. CT has not yet acquired the visibility of geometry in the mind of the technically literate public. Vaughan Pratt [For admin and other information see: http://www.mta.ca/~cat-dist/ ]