Re: Lambek's lemma

["Prof. Peter Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>]

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/ ]