From: mxh@dcs.ed.ac.uk Date: Tue, 1 Dec 92 15:12:49 GMT
I'm looking for a reference for the following lemma on composition of fibrations [and the relation with indexed products].
There is a result which can be used in showing that every algebraic functor has an adjoint (Lawvere's thesis): if V is a cartesian closed category then the pointwise left kan extension k : A --> V of a finite product preserving functor f : B --> V, along any functor r : B --> A, is finite product preserving. [This can be tricky to prove, even for the expert. The only time I remember Saunders hesitating a bit during his marathon lecturing stint at Bowdoin College, Maine Summer 1969 was exactly over this point near the end of a lecture. He was trying to do it from the universal property of kan extensions. That evening Dubuc and I pointed out that pointwiseness was essential; by the next lecture Saunders had a proof which I'm sure he would have found without our comments!] Brian Day's Masters Thesis had a proof in the appendix. Borceux-Day have something that I have no time to look up in Bull Austral Math Soc (I think; help anyone?). Max Kelly and Stephen Lack have done something recently to appear in Appl Cat Structures Vol 1 (Univ Syd Math Report 92-29). But what the crumbs is Ross on about in relation to Martin Hofmann's question, you ask. Well, take V to be Cat, which is cartesian closed. Let p : E --> B be obtained from f : B --> Cat by the Grothendieck construction. Then r o p is the fibration constructed from k : A --> Cat. So, a reference? I'd say "its a variant of the above result on kan extns of prod pres funcs". It is also true that Cat is a topos wrt categories enriched over it, and then left kan extn of a (enriched) left exact functor into Cat is left exact. [See Kelly's paper in Cahiers on enriched locally presentable categories.] No time to give all the detail I'd like. --Ross ==============================================================================