Characterizing the adjunction that arises given a groupoid G in a cartesian category C

Characterizing the adjunction that arises given a groupoid G in a cartesian category C

[Christopher Townsend]

If G = (G_1 => G_0) is a groupoid in a cartesian category C then there

is an adjunction between [G,C] and C provided that C has coequalizers.

Here [G,C] is notation for the category of objects over G_0 with G_1

actions. The right adjoint takes an object X to (G_0xX,mxId) where m is

the groupoid G's composition.

I'd appreciate any guidance on what has been noted/published about the

following lemma whose proof I believe follows easily once you realise

that the left adjoint sends (G_1,m) to G_0:

Lemma: If L-!R is an adjunction between cartesian categories D and C

(L:D->C and R:C->D), then this adjunction is equivalent to the

adjunction [G,C]->C just described for some groupoid G internal to C if

and only if there exists W an object of D such that the pullback functor

W*:D->D/W is monadic and the functor D/W->C/LW induced by L is an

equivalence.

I feel it is a very neat characterization of the situation where an

adjunction arises from a groupoid as the conditions on D seem very

'mild' and not at all related to groupoids; but the groupoid structure

drops out.

Hopefully (the lemma is correct? and) somebody has published the lemma

at this level of generality? I believe that the technique is known as it

is essentially used in SGA4 to show that every etendu topos is of the

form BG. Also it is in effect used in the proof of the Joyal & Tierney

theorem on the localic groupoid representation of Grothendieck toposes.

Thanks,

Christopher Townsend


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