theorem about ends

theorem about ends

[Paul Levy]

Dear all,

Does the following result (which I learnt from Rasmus Mogelberg)
appear in the literature somewhere?


Given categories C and D, a functor P : C^op x D --> Set and an
adjunction F -| U : D --> C

the end over c in C of P(c,Fc) is (isomorphic to) the end over d in D
of P(Ud,d).


Paul


--
Paul Blain Levy
School of Computer Science, University of Birmingham
+44 (0)121 414 4792
http://www.cs.bham.ac.uk/~pbl











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

Re: theorem about ends

[Steve Lack]

Dear Paul,

This is (a special case of) Lemma 2.1 in 

G.M. Kelly & Stephen Lack, Finite-product-preserving functors, Kan extensions, and strongly finitary 2-monads.
Applied Categorical Structures 1:85-94, 1993.

Steve.

On 07/02/2011, at 11:25 AM, Paul Levy wrote:

> Dear all,
> 
> Does the following result (which I learnt from Rasmus Mogelberg)
> appear in the literature somewhere?
> 
> 
> Given categories C and D, a functor P : C^op x D --> Set and an
> adjunction F -| U : D --> C
> 
> the end over c in C of P(c,Fc) is (isomorphic to) the end over d in D
> of P(Ud,d).
> 
> 
> Paul
> 
> 
> --
> Paul Blain Levy
> School of Computer Science, University of Birmingham
> +44 (0)121 414 4792
> http://www.cs.bham.ac.uk/~pbl
> 
> 
> 
> 
> 
> 
> 
> 
> 
> 
> 
> [For admin and other information see: http://www.mta.ca/~cat-dist/ ]



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

Re: theorem about ends

[Richard Garner]

Dear Paul,

I do not know anywhere that it appears explicitly, but it can be
pieced together quite quickly from results about weighted limits in
Kelly's book. First, given any adjunction X -| Y : B --> A, any W : A
--> Set, and any G : B --> C, we have

{WY, G} = {W, GX}  (**)

in the sense that the one exists if the other does, and the canonical
comparison is then an isomorphism. This follows since Lan_X(W) = WY
(by (4.28) of Kelly) and {Lan_X(W), G} = {W, GX} (by (4.58) ibid).

Since the end of a functor T: K^op x K --> E is by definition ((3.59)
ibid) the limit of H weighted by the hom-functor H_K: K^op x K -->
Set, we have, in the situation you describe, that

End(P(-,F-)) = {H_C, P.(1 x F)} = {H_C.(1 x U), P} = {H_D.(F^op x 1),
P} = {H_D, P.(U^op x 1)} = End(P(U-,-))

by applying (**) twice to the adjointnesses 1 x F -| 1 x U  and  U^op
x 1 -| F^op x 1, and using the natural isomorphism H_C.(1 x U) =
H_D.(F^op x 1) obtained from the adjointness F -| U.

Richard



On 7 February 2011 11:25, Paul Levy <pbl@cs.bham.ac.uk> wrote:
> Dear all,
>
> Does the following result (which I learnt from Rasmus Mogelberg)
> appear in the literature somewhere?
>
>
> Given categories C and D, a functor P : C^op x D --> Set and an
> adjunction F -| U : D --> C
>
> the end over c in C of P(c,Fc) is (isomorphic to) the end over d in D
> of P(Ud,d).
>
>
> Paul
>
>
> --
> Paul Blain Levy
> School of Computer Science, University of Birmingham
> +44 (0)121 414 4792
> http://www.cs.bham.ac.uk/~pbl
>
>

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

Re: theorem about ends

[Ross Street]

Dear Paul

On 07/02/2011, at 11:25 AM, Paul Levy wrote:

> Does the following result (which I learnt from Rasmus Mogelberg)
> appear in the literature somewhere?
>
> Given categories C and D, a functor P : C^op x D --> Set and an
> adjunction F -| U : D --> C
>
> the end over c in C of P(c,Fc) is (isomorphic to) the end over d in D
> of P(Ud,d).

This is the sort of thing that would be used in the course of things
without explicit enunciation as a Lemma or Proposition. It involves
two applications of the end version of Yoneda (take V = Set for the
ordinary case):

end_c P(c,Fc)  =~ end_{c,d} V(D(Fc,d),P(c,d)) =~  end_{c,d}
V(C(c,Ud),P(c,d)) =~ end_d P(Ud,d).

It is quite pretty, I agree.

Ross


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

Re: theorem about ends

[Fred E.J. Linton]

Paul Blain Levy asks:

> Does the following result (which I learnt from Rasmus Mogelberg)
> appear in the literature somewhere?
> 
> Given categories C and D, a functor P : C^op x D --> Set and an
> adjunction F -| U : D --> C
> 
> the end over c in C of P(c,Fc) is (isomorphic to) the end over d in D
> of P(Ud,d).

For well over 40 years I've always thought of that as 
the Beck/Lawvere vision of what an adjunction *is* :-) .

Cheers, -- Fred





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

Re: theorem about ends

[Richard Garner]

Actually, since the codomain of your functor P is actually Set, the
argument I gave---which would be valid for any suitably complete
codomain---can be rewritten to avoid the use of weighted limits
entirely, by expressing those necessary in this case as hom-sets in a
functor category. It then becomes the single calculation that

End(P(-,F-)) = [C^op x C, Set](Hom_C, P.(1 x F)) = [C^op x D,
Set](Hom_C.(1 x U), P) = [C^op x D, Set](Hom_D.(F^op x 1), P) = [C^op
x D, Set](Hom_D, P.(U^op x 1)) = End(P(U-,-))

which requires no machinery beyond that of transpositions under adjunction.

Richard

On 7 February 2011 15:35, Richard Garner <richard.garner@mq.edu.au> wrote:
> Dear Paul,
>
> I do not know anywhere that it appears explicitly, but it can be
> pieced together quite quickly from results about weighted limits in
> Kelly's book. First, given any adjunction X -| Y : B --> A, any W : A
> --> Set, and any G : B --> C, we have
>
> {WY, G} = {W, GX}  (**)
>
> in the sense that the one exists if the other does, and the canonical
> comparison is then an isomorphism. This follows since Lan_X(W) = WY
> (by (4.28) of Kelly) and {Lan_X(W), G} = {W, GX} (by (4.58) ibid).
>
> Since the end of a functor T: K^op x K --> E is by definition ((3.59)
> ibid) the limit of H weighted by the hom-functor H_K: K^op x K -->
> Set, we have, in the situation you describe, that
>
> End(P(-,F-)) = {H_C, P.(1 x F)} = {H_C.(1 x U), P} = {H_D.(F^op x 1),
> P} = {H_D, P.(U^op x 1)} = End(P(U-,-))
>
> by applying (**) twice to the adjointnesses 1 x F -| 1 x U  and  U^op
> x 1 -| F^op x 1, and using the natural isomorphism H_C.(1 x U) =
> H_D.(F^op x 1) obtained from the adjointness F -| U.
>
> Richard
>

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