* theorem about ends @ 2011-02-07 0:25 Paul Levy 2011-02-07 3:00 ` Steve Lack ` (2 more replies) 0 siblings, 3 replies; 6+ messages in thread From: Paul Levy @ 2011-02-07 0:25 UTC (permalink / raw) To: categories list 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/ ] ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: theorem about ends 2011-02-07 0:25 theorem about ends Paul Levy @ 2011-02-07 3:00 ` Steve Lack 2011-02-07 4:35 ` Richard Garner 2011-02-07 11:26 ` Ross Street 2 siblings, 0 replies; 6+ messages in thread From: Steve Lack @ 2011-02-07 3:00 UTC (permalink / raw) To: Paul Levy; +Cc: categories list 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/ ] ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: theorem about ends 2011-02-07 0:25 theorem about ends Paul Levy 2011-02-07 3:00 ` Steve Lack @ 2011-02-07 4:35 ` Richard Garner 2011-02-07 11:26 ` Ross Street 2 siblings, 0 replies; 6+ messages in thread From: Richard Garner @ 2011-02-07 4:35 UTC (permalink / raw) To: Paul Levy; +Cc: categories list 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/ ] ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: theorem about ends 2011-02-07 0:25 theorem about ends Paul Levy 2011-02-07 3:00 ` Steve Lack 2011-02-07 4:35 ` Richard Garner @ 2011-02-07 11:26 ` Ross Street 2 siblings, 0 replies; 6+ messages in thread From: Ross Street @ 2011-02-07 11:26 UTC (permalink / raw) To: Paul Levy; +Cc: categories list 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/ ] ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: theorem about ends
@ 2011-02-07 3:06 Fred E.J. Linton
0 siblings, 0 replies; 6+ messages in thread
From: Fred E.J. Linton @ 2011-02-07 3:06 UTC (permalink / raw)
To: categories
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/ ]
^ permalink raw reply [flat|nested] 6+ messages in thread
[parent not found: <AANLkTikzK3ygOLMAUqm6WKWCrv7Ba8aBHugbpFrCWqMN@mail.gmail.com>]
* Re: theorem about ends [not found] <AANLkTikzK3ygOLMAUqm6WKWCrv7Ba8aBHugbpFrCWqMN@mail.gmail.com> @ 2011-02-07 5:04 ` Richard Garner 0 siblings, 0 replies; 6+ messages in thread From: Richard Garner @ 2011-02-07 5:04 UTC (permalink / raw) To: Paul Levy; +Cc: categories list 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/ ] ^ permalink raw reply [flat|nested] 6+ messages in thread
end of thread, other threads:[~2011-02-07 11:26 UTC | newest] Thread overview: 6+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2011-02-07 0:25 theorem about ends Paul Levy 2011-02-07 3:00 ` Steve Lack 2011-02-07 4:35 ` Richard Garner 2011-02-07 11:26 ` Ross Street 2011-02-07 3:06 Fred E.J. Linton [not found] <AANLkTikzK3ygOLMAUqm6WKWCrv7Ba8aBHugbpFrCWqMN@mail.gmail.com> 2011-02-07 5:04 ` Richard Garner
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).