From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/5260 Path: news.gmane.org!not-for-mail From: "Prof. Peter Johnstone" Newsgroups: gmane.science.mathematics.categories Subject: Re: Lambek's lemma Date: Thu, 12 Nov 2009 21:14:35 +0000 (GMT) Message-ID: References: Reply-To: "Prof. Peter Johnstone" NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed X-Trace: ger.gmane.org 1258079844 20902 80.91.229.12 (13 Nov 2009 02:37:24 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Fri, 13 Nov 2009 02:37:24 +0000 (UTC) To: Vaughan Pratt , Original-X-From: categories@mta.ca Fri Nov 13 03:37:17 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 1N8m2G-0006cV-96 for gsmc-categories@m.gmane.org; Fri, 13 Nov 2009 03:37:16 +0100 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1N8lVP-0006DL-8v for categories-list@mta.ca; Thu, 12 Nov 2009 22:03:19 -0400 Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:5260 Archived-At: Vaughan's argument appears in the Elephant (but with the second square, which he has indicated by dots, drawn in, so that there are seven arrows) as Lemma A1.1.4. Though it's not credited there, I learned it from Peter Freyd --- I can't remember when, but that part of the Elephant was written well before 1998. Peter Johnstone ----------------------- On Wed, 11 Nov 2009, Vaughan Pratt wrote: > 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/ ] > [For admin and other information see: http://www.mta.ca/~cat-dist/ ]