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.
I have a split fibration (it's actually the externalization of an internal category) where the induced pullback functors are themselves fibrations (probably all of them, but certainly the ones induced by monomorphisms). What does this mean?
I just found some more of them too!
One thing this does not give you is a consistent 3-way factorization system, because if you factor something you're going to get mini-vertical, mini-cartesian, cartesian and they'll probably all be nontrivial, but if you compose the mini-vertical and mini-cartesian and refactor, you will just get mini-cartesian because the cartesian will be id and you'll be working in the trivial mini-fibration. Now if only I knew what it does give you!
(What I'd love is to get a nice simple property of the internal categories that makes them externalize this way.)
What it gets you for the family fibration of ordinary categories:
This also tells me my "probably" was wrong and my examples are about monos.
Is there a nice way to tell if an internal category has pullbacks?
A note about this: the monic version isn't always trivial for internal categories! It means "sub-unary" pullbacks and if there are a lot of subterminal objects in your host category these can be varied, interesting, and far from guaranteed. So now I'm looking for a way to tell if an internal category has pullbacks without externalizing it so I can adapt it for these circumstances.
If your context category has enough structure to internalize the cospan diagram (most do) I imagine you can present it in terms of that? Might not be easy to check though.
Could also try to show the codomain map from the internal arrow category is a [[fibration in a 2-category]] of internal categories but I'm not sure exactly which notion of "pullbacks" this would verify and also it sounds maybe about as hard as externalizing ...
Okay I made a serious mistake earlier: pullbacks don't suffice to have pullback functors for, say, in be fibrations because the definition of fibration is too strict. Pullback functors like are some kind of lax Street fibrations described below. I think "sub-unary pullback" is still a decent word for what you get when pullback functors for monos are fibrations though--you just don't need the laxness, or even Streetness, in this case.
Lax Street fibrations: Consider a functor . Call a lax Cartesian lift of if and whenever in and in such that , there exists a unique such that and . is a Lax street fibration if every arrow in has a lax Cartesian lift.
In the spirit of this stream, has anybody heard of this before?
"Sub-unary pullbacks" at least means is injective, but there are extra universality conditions on the lift. In particular, if you factorize the square you're lifting in through (too many cods!!!!!) and then you make a third square by squishing that through the corresponding . Then lifts of the third square are in one-to-one correspondence with lifts of the second square that factor through both other lifts. This is a very involved condition and I'd like to make it nicer.
James Deikun said:
Lax Street fibrations: Consider a functor . Call a lax Cartesian lift of if and whenever in and in such that , there exists a unique such that and . is a Lax street fibration if every arrow in has a lax Cartesian lift.
In the spirit of this stream, has anybody heard of this before?
I have. Back in the first year of my PhD I worked with my then fellow PhD student @Riccardo Zanfa on this lax version of Street fibration. Riccardo has since left academia, and the results we got were probably original but sufficiently close to folklore that they didn't stand out on their own (even more so since I have spotted some of the minor results appearing on the nlab); the main thing that got in the way of it becoming a paper was that we didn't have any compelling applications for which there weren't already stronger results known. So I might as well share them in case we can claim a little credit..!
Given an adjunction between locally cartesian closed categories, going via local Frobenius reciprocity, we can show that is a Street fibration if and only if is locally cartesian closed. is a lax fibration for which the comparison morphisms ( in your notation) are epimorphisms if and only if is sublocally cartesian closed (the epis dualize to monos across the adjunction).
More generally, if is a functor between categories with pullbacks, $$F$$$ is a lax fibration if and only if it is a "local left adjoint", meaning that has an adjoint for every object .
Hope some of that is relevant to your situation!
Correct me if I'm wrong, but isn't a lax fibration if and only if it's a local left adjoint if and only if has pullbacks? It makes me wonder what happens with in general without the assumption of pullbacks.