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: learning: questions

Topic: base change functor

David Egolf (he/him) (Sep 29 2025 at 00:27):

Let $f:X \to Y$ be a morphism in a category $C$ with pullbacks. Then the nLab tells me that there is an induced functor $f^\ast:C/Y \to C/X$ . Intuitively, this "pulls back" a morphism to $Y$ along $f$ to get a morphism to $X$ .

However, this is a bit confusing to me! If there are multiple pullbacks for the same diagram, then does getting a functor $f^\ast$ require choosing specific pullbacks? That sounds inconvenient!

If one does need to choose a bunch of specific pullbacks to really specify $f^\ast$ as a functor, then does it matter which ones are picked?

Or perhaps one can get away with not really specifying $f^\ast$ , except up to natural isomorphism? I'm hoping that all possible specific choices of pullbacks lead to naturally isomorphic functors. So then perhaps one can just imagine that some choice of pullbacks was made, without bothering about really making such a choice - and then just to try to set up arguments so that the specific choice of $f^\ast$ never matters?

Any thoughts appreciated!

Mike Shulman (Sep 29 2025 at 00:38):

This is a well-known issue for functors determined by universal properties.

Yes, to get a functor in the usual sense requires having a choice of specific pullbacks.
Many categories with pullbacks come with pre-chosen specified pullbacks, coming from a constructive proof that the category has pullbacks. For instance, if the foundational theory is ZFC, then in Set you can take the specific pullbacks that are a subset of a cartesian product.
If for some reason you have a category that has pullbacks but not specified ones, which is rare but can happen, then yes, you need the axiom of choice to create a pullback functor. This is related to the fact that "every fully faithful and essentially surjective functor is an equivalence of categories" is equivalent to the axiom of choice.
It doesn't matter which pullbacks you pick, up to isomorphism: any other choice will give a naturally isomorphic pullback functor, as you guessed. So if you are working "categorically" with everything only needed to be defined up to isomorphism, then yes, any result you get won't care which choices you made -- except that to have a true functor you need some pullbacks, such as from a concrete construction or the axiom of choice.
If you want to avoid the axiom of choice and work with categories that don't have specified pullbacks, you can talk about [[anafunctors]] instead of functors, which are functors whose values are "determined only up to unique isomorphism" without needing to make any specific choice.
Finally, if you choose HoTT/UF as your foundational theory instead of set theory, and work with univalent categories, then the uniqueness-up-to-isomorphism of pullbacks implies uniqueness-up-to-equality, and therefore there is a unique pullback functor, by the function comprehension principle (unique choice principle).

Josselin Poiret (Sep 29 2025 at 09:36):

one more thing around this question: in the abstract case, even if you have specified choices of pullbacks for every morphism $f$ , these will not arrange into a 1-functor into Cat, only a 2-functor. You could additionally require that the choice of pull-backs that you get with your category does compose strictly, and get a 1-functor. This is a version of the notion of [[split fibration]]

Nathanael Arkor (Sep 29 2025 at 11:17):

It's worth specifying that by "2-functor", you mean "weak 2-functor" or "pseudofunctor", because (outside the nLab), "2-functor" typically refers to the strict notion.

Josselin Poiret (Sep 29 2025 at 11:52):

yes, apologies, I always forget the fact that the strict version even exists

David Egolf (he/him) (Sep 29 2025 at 17:37):

Thanks, that's interesting and helpful!

Mike Shulman said:

If for some reason you have a category that has pullbacks but not specified ones, which is rare but can happen...

I hadn't realized that we'd often have specified pullbacks! For example, I suppose that in any presheaf topos we can get specified pullbacks by computing the pullback "object-wise". When evaluating at any object, our diagram of presheaves becomes a diagram of sets, and then we can compute a pullback there using the usual specific pullback for $\mathsf{Set}$ .

Kevin Carlson (Sep 29 2025 at 18:14):

Yes, and then in any reflective subcategory of a presheaf category, which is a whole lot of important categories, you can inherit the explicit pullbacks from the big category.

Mike Shulman (Sep 29 2025 at 18:27):

Basically the only naturally-occurring categories I know of that have pullbacks but not specified ones are "homotopy categories", where the morphisms are equivalence classes. Usually in that case you have to pick representatives of the equivalence classes in order to determine a pullback, while different choices will produce a different pullback object (though, of course, one that is isomorphic in the homotopy category), so the pullbacks aren't specified given only a cospan in the homotopy category.

This is especially rare because the homotopy categories that arise naturally in homotopy theory don't have pullbacks (although they have weak pullbacks). But there are a few homotopy-category-like constructions that do end up having pullbacks, such as some constructions of regular or exact completions.