Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 3 of 3
Hi, I hope it is OK to ask here again a basic question. I have some difficulty with the proof of the coend formula for left Kan extensions in Mac Lane (pp. 240-241 in the second edition).
While I was able to understand each step of the chain of isomorphisms, there is the question of naturality in the functor throughout the chain, nonchalantly stated in the proof. It took me some while to even understand how the ends in the chain are functors of , and I am currently struggling to prove naturality in . My strategy is to show that isomorphisms commuting with different universal wedges are, in fact, natural in , through endless diagram chasing.
Both making the ends functors of and proving naturality turns out
to be an endless messy exercise, pages upon pages
of diagrams. So, I believe that I must be missing some simple
argument. Is there a simple way to prove naturality in ? Is there
any reference where the proof of naturality is spelled out? I must
comment that for me, ends and coends are universal wedges (as in Mac
Lane), and I am not familiar with enriched categories, weighted limits etc.
Verifying naturality is always a good idea; sometimes whole papers result from a failure to verify naturality, see, e.g., Thomason’s “Beware of the phony multiplication…”. From my own practice, in one of my recent papers submitted to a journal, a proof turned out to be defective because a certain transformation was not natural. Fortunately, it was easily correctable.
Concerning the specific proof that you cited: instead of writing down any actual diagram, I would simply argue by composing natural transformations, without writing down any diagrams. You also need to invoke the naturality of constructions used in the proof.
For example, the first step involves the end formula for Nat (the set of natural transformations), and you can simply refer to the corresponding proposition that establishes this formula and proves its naturality.
The second step is formal unfolding.
The third step step commutes a colimit (coend) out of the first argument of A(-,-). The proposition that establishes this isomorphism also proves its naturality in the second argument. From this, you deduce the naturality with respect to S, by whiskering the corresponding natural transformation S_1→S_2 and the functor into which it is plugged in.
The fourth step unfolds the definition of copowers using its universal property. Same story as in the previous step.
Notice that at all steps we argue without diagrams, just by whiskering functors and natural transformations together.
Thanks a lot for your answer! I will certainly try to understand how to use whiskering for a simple proof.
1 to 3 of 3