From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/5264 Path: news.gmane.org!not-for-mail From: Steve Vickers Newsgroups: gmane.science.mathematics.categories Subject: Re: Lambek's lemma Date: Fri, 13 Nov 2009 10:07:41 +0000 Message-ID: References: Reply-To: Steve Vickers NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1258141866 6348 80.91.229.12 (13 Nov 2009 19:51:06 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Fri, 13 Nov 2009 19:51:06 +0000 (UTC) To: Vaughan Pratt , Original-X-From: categories@mta.ca Fri Nov 13 20:50:59 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 1N92Ac-0004hg-UE for gsmc-categories@m.gmane.org; Fri, 13 Nov 2009 20:50:59 +0100 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1N91iJ-0004dp-KY for categories-list@mta.ca; Fri, 13 Nov 2009 15:21:43 -0400 Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:5264 Archived-At: Dear Vaughan, I used the same argument in "Topical Categories of Domains" Propn 2.3.7 (published 1999, though long in the gestation). I remarked "We briefly recall the usual argument", so I'm not claiming any priority. As I recall I had little trouble working out the proof for myself, but I knew the result as folklore and assumed any simple proofs would be part of the same folklore. (Actually, my result is slightly more general. I was working in a 2-category (of Toposes) that, unlike Cat, is not well-pointed. Given the endo-1-cell T, I assumed that the 0-cell A of T-algebras (the inserter from T to the identity) had a global point - a 1-cell from 1 to A - that was strongly initial in the sense that it was left adjoint to the unique 1-cell A -> 1. In my context the simple argument still worked.) Regards, Steve. 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/ ]