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: deprecated: id my structure

Topic: fibrations in my fibrations


view this post on Zulip James Deikun (Jan 19 2023 at 22:18):

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?

view this post on Zulip James Deikun (Jan 20 2023 at 00:51):

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!

view this post on Zulip James Deikun (Jan 20 2023 at 01:16):

(What I'd love is to get a nice simple property of the internal categories that makes them externalize this way.)

view this post on Zulip James Deikun (Jan 20 2023 at 06:07):

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?

view this post on Zulip James Deikun (Jan 20 2023 at 11:56):

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.

view this post on Zulip Morgan Rogers (he/him) (Jan 20 2023 at 15:00):

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.

view this post on Zulip James Deikun (Jan 20 2023 at 17:12):

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 ...

view this post on Zulip James Deikun (Jan 20 2023 at 22:19):

Okay I made a serious mistake earlier: pullbacks don't suffice to have pullback functors for, say, !:21!: 2 \to 1 in Fam(C)\mathrm{Fam}(C) 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.

view this post on Zulip James Deikun (Jan 20 2023 at 22:32):

Lax Street fibrations: Consider a functor p:EBp : E \to B. Call ϕ:ee,h:p(e)b\phi : e' \to e, h : p(e') \to b a lax Cartesian lift of f:bp(e)f : b \to p(e) if p(ϕ)=fhp(\phi) = f \circ h and whenever ψ:ee\psi : e'' \to e in EE and g:p(e)bg : p(e'') \to b in BB such that fg=p(ψ)f \circ g = p(\psi), there exists a unique χ:ee\chi : e'' \to e' such that ψ=ϕχ\psi = \phi \circ \chi and hp(χ)=gh \circ p(\chi) = g. pp is a Lax street fibration if every arrow in BB has a lax Cartesian lift.

In the spirit of this stream, has anybody heard of this before?

view this post on Zulip James Deikun (Jan 21 2023 at 14:32):

"Sub-unary pullbacks" at least means codC:C1C0\mathrm{cod}_C : C_1 \to C_0 is injective, but there are extra universality conditions on the lift. In particular, if you factorize the square you're lifting in through cod:(πcod:C1C1)cod\mathrm{cod} : (\pi_{\mathrm{cod}} : \overrightarrow{C}_1 \to C_1) \to \mathrm{cod} (too many cods!!!!!) and then you make a third square by squishing that through the corresponding dom\mathrm{dom}. 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.

view this post on Zulip Morgan Rogers (he/him) (Jan 21 2023 at 16:28):

James Deikun said:

Lax Street fibrations: Consider a functor p:EBp : E \to B. Call ϕ:ee,h:p(e)b\phi : e' \to e, h : p(e') \to b a lax Cartesian lift of f:bp(e)f : b \to p(e) if p(ϕ)=fhp(\phi) = f \circ h and whenever ψ:ee\psi : e'' \to e in EE and g:p(e)bg : p(e'') \to b in BB such that fg=p(ψ)f \circ g = p(\psi), there exists a unique χ:ee\chi : e'' \to e' such that ψ=ϕχ\psi = \phi \circ \chi and hp(χ)=gh \circ p(\chi) = g. pp is a Lax street fibration if every arrow in BB 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 FRF \dashv R between locally cartesian closed categories, going via local Frobenius reciprocity, we can show that FF is a Street fibration if and only if RR is locally cartesian closed. FF is a lax fibration for which the comparison morphisms (h:p(e)bh:p(e') \to b in your notation) are epimorphisms if and only if RR is sublocally cartesian closed (the epis dualize to monos across the adjunction).
More generally, if FF is a functor between categories with pullbacks, $$F$$$ is a lax fibration if and only if it is a "local left adjoint", meaning that F/XF/X has an adjoint for every object XX.
Hope some of that is relevant to your situation!

view this post on Zulip James Deikun (Jan 22 2023 at 15:06):

Correct me if I'm wrong, but isn't Δ:CC×C\Delta : C \to C \times C a lax fibration if and only if it's a local left adjoint if and only if CC has pullbacks? It makes me wonder what happens with (F,F)(F,F) in general without the assumption of pullbacks.