You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Hi all,
@Robin Jourde and I just proved that the pullback of two functors between complete categories is again complete if one of the two functors is a continuous fibration.
Does anyone know a reference for this, please?
And the other functor isn't necessarily even continuous? That would be surprising to me.
We didn't use it, but of course we could've made a mistake. I've TeXed a proof sketch, so it's easy for me to submit it to your scrutiny.
Sure, post it or send it or anything.
Here it is, sorry don't have time to fix the citations right now, but both are Makkai and Paré.
main.pdf
Proposition 1.3 in Classifying Topos, by Giraud. It is stated for finitely complete categories, but the same proof goes through for complete ones.
Oh, of course. Yes, that works. Here's another proof: a continuous fibration is equivalent to a pseudofunctor to the 2-category of complete categories and continuous functors. Evidently such a pseudofunctor can be precomposed with any functor .
That's ridiculously simple! Thanks, @Mike Shulman.
A bit late but here's an alternative perspective which might also be enlightening (and which I'm hoping other people can enlighten me more on!). I've been thinking a lot about fibrations internal to 2-categories as part of some recent work on logical relations, so have stumbled across similar results and been trying to use my joint work with @Nathanael Arkor and Andrew Slattery to generalise them to the framework of relative pseudomonads. It's not as quick as Mike's argument but there are some things you can say.
The first thing you can observe quite easily is that if you have a relative pseudomonad on a pseudofunctor into a 2-category then a fibration in the 2-category of pseudoalgebras and algebra pseudomaps is exactly an algebra pseudomap whose underlying 1-cell is a fibration in the base .
Next, if has pullbacks (in the strict, 2-categorical sense) and you have
Then:
The construction basically follows the familiar construction for eg cartesian products: morally you apply the universal property of the fibration to the 2-cell given by the colax morphism structure of . (In actuality you also post-compose this with the 2-cell given by the lax morphism structure of , but in the pseudo case this doesn't do much.)
I have not checked the details of Tom's particular example but I believe this covers that, and lots of other limit-like ones, because (1) for limits any functor is an oplax algebra map, and (2) in limit-like cases where the pseudomonad is often lax-idempotent, there are ways to upgrade a colax algebra structure to a pseudo one.
For me this goes some way to explaining the somewhat-surprising fact that you don't need any conditions on the functor you're pulling back along: it boils down to the fact any functor is a colax algebra map, and hence to some "property-likeness" in the sense of Kelly and Lack.
What I don't understand is the general picture, namely why being a fibration is sufficient for pullbacks to exist even though they are typically too strict for 2-categories of pseudoalgebras. Possibly it is linked to Mike's work with Steve Lack on limits for lax morphisms? I am not sure but would like to know what's going on from a more conceptual perspective! I'd also like to understand why you can get CCC structure using these kinds of results, but as it stands I don't know how to state that at all. (Usually these results require pullbacks, ie products / algebra structure existing in certain slices / comma objects, which may be relevant...?)
Nice, thanks @Philip Saville!
Something that further bothers me is that in our proof I don't think we need the base to be complete, while I think it is needed to transport the continuity hypotheses from fibrations to indexed categories and back in Mike's proof, right?
Yes, my proof does assume that.
ah in fact in my argument it's sufficient for the base to have either lax or oplax algebra structure, because it doesn't really turn up in the proof -- the argument almost solely uses the algebra structure of or the algebra structure of . I stated it with pseudo because it felt a bit strange having it weaker, but maybe the weaker assumption is actually the natural one because it avoids having to ask for the base to be complete...