Let $\mathcal C$ be a category with pullbacks, let $Arr(\mathcal C)$ be its arrow category. The functor $cod\colon Arr(\mathcal C)\to\mathcal C$ that takes an object of $Arr(\mathcal C)$, i.e. a morphism in $\mathcal C$, to its codomain is a canonical example of a Grothendieck fibration. The cartesian arrows are exactly the pullback squares.

There is an easy generalization of this fact. Take any category $\mathcal D$ a functor $F\colon D\to C$ and consider the comma category $id_{\mathcal C}\downarrow F$. The objects of $id_{\mathcal C}\downarrow F$ are arrows $g\colon c\to F(d)$, the morphisms are pairs $(f,h)$, where $f$ is a morphism in $\mathcal C$, $h$ is a morphism in $\mathcal D$ and $$ \require{AMScd} \begin{CD} c@>f>>c'\\ @VgVV@VVg'V\\ F(d)@>>F(h)>F(d') \end{CD} $$ commutes.

There is an obviously defined functor $cod_F\colon id_{\mathcal C}\downarrow F\to\mathcal D$ that takes $g\colon c\to F(d)$ to the $d$ object and a square like the one above to the $h$ morphism.

Note that $id_{\mathcal C}\downarrow id_{\mathcal C}\simeq Arr(\mathcal C)$ and that $cod_{id_{\mathcal C}}\simeq cod$.

Question: What is the appropriate reference for the fact that $cod_F$ is a fibration?

I need this fact in a paper I am writing, the paper is intended for an audience that will probably not accept that this is "easy to check" or something.

  • 2
    $\begingroup$ Shouldn't this follow from the pullback stability of Grothendieck fibrations? $\endgroup$
    – asdq
    Feb 17, 2020 at 12:42
  • $\begingroup$ @ArnaudD. What do you mean? The functor $\mathrm{cod}_F$ is the strict pullback of $\mathrm{cod}$ along $F$. $\endgroup$
    – Pece
    Feb 17, 2020 at 16:18
  • $\begingroup$ Yes, this works fine. The comma category is naturally a lax pullback, but every lax pullback is constructed as a strict pullback of an arrow category. $\endgroup$ Feb 17, 2020 at 16:24
  • $\begingroup$ @Pece Oh right, I hadn't thought of that. I was thinking about $\operatorname{cod}(F)$ as a "lax pullback" of $id_\mathcal{C}$ along $F$. $\endgroup$
    – Arnaud D.
    Feb 17, 2020 at 17:52
  • $\begingroup$ @asdq Yes, this is what I was missing. Thank you. If you convert your comment to an answer, I will be happy to accept it. $\endgroup$ Feb 17, 2020 at 20:42


You must log in to answer this question.

Browse other questions tagged .