Category Theory
Zulip Server
Archive

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.

Stream: theory: category theory

Topic: Reference request for completeness of pullback category

Tom Hirschowitz (Jun 20 2025 at 14:51):

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?

Mike Shulman (Jun 20 2025 at 17:17):

And the other functor isn't necessarily even continuous? That would be surprising to me.

Tom Hirschowitz (Jun 20 2025 at 19:30):

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.

Mike Shulman (Jun 20 2025 at 20:07):

Sure, post it or send it or anything.

Tom Hirschowitz (Jun 21 2025 at 06:29):

Here it is, sorry don't have time to fix the citations right now, but both are Makkai and Paré.
main.pdf

Adrian Clough (Jun 21 2025 at 09:04):

Proposition 1.3 in Classifying Topos, by Giraud. It is stated for finitely complete categories, but the same proof goes through for complete ones.

Mike Shulman (Jun 21 2025 at 15:49):

Oh, of course. Yes, that works. Here's another proof: a continuous fibration $B\to C$ is equivalent to a pseudofunctor $C^{\rm op} \to \rm Cplt$ to the 2-category of complete categories and continuous functors. Evidently such a pseudofunctor can be precomposed with any functor $A\to C$.

Tom Hirschowitz (Jun 22 2025 at 08:03):

That's ridiculously simple! Thanks, @Mike Shulman.

Philip Saville (Jul 02 2025 at 17:13):

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 $T$ on a pseudofunctor $J : \mathcal{A} \to \mathcal{C}$ into a 2-category $\mathcal{C}$ then a fibration in the 2-category $T\text{-}\mathrm{Alg}$ of pseudoalgebras and algebra pseudomaps is exactly an algebra pseudomap whose underlying 1-cell is a fibration in the base $\mathcal{C}$.

Next, if $\mathcal{C}$ has pullbacks (in the strict, 2-categorical sense) and you have

• a lax morphism of pseudoalgebras $(p, \overline{p}) : (E, (-)^e, \hat{e}, \tilde{e}) \to (B, (-)^b, \hat{b}, \tilde{b})$
• a colax morphism of pseudoalgebras $(f, \overline{f}) : (A, (-)^a, \hat{a}, \tilde{a}) \to (B, (-)^b, \hat{b}, \tilde{b})$

Then:

1. The pullback $P$ of $p$ along $f$ acquires a colax algebra structure such that the arrow $P \to A$ becomes a strict algebra morphism and the arrow $P \to E$ becomes a colax algebra morphism.
2. Moreover, if $(p, \overline{p})$ is a pseudomorphism of algebras then this makes $P$ into a pullback in the 2-category of colax algebras and colax algebra maps.

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 $f$. (In actuality you also post-compose this with the 2-cell given by the lax morphism structure of $p$, 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...?)

Tom Hirschowitz (Jul 03 2025 at 06:33):

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?

Mike Shulman (Jul 03 2025 at 06:35):

Yes, my proof does assume that.

Philip Saville (Jul 03 2025 at 07:32):

ah in fact in my argument it's sufficient for the base $B$ 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 $A$ or the algebra structure of $E$. I stated it with $B$ 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...