Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeJul 5th 2011
    • (edited Jul 6th 2011)

    [edit: removed, sorry]

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeJul 6th 2011
    • (edited Jul 6th 2011)

    [edit: removed, sorry]

    • CommentRowNumber3.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 6th 2011

    Maybe a silly comment, I didn’t think about it too hard yet, but is it possible that the 2-functor Set :PosetTopos essSet^-: Poset \to Topos_{ess} to the 2-category of Grothendieck toposes and essential geometric morphisms is reflective (has a left 2-adjoint)?

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeJul 8th 2011
    • (edited Jul 8th 2011)

    Thanks, Todd, for offering help. I had been doing too many things at once, and got myself mixed up here.

    Maybe I still am. But I hope it’s getting better. So what about this “fix” here:

    the functor [,Set]:PosetTopos[-,Set] : Poset \to Topos factors through TopSpaceTopSpace

    [,Set]:PosetAlexandrovTopSpaceLocaleShTopos. [-,Set] : Poset \stackrel{Alexandrov}{\to} TopSpace \hookrightarrow Locale \stackrel{Sh}{\hookrightarrow} Topos \,.

    The trouble with my original suggestion is that of course the second morphisms does not preserve all limits (it is left adjoint, instead) but the first one seems to.

    • CommentRowNumber5.
    • CommentAuthorTobyBartels
    • CommentTimeJul 9th 2011
    • (edited Jul 9th 2011)

    The functor TopSpaceLocaleTopSpace \hookrightarrow Locale isn’t really an inclusion (and essentially so, being not faithful), but you should be able to replace TopSpaceTopSpace here with the category of sober spaces if that’s important. (This works because you start with PosetPoset instead of with ProsetProset.)

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeJul 9th 2011
    • (edited Jul 9th 2011)

    Right, yes. Just the other day I have added that discussion to locale (or expanded on the discussion that had been there).

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeJul 25th 2011
    • (edited Jul 25th 2011)

    A while back Todd kindly made the following suggestion:

    is it possible that the 2-functor [,Set]:PosetTopos ess[-,Set] : Poset \to Topos_{ess} to the 2-category of Grothendieck toposes and essential geometric morphisms is reflective (has a left 2-adjoint)?

    It took me a while to come back to this. But I seem to believe now that this suggestion is going exactly in the right direction.

    A key step to see this while using standard facts about localic reflection should be theorem 4.2 in this article (a discussion of which I have by now added to Alexandrov space).

    This says that a morphism AlexPAlexQAlex P \to Alex Q of Alexandrov locales comes from a morphism PQP \to Q of posets precisely if its inverse image has a left adjoint.

    Now, one has to be a bit careful with the 2-category structures on Locale and Topos, but unless I am mixing it up, I think this means under the 2-fully faithful 2-functor Sh:LocaleToposSh : Locale \to Topos that:

    a geometric morphism [P,Set][Q,Set][P, Set] \to [Q,Set] comes from a morphisms PQP \to Q of posets precisely if it is essential.

    Right? (I mixed up my variances and 2-variances in all possible ways in the last hour and am getting a bit tired, so I won’t mind if you give me a sanity check.)

    (Unless I am wrong, there is probably also a much more direct way to see this. )

    • CommentRowNumber8.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 26th 2011

    a geometric morphism [P,Set][Q,Set][P, Set] \to [Q, Set] comes from a morphism PQP \to Q of posets precisely if it is essential.

    Yes, that is precisely what I was thinking. (And yes, getting mixed up in variances here is as easy as falling off a log.) More exactly, my thinking was that

    • If CC and DD are small categories, then there is a contravariant equivalence between the category of essential geometric morphisms Set CSet DSet^C \to Set^D and the category of functors C¯D¯\widebar{C} \to \widebar{D} where C¯\widebar{C} denotes Cauchy completion, and

    • Posets are already Cauchy-complete.

    To break down the first point a little more: the bicategory of profunctors between (Cauchy-complete) categories is equivalent to the bicategory of presheaf categories and cocontinuous maps. In more detail, a functor F:C opD opF: C^{op} \to D^{op} induces a profunctor or bimodule hom D op(,F):D×C opSet\hom_{D^{op}}(-, F-): D \times C^{op} \to Set that has a right adjoint bimodule hom D op(F,):C op×DSet\hom_{D^{op}}(F-, -): C^{op} \times D \to Set, so that we get an induced adjoint pair

    (F !:Set CSet D)(F *:Set DSet C)(F_!: Set^C \to Set^D) \dashv (F^\ast: Set^D \to Set^C)

    in the bicategory of cocontinuous maps between presheaf categories, which gives an adjoint string

    F !F *F *F_! \dashv F^\ast \dashv F_\ast

    in the bicategory of presheaf categories and functors. This F *F_\ast is the essential geometric morphism. To go the other direction, starting with an adjoint string

    FGH:Set CSet D,F \dashv G \dashv H: Set^C \to Set^D,

    (i.e., starting with an essential geometric morphism HH), the bicontinuous functor GG induces a functor

    Bicont(G,Set):Bicont(Set C,Set)Bicont(Set D,Set)Bicont(G, Set): Bicont(Set^C, Set) \to Bicont(Set^D, Set)

    where Bicont(Set C,Set)Bicont(Set^C, Set) is practically the definition of Cauchy completion C¯\widebar{C}. So an essential geometric morphism Set CSet DSet^C \to Set^D induces a functor C¯D¯\widebar{C} \to \widebar{D}. However, a morphism θ:HH\theta: H \to H' between essential geometric morphisms induces a mate θ :GG\theta^\dagger: G' \to G running in the opposite direction, so that what we get is an equivalence

    EssGeom(Set C,Set D)[C¯,D¯] opEssGeom(Set^C, Set^D) \to [\widebar{C}, \widebar{D}]^{op}

    induced by HBicont(G,Set)H \mapsto Bicont(G, Set). Of course, the codomain here is equivalent to [C¯ op,D¯ op][\widebar{C}^{op}, \widebar{D}^{op}].

    • CommentRowNumber9.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 26th 2011

    To continue with my train of thought when I first made that proposal to Urs: here is my current guess as to what is going on.

    First, for \mathcal{B} a 2-category, let op\mathcal{B}^{op} denote the 2-category we get by reversing 1-cells but not 2-cells; let co\mathcal{B}^{co} denote the 2-category we get by reversing 2-cells but not 1-cells, and let coop\mathcal{B}^{coop} denote the 2-category that we get by reversing both.

    I think I want to start with the observation or guess that SetSet plays a role of ambimorphic object which in one role is a Cauchy complete category and which in another role is a bicomplete category. The idea is that we have an adjunction determined by this ambimorphic object, giving a local equivalence of categories

    BCat Cauchy[C,Set]CBicont(B,Set)\frac{B \to Cat_{Cauchy}[C, Set]}{C \to Bicont(B, Set)}

    where the objects on top are bicontinuous functors BSet CB \to Set^C (BB bicomplete), and the objects on the bottom are ordinary functors CBicont(B,Set)C \to Bicont(B, Set). This means we have a biadjunction

    (Cat CauchySet ()Bicomp op)(Bicomp opBicont(,Set)Cat Cauchy)(Cat_{Cauchy} \stackrel{Set^{(-)}}{\to} Bicomp^{op}) \dashv (Bicomp^{op} \stackrel{Bicont(-, Set)}{\to} Cat_{Cauchy})

    We can specialize this biadjunction by restricting bicomplete BB (as above) to toposes, noting the fact that Set CSet^C lands in toposes. In other words, if Topos bicontTopos_{bicont} denotes the category of toposes and bicontinuous functors between them, the biadjunction above specializes to a second “ambimorphic biadjunction”

    (Cat CauchySet ()Topos bicont op)(Topos bicont opBicont(,Set)Cat Cauchy)(Cat_{Cauchy} \stackrel{Set^{(-)}}{\to} Topos_{bicont}^{op}) \dashv (Topos_{bicont}^{op} \stackrel{Bicont(-, Set)}{\to} Cat_{Cauchy})

    Next: the process of taking right adjoints at the 1-cell level and mates at the 2-cell level should give us a biequivalence

    Topos bicont coopTopos essTopos_{bicont}^{coop} \to Topos_{ess}

    and so, applying “co” to the second ambimorphic adjunction, we ought to get a biadjunction

    (Cat Cauchy coTopos ess)(Topos essCat Cauchy co)(Cat_{Cauchy}^{co} \to Topos_{ess}) \dashv (Topos_{ess} \to Cat_{Cauchy}^{co})

    hoping here I haven’t made variance/level slips. (The “co” affects the directions of 2-cells but I suspect not the direction of biadjunctions, because the triangulator 2-cells in a biadjunction are isomorphisms and I think “co” here just amounts to inverting them. Even though I’m getting slightly nervous about variance, it does look right that the functor from toposes and essential geometric morphisms back to categories should be the right adjoint part, since this should be the category of essential points EssGeom(Set,)EssGeom(Set, -), and this looks to be limit preserving.)

    I am guessing that the process described as

    PosetAlexLocaleToposPoset \stackrel{Alex}{\to} Locale \to Topos

    first of all factors through Topos essToposTopos_{ess} \hookrightarrow Topos, but could be alternatively described as

    PosetCat Cauchy coTopos essPoset \to Cat_{Cauchy}^{co} \to Topos_{ess}

    where the first functor is actually the assignment PP opP \mapsto P^{op}. In other words, the 2-functor which takes a poset PP to its opposite P opP^{op} is a 2-functor which preserves directions of 1-cells but reverses 2-cells, so gives

    Poset() opPoset coCat Cauchy coPoset \stackrel{(-)^{op}}{\to} Poset^{co} \hookrightarrow Cat_{Cauchy}^{co}

    which we follow with the aforementioned Cat Cauchy coTopos essCat_{Cauchy}^{co} \to Topos_{ess}.

    Maybe I should pause for a sanity check myself: the thing you (Urs) proposed takes a poset PP to the locale whose frame is that of upward-closed subsets of PP, and then we take sheaves on that locale. The thing I suggested takes PP to P opP^{op} to Set P opSet^{P^{op}}. Hm… this seems a little twisted around; sheaves on the locale would be particular presheaves on the frame of up-sets [P,2][P, 2], which would be functors [P,2] opSet[P, 2]^{op} \to Set, which would induce functors PSetP \to Set, not P opSetP^{op} \to Set. Hm - what would be your take on using down-sets instead of up-sets here?

    The more I look at this, though, the less sure I am of my original suggestion that there is an adjunction along the lines of what I suggested in comment 3., and I can’t remember what might have been proposed in comments 1. and 2.

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeJul 26th 2011

    Thanks a whole lot, Todd!

    I need to think about some of the things you are saying here. For the moment I have started (just started) to record some statements at essential geometric morphism in a new section Properties – Relation to morphisms of (co)sites.

    Concerning the very last bit:

    Hm - what would be your take on using down-sets instead of up-sets here?

    The equivalence [P,Set]Sh(AlexP)[P,Set] \simeq Sh(Alex P) really proceeds via

    Op(AlexP)UpperSets(P) Op(Alex P) \simeq UpperSets(P)

    as far as I can see.

    The more I look at this, though, the less sure I am of my original suggestion that there is an adjunction along the lines of what I suggested in comment 3., and I can’t remember what might have been proposed in comments 1. and 2.

    The proposal in 1. and 2. was too naive as that I will repeat it here :-)

    For the moment I’d be happy to postpone the discussion of preservation of limits for a bit and concentrate on the full and faithfulness of [,Set]:PosetTopos ess[-,Set] : Poset \to Topos_{ess}. One thing I need to sort out for myself still is how its action on morphisms works out through the factorization [,Set]ShAlex[-,Set] \simeq Sh \circ Alex.

    • CommentRowNumber11.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 26th 2011
    • (edited Jul 26th 2011)

    The equivalence [P,Set]Sh(AlexP)[P,Set] \simeq Sh(Alex P) really proceeds via Op(AlexP)UpperSets(P)Op(Alex P) \simeq UpperSets(P) as far as I can see.

    Sorry, I didn’t make myself clear. I agree with this statement.

    What I was trying to do was put together your chain of arrows from PosetPoset to Topos essTopos_{ess} with my chain of arrows from PosetPoset to Topos essTopos_{ess} and see whether there was agreement (i.e., a commutative diagram). I was coming to the conclusion that there wasn’t agreement, because my chain does this:

    PP opSet P opP \mapsto P^{op} \mapsto Set^{P^{op}}

    (the first arrow goes from PosetPoset to Cat Cauchy coCat_{Cauchy}^{co}, and the second goes from Cat Cauchy coCat_{Cauchy}^{co} to Topos essTopos_{ess}). So I was trying to feel out if you were willing to use the other convention for the Alexandrov topology, where you take down-sets instead, and for which you’d have Sh(AlexP)Set P opSh(Alex P) \simeq Set^{P^{op}} (which would then agree with my chain).

    But now that I think it over further, I think it probably doesn’t matter much: there is a 2-equivalence Cat Cauchy coCat CauchyCat_{Cauchy}^{co} \simeq Cat_{Cauchy}. So for now you can ignore this particular remark, and I’ll mull over it privately.

    For the moment I’d be happy to postpone the discussion of preservation of limits for a bit and concentrate on the full and faithfulness of [,Set]:PosetTopos ess[-, Set]: Poset \to Topos_{ess}.

    I think that’s going to work out just fine. Using my chain at least (and I repeat that I don’t think any discrepancies between our chains will be a serious matter), it’s clear to me that i:PosetCat Cauchy coi: Poset \to Cat_{Cauchy}^{co} is full and faithful (i.e., the local functors hom(P,Q)hom(iP,iQ)\hom(P, Q) \to \hom(i P, i Q) will be equivalences), and the map j:Cat Cauchy coTopos essj: Cat_{Cauchy}^{co} \to Topos_{ess} will be similarly “full and faithful” because it has a 2-coreflector EssGeom(Set,)EssGeom(Set, -), i.e., the unit of the 2-adjunction, whose components look like

    CEssGeom(Set,Set C),C \to EssGeom(Set, Set^C),

    is an equivalence for every Cauchy-complete CC.

    What I am worried about though is the fact that ii is a right 2-adjoint, where jj is a left 2-adjoint, as far as I can make out. That makes me worried about preservation of limits.

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeJul 26th 2011

    Hi Todd,

    okay, I see. I am still a bit behind with following some details of what you describe, though I do follow the general strategy.

    Right at the beginning, you may have to help me here: you say

    Bicont(Set C,Set)Bicont(Set^C,Set) is practically the definition of Cauchy completion

    Why is that?

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeJul 26th 2011

    Why is that?

    Ah, never mind, I see it now in the description of “points of the Cauchy completion”

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeJul 26th 2011
    • (edited Jul 26th 2011)

    Okay, I think I follow all the constructions now. What I do not quite see yet is how you deduce that some of them actually constitute equivalences.

    For instance, how do you see that j:Cat Cauchy coTopos essj : Cat^{co}_{Cauchy} \hookrightarrow Topos_{ess} is co-reflective?

    Meanwhile, I am trying to get hold of the book by Borceux and Dejan Cauchy completion in category theory . Is that a good idea? Or would you recommend something else?

    • CommentRowNumber15.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 26th 2011
    • (edited Jul 26th 2011)

    Sorry: for someone who seems to talk about Cauchy completion a lot, I really don’t know the literature on it too well, in particular the Borceux-Dejan reference. I’m sure it can’t hurt.

    So I was basically claiming that Topos ess(Set,) opTopos_{ess}(Set, -)^{op} is right adjoint to jj. In more detail, if EE is a Grothendieck topos and CC is Cauchy complete, that there is an equivalence

    CTopos ess(Set,E) opSet CE\frac{C \to Topos_{ess}(Set, E)^{op}}{Set^C \to E}

    where the arrows on top are ordinary functors, and the arrows on bottom are essential geometric morphisms. This may look more recognizable if I rewrite it like this:

    CLRAdj(E,Set)ESet C\frac{C \to LRAdj(E, Set)}{E \to Set^C}

    where LRAdj(E,Set)LRAdj(E, Set) denotes the category of functors ESetE \to Set which are simultaneously left and right adjoints, and the arrows on the bottom are functors that are simultaneously left and right adjoints.

    I was furthermore claiming that for any (small) category CC, that left-right adjoints ESet CE \to Set^C are the same as bicontinuous functors ESet CE \to Set^C. It could be a rash claim, but let’s see. I know that Grothendieck toposes are total categories, and this would mean that left adjoints ESet CE \to Set^C coincide with cocontinuous functors ESet CE \to Set^C. I guess I was also hoping that Grothendieck toposes are cototal. This I am less sure about, but it would mean dually that right adjoints ESet CE \to Set^C coincide with continuous functors. If that is true, then left-right adjoints ESet CE \to Set^C are the same as bicontinuous functors ESet CE \to Set^C.

    So let’s see: total category informs me (by dualizing) that any complete, well-powered category with a cogenerator is cototal. Well, Grothendieck toposes EE are complete and well-powered, and if SS is a set of objects that generates EE, then I assume that cSΩ c\prod_{c \in S} \Omega^c cogenerates EE. So for now that’s my argument that EE is cototal.

    So now we are down to checking that functors CBicont(E,Set)C \to Bicont(E, Set) are equivalent to bicontinuous functors ESet CE \to Set^C. I was hoping this was obvious: to check whether a functor f:ESet Cf: E \to Set^C preserves limits and colimits, it is enough to check that fev c:ESetf \circ ev_c: E \to Set preserves limits and colimits for every object cc of CC. This means that given bicontinuous f:ESet Cf: E \to Set^C, we can construct a functor CBicont(E,Set)C \to Bicont(E, Set) that sends cc to fev cf \circ ev_c. And so on.

    Summarizing: there should be an equivalence

    functors:CLRAdj(E,Set)leftrightadjoints:ESet C\frac{functors: C \to LRAdj(E, Set)}{left-right-adjoints: E \to Set^C}

    and this was supposed to justify the adjunction

    CTopos ess(Set,E) opSet CE\frac{C \to Topos_{ess}(Set, E)^{op}}{Set^C \to E}

    where CSet CC \mapsto Set^C is left adjoint to ETopos ess(Set,E) opE \mapsto Topos_{ess}(Set, E)^{op}.

    The unit of the adjunction CTopos ess(Set,Set C)C \to Topos_{ess}(Set, Set^C) is an equivalence precisely when CC is Cauchy complete. That gives the coreflection.

    • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeJul 26th 2011

    Hi Todd,

    thanks again, that does help.

    I was offline for a few hours (had to go to the cinema ;-). I’ll try to come back to this now, but maybe won’t get back to you before tomorrow morning.

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeJul 28th 2011
    • (edited Jul 28th 2011)

    Todd,

    after having managed to get myself distracted from this discussion here in all possible kinds of ways (as you will have seen) I would like to finalize this now.

    After having included much standard stuff from Borceux-Dejean into Cauchy complete category the other day I am now working on writing up the section In terms of essential geometric morphisms. I am doing this in a very explicit and pedestrian manner, since this is not just for me (not that I myself would not benefit from explicit and pedestrian discussion, of course, I am just saying this in case you are wondering why I am expanding your half-line remarks into lengthy arguments! :-).

    So far I have mainly the statement and proof that

    C¯Topos ess(Set,Set C) \overline{C} \simeq Topos_{ess}(Set, Set^C)

    Or do I? Because I get

    C¯Topos ess(Set,Set C) op. \overline{C} \simeq Topos_{ess}(Set, Set^C)^{op} \,.

    Could you maybe check that? Because I get that the equivalence proceeds by sending FC¯F \in \overline{C} to f *:=[C,Set](F,)f^* := [C,Set](F,-) and that means that a morphism FGF \to G is sent to a tranformation [C,Set](G,)[C,Set](F,)[C,Set](G,-) \to [C,Set](F,-) which is a geometric transformation gfg \to f.

    (Sorry if I am falling off the variance-log here once again :-)

    • CommentRowNumber18.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 28th 2011
    • (edited Jul 28th 2011)

    It’s Topos ess(Set,Set C) opTopos_{ess}(Set, Set^C)^{op}. I’m pretty sure I wrote that at some point, but I might have later forgotten to put in the op^{op}. Edit: yes I included it in the third sentence of comment 15, and elsewhere in that comment.

    • CommentRowNumber19.
    • CommentAuthorUrs
    • CommentTimeJul 28th 2011

    Okay, good. Thanks.

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeJul 28th 2011

    Okay, I have now typed up the remainded of the argument: still in the subsection In terms of essential geometric morphisms.

    • CommentRowNumber21.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 28th 2011
    • (edited Jul 28th 2011)

    By the way, I think I gave a needlessly complicated argument back in 15, because I didn’t need to get into all that cototality stuff. (Although I’m glad I did, because I learned something from it.)

    Namely, we can see the equivalence

    functors:CLRAdj(E,Set)left/rightadjoints:ESet C\frac{functors: C \to LRAdj(E, Set)}{left/right-adjoints: E \to Set^C}

    directly. Given a left/right-adjoint f:ESet Cf: E \to Set^C, we get for each object cc of CC a left/right-adjoint

    EfSet Cev cSetE \stackrel{f}{\to} Set^C \stackrel{ev_c}{\to} Set

    and so given such ff, we get a functor CLRAdj(E,Set)C \to LRAdj(E, Set) which sends ff to ev cfev_c \circ f. And given a functor g:CLRAdj(E,Set)g: C \to LRAdj(E, Set), we get for each object ee of EE a functor

    CgLRAdj(E,Set)ev eSetC \stackrel{g}{\to} LRAdj(E, Set) \stackrel{ev_e}{\to} Set

    and so given such gg, we get a functor ESet CE \to Set^C that sends ee to ev egev_e \circ g. This has both a left adjoint Set CESet^C \to E and a right adjoint Set CESet^C \to E. The left adjoint takes an object FF of Set CSet^C to the following object of EE:

    cl(c)(F(c)),\int^c l(c)(F(c)),

    where l(c)g(c)l(c) \dashv g(c). For a morphism cl(c)(F(c))e\int^c l(c)(F(c)) \to e corresponds to a wedge l(c)(F(c))el(c)(F(c)) \to e that is extranatural in cc, which corresponds to a family F(c)g(c)(e)F(c) \to g(c)(e) that is natural in cc, i.e., to a transformation Fev egF \to ev_e \circ g, as desired. Similarly, the right adjoint takes an object FF of Set CSet^C to the following object of EE:

    cr(c)(F(c)),\int_c r(c)(F(c)),

    where g(c)r(c)g(c) \dashv r(c). For a morphism e cr(c)(F(c))e \to \int_c r(c)(F(c)) corresponds to a wedge er(c)(F(c))e \to r(c)(F(c)) that is extranatural in cc, which corresponds to a family g(c)(e)F(c)g(c)(e) \to F(c) that is natural in cc, i.e., to a transformation ev egFev_e \circ g \to F, as desired.

    • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeJul 28th 2011

    But isn’t it even simpler? Both sides are evidently equivalent to functors C×ESetC \times E \to Set that preserve all limits and colimits in the second argument.

    • CommentRowNumber23.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 28th 2011

    But isn’t it even simpler?

    But see, that brings us back to my first argument. We would have to convince ourselves that a functor F:C×ESetF: C \times E \to Set has left and right adjoints for each F(c,)F(c, -) if and only if each F(c,)F(c, -) preserves limits and colimits. To get that equivalence, we need co/totality of EE (or something similar).

    • CommentRowNumber24.
    • CommentAuthorUrs
    • CommentTimeJul 28th 2011

    But we know that the adjoint functor theorem applies to functors between toposes by standard facts?! Sorry, I may be missing your point.

    • CommentRowNumber25.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 28th 2011

    Well, maybe I’m forgetting which standard facts. Could you tell me?

    My verification of cototality amounted to a verification of one set of hypotheses for an adjoint functor theorem to apply (that guarantees when a limit-preserving functor has a left adjoint). If you have something shorter in mind, please remind me.

    • CommentRowNumber26.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 28th 2011

    Just to add another comment to that: my second argument is purely conceptual, i.e., doesn’t rely on the technicalities of adjoint functor theorems. But I don’t mind – whichever way you’d prefer to do it is fine by me.

    • CommentRowNumber27.
    • CommentAuthorUrs
    • CommentTimeJul 28th 2011

    The adjoint functor theorem is known to hold for locally presentable categories (and accessible functors between them, I should add, but that’s okay for our case).

    I think this is Theorem 1.66 of J. Adamek, J. Rosicky, “Locally Presentable and Accessible Categories”. But let me try to look it up again.

    • CommentRowNumber28.
    • CommentAuthorUrs
    • CommentTimeJul 28th 2011

    Also corollary 5.5.2.9 in HTT

    • CommentRowNumber29.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 28th 2011
    • (edited Jul 28th 2011)

    Yes, but: you probably have in mind the version that guarantees existence of a right adjoint for a colimit-preserving functor. It is not in general true that a limit-preserving functor between locally presentable categories has a left adjoint. (Mike gave an example recently at MO of a limit-preserving functor GrpSetGrp \to Set that is not a right adjoint. I’ve fallen into this trap several times myself.) That’s why I went to the trouble of proving that toposes are cototal.

    Here is the link to Mike’s example.

    • CommentRowNumber30.
    • CommentAuthorUrs
    • CommentTimeJul 28th 2011

    By the way, I have been chatting about this (Cat CauchyTopos essCat_{Cauchy} \hookrightarrow Topos_{ess}) also with Benno, and he remarks:

    In the meantime I found “my own” proof: it identifies the Cauchy-completion C¯\overline{C} as the full subcategory of indecomposable projectives in [C op,Set][C^op, Set] and one check that the further left adjoint f !f_! sends indecomposable projectives to indecomposable projectives

    • CommentRowNumber31.
    • CommentAuthorUrs
    • CommentTimeJul 28th 2011
    • (edited Jul 28th 2011)

    It is not in general true that a limit-preserving functor between locally presentable categories has a left adjoint.

    I am thinking: it is if it is accessible. Which it is in our case, since it preserves even all colimits.

    • CommentRowNumber32.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 28th 2011

    Ah, okay, that works. Thanks.

    As I say: anyway you want to do it is fine. I still like my second argument, because the other way requires some bigger guns (which you call ’standard facts’ – you do have to argue, as you’ve just done).

    • CommentRowNumber33.
    • CommentAuthorUrs
    • CommentTimeJul 28th 2011

    Okay. But quite generally we need to record these things better on the nnLab.

    I have added to adjoint functor theorem

    1. the version for locally presentable categories;

    2. in the Examples-section: the statement about totality and cototality of toposes. There I say: See the discussion at topos. We should write out the arguments there.

    • CommentRowNumber34.
    • CommentAuthorUrs
    • CommentTimeJul 28th 2011

    Sorry, Grothendieck toposes.

    • CommentRowNumber35.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 28th 2011

    I added a proof for the assertion of totality and cototality in Grothendieck topos.

    • CommentRowNumber36.
    • CommentAuthorUrs
    • CommentTimeJul 28th 2011

    Thanks! I have added some hyperlinks. We should really move this discussion to a more dedicated entry, though.

    • CommentRowNumber37.
    • CommentAuthorMike Shulman
    • CommentTimeJul 29th 2011

    I wasn’t really following this discussion, unfortunately, but it seems to have come to a satisfactory conclusion. I like the observation that toposes are both total and cototal; it hadn’t entered my consciousness in that language before.