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: Composition of fibrations

Max New (Jun 09 2022 at 13:17):

Can someone point me to a simple proof that fibrations in a 2-category compose? I'm using the definition that $p : E \to B$ is a fibration when $p \to dom(B/p)$ has a right adjoint in $K/B$ (where $K$ is the ambient 2-category).

The nlab only informs me that this is "easy to show" :rolling_eyes:

Jonathan Weinberger (Jun 09 2022 at 17:20):

Different setting, but @Ulrik Buchholtz and I show in Synthetic fibered (∞, 1)-category theory, Prop. 3.2.7, that in general fibrations defined by a left adjoint right inverse (or, dually, right adjoint right inverse) condition compose, such as in particular cocartesian fibrations.
Note that here, we are using the other characterization namely that $E^{\Delta^1} \to p \downarrow B$ has a left adjoint right inverse (or, for the contravariant case $E^{\Delta^1} \to B \downarrow p$ has a right adjoint right inverse).
We work in simplicial homotopy type theory due to Riehl--Shulman (cf. A type theory for synthetic ∞-categories), but I'd think the argument can be adapted in a reasonable way.

Mike Shulman (Jun 09 2022 at 18:51):

I think it's much easier to show using a different definition. You can prove that fibrations in Cat compose by lifting a cartesian arrow over a cartesian arrow, and then if you define fibrations in a 2-category representably it follows immediately therein.

Jonathan Weinberger (Jun 09 2022 at 22:05):

@Mike Shulman Good point!

Max New (Jun 10 2022 at 14:54):

That's very nice, @Mike Shulman , but I am really looking at a slight variation on the definition of fibration so I was hoping an abstract proof would generalize easily to my situation.

Max New (Jun 10 2022 at 14:58):

I tried doing it manually and I came up with the following diagram: Screen-Shot-2022-06-10-at-10.54.30-AM.png

For the composite to be a fibration, I need the top to have a right adjoint over $B$ and we know the left and bottom triangles are right adjoints over $E$ and $B$ so it seems like there should be some diagrammatic pasting argument that the top right should similarly work and then we can just compose adjoints together.