The domain functor is a fibration

category-theoryfibration

I'm learning about fibrations and I read that the functor $dom: C^{\rightarrow} \rightarrow C$ is one for arbitrary category $C$. I can't see it.

I need to show that any morphism in $C^{\rightarrow}$ is (for now just weakly) cartesian wrt $dom$. According to Zhang, it should follow merely from the fact that morphisms in $C^{\rightarrow}$ are commutative squares.

Letting $s \in C^{\rightarrow}[b, a]$ be such a morphism with $dom(s) = f$. I need to show that if $s' \in C^{\rightarrow}[b', a]$ is another such morphism with $dom(s') = f$, then there is a unique morphism $t
\in C^{\rightarrow}[b', b]$
with $dom(t) = 1$ and $s' = s \circ t$. Where does the arrow $cod(t)$ in $C$ come from?

enter image description here

Best Answer

It's crucial to remember that fibrations over $C$ are exactly the Grothendieck constructions of contravariant (pseudo)functors from $C$ to $\mathrm{Cat},$ with the fibers of the fibration corresponding to the values of the functor. Indeed, this is really how people ought to define fibrations, with the usual definition as a characterization, since the usual definition is so hard to grasp at first.

So, what is the fiber of $\mathrm{dom}$ over some $c\in C$? It's the class of arrows with domain $c$ and commutative squares whose domain component is $\mathrm{id}_c.$ That is, the fiber is precisely the slice category $c/C.$ And we have a very simple pseudofunctor out of $C^{\mathrm{op}}$ sending $c\mapsto c/C$ and $f:c\to c'$ to the functor $c/C\to c'/C$ given by precomposition with $f.$ In fact, this happens to be a strict functor into $\mathrm{Cat}.$

For my money, that's all you should realize to understand how $\mathrm{dom}$ is a fibration. You may well find it easier to work out the proof that the Grothendieck construction of an arbitrary functor into $\mathrm{Cat}$ is a fibration than to work it out in this particular case.