Re: Lambek's lemma

[Charles Wells <charles@abstractmath.org>]

Isosceles triangles caused a bit of discussion on the mathedu mailing
list recently, starting at
http://mathforum.org/kb/message.jspa?messageID=6864271&tstart=0
(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 <pratt@cs.stanford.edu> 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/ ]
>



-- 
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.htm
personal website:  http://www.abstractmath.org/Personal/index.html
sixwingedseraph.facebook.com


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]