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

Matteo Capucci (he/him) (Dec 08 2021 at 14:30):

Morphisms of fibrations are usually taken to be commutative squares where the top horizontal arrow preserves cartesian arrows:
image.png

Matteo Capucci (he/him) (Dec 08 2021 at 14:32):

On the other hand, one could define morphisms of fibrations as follows:
image.png

Matteo Capucci (he/him) (Dec 08 2021 at 14:32):

I could expect the two definitions to be actually equivalent, but are they?

Joe Moeller (Dec 08 2021 at 15:51):

I think this basically amounts to the fact that Fib is 2-fibered over Cat, and the fibers are Fib(X).

Mike Shulman (Dec 08 2021 at 16:43):

Or, in lower-brow language, the universal property of pullbacks?

dusko (Dec 09 2021 at 00:55):

Matteo Capucci (he/him) said:

On the other hand, one could define morphisms of fibrations as follows:
image.png

did you try to compute $F^*{\cal B}$, just to see what you mean? if it is a strict pullback, then it is equivalent by the definition of pullbacks, but you are being evil looking for objects $x$ and $b$ such thast $Fx=Qb$. if you want them to be isomorphic, then there are situations when coherence problems arise. (eg, take $\cal Y$ to be a group, and make sure that $Q$ does not split...)) if $F^*{\cal B}$ is a comma, then try to categorify the Hurewitz liftings, and you will see where grothendieck came from when he defined fibrations.

but where did you get that square as a definition of fibration morphisms? even if we take $F$ to be the identity, the functor $H$ may make the triangle commute, but may not preserve the cartesian liftings, and the fact that $Q$ is a fibration is lost to it.

Mike Shulman (Dec 09 2021 at 00:57):

I assumed that he simply didn't write the condition of preserving cartesian arrows, since it's present in both versions of the definition.

Mike Shulman (Dec 09 2021 at 00:57):

And fortunately, the pullback of a fibration is also a bipullback, so there's no harm in being "evil" here.

dusko (Dec 09 2021 at 01:03):

sorrh, but that sounds like a bit of theology. strict pullbacks of functors are ok because they are also bipullbacks. does that bring the strict pullback of two functors into existence without comparing their object parts?

dusko (Dec 09 2021 at 01:04):

((oops, it is 2am here. i'll check back.)) :sleeping:

Matteo Capucci (he/him) (Dec 09 2021 at 16:03):

The question (sorry if that's not explicit in the op) is indeed whether the 'upper' part of the second kind of morphisms automatically preserves cartesian arrows

Matteo Capucci (he/him) (Dec 09 2021 at 16:04):

dusko said:

but where did you get that square as a definition of fibration morphisms?

This is what you get by Grothendieck construction of $Fib : Cat^{op} \to Cat$ which sends a category X to the category Fib(X) of fibrations over it.
Maybe I can answer the question above myself: $H$ preserves cartesian arrows exactly if I ask morphisms in Fib(X) to preserve cartesian arrows

Joe Moeller (Dec 09 2021 at 20:11):

This is precisely what I was thinking with my sorta thoughtless answer.

Mike Shulman (Dec 09 2021 at 21:15):

Yes, in both ways of phrasing the definition you have to explicitly require the functor to preserve cartesian arrows.