From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/5256 Path: news.gmane.org!not-for-mail From: Charles Wells Newsgroups: gmane.science.mathematics.categories Subject: Re: Lambek's lemma Date: Thu, 12 Nov 2009 14:59:57 -0600 Message-ID: References: Reply-To: Charles Wells NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: ger.gmane.org 1258079565 20348 80.91.229.12 (13 Nov 2009 02:32:45 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Fri, 13 Nov 2009 02:32:45 +0000 (UTC) To: catbb Original-X-From: categories@mta.ca Fri Nov 13 03:32:38 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 1N8lxm-00052l-8U for gsmc-categories@m.gmane.org; Fri, 13 Nov 2009 03:32:38 +0100 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1N8lU5-00063y-Vn for categories-list@mta.ca; Thu, 12 Nov 2009 22:01:58 -0400 Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:5256 Archived-At: Isosceles triangles caused a bit of discussion on the mathedu mailing list recently, starting at http://mathforum.org/kb/message.jspa?messageID=3D6864271&tstart=3D0 (isosceles triangles only appear a couple of levels down and then the discussion gets quite heated.) . I also wrote about it here: http://sixwingedseraph.wordpress.com/2009/10/23/naive-proofs/ in connection with the possibility of their being a generic triangle. Wikipedia says the proof of the pons asinorum by mirror image was by Pappus= . Charles Wells On Thu, Nov 12, 2009 at 1:07 AM, Vaughan Pratt wrot= e: > 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? =A0Here's an argument with > five arrows. > > TA --a--> A > =A0| =A0 =A0 =A0 =A0| > =A0|Tf =A0 =A0 =A0|f > =A0| =A0 =A0 =A0 =A0| > =A0v =A0 =A0 =A0 =A0v > TTA -Ta-> TA > . =A0 =A0 =A0 =A0 =A0 \ > . =A0 =A0 =A0 =A0 =A0 =A0\a > . =A0 =A0 =A0 =A0 =A0 =A0 \ > . =A0 =A0 =A0 =A0 =A0 =A0 _\| > . > . =A0 =A0 =A0 =A0 =A0 =A0 =A0 =A0 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 =3D aTaTf =3D > aT(af). =A0The latter square therefore witnesses a homomorphism af: A --> > A. But by initiality there is only one such homomorphism, the identity, > whence af =3D 1. =A0Hence fa =3D TaTf (commutative diagram) =3D T(af) =3D= T(1) =3D > 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. =A0I 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. =A0This is the celebrated *Pons Asinorum= * > or Bridge of Asses. =A0Applied here, the ability to prove Lambek's lemma > is a litmus test of whether you can think categorically. =A0(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 . =A0The= n > someone's computer program noticed that the triangles ABC and ACB (A > being the apex, with |AB| =3D |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. =A0CT 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/ ] > --=20 professional website: http://www.cwru.edu/artsci/math/wells/home.html blog: http://sixwingedseraph.wordpress.com/ abstract math website: http://www.abstractmath.org/MM//MMIntro.htm astounding math stories: http://www.abstractmath.org/MM//MMAstoundingMath.h= tm personal website: http://www.abstractmath.org/Personal/index.html sixwingedseraph.facebook.com [For admin and other information see: http://www.mta.ca/~cat-dist/ ]