6
$\begingroup$

Is there a standard method for showing that a functor $F:\mathcal{C}\to\mathcal{D}$ is a fibration, aside from constructing a cleavage?

In the proof of the Grothendieck construction, the fibration we obtain from an indexed category $\Psi:\mathcal{B}^{op}\to\mathfrak{Cat}$ is automatically cloven since we're constructing a specific Cartesian arrow $(u,1_{\Psi(u)(Y)})$ for each arrow $u:I\to J\in\mathcal{B}$ and object $(J,Y)\in\int\Psi$ above $J$.

Every time I want to show that a functor is a fibration, I end up constructing Cartesian arrows parametrized as above and thusly showing that it's a cloven fibration -- is this by necessity?

Any method of showing that a functor is a fibration without choosing a cleavage is welcome, but in particular something similar to the adjoint functor theorem for fibrations would be cool. That is, a statement along the lines of

If $F:\mathcal{C}\to\mathcal{D}$ is a functor and $\mathcal{C}$ is blah and $\mathcal{D}$ is bloop and $F$ preserves/reflects blorps then $F$ is a fibration.

Improve this question
$\endgroup$
18
  • 1
    $\begingroup$ Just as an example, given a category $\mathcal{C}$ with finite limits, showing $\mathrm{cod}\colon \mathcal{C}^\mathbf{2} \to \mathcal{C}$ is a fibration does not involve choosing a cleaving. Any time that one uses a universal property to show the existence of a cartesian lift, then you aren't exactly constructing a cleaving, since you don't have to specify precisely which item with the universal property you are using. $\endgroup$
    – David Roberts ♦
    Jan 30, 2021 at 5:38
  • 2
    $\begingroup$ @AlecRhea: Showing that a pullback exists is different from choosing a pullback for every f, just like showing that a map is surjective is different from choosing a section (the latter requires the axiom of choice in general). $\endgroup$
    – Dmitri Pavlov
    Jan 30, 2021 at 6:13
  • 3
    $\begingroup$ @AlecRhea: there are two ways to say that a category $\mathcal{C}$ has pulbacks. As structure: there is a pullback-forming operation which takes a two arrows with a common codomain and gives a specific pullback diagram for them. As property: for any two arrows with a common codomain there exists a diagram which is a pullback of these arrows. If you use the latter, the codomain fibration twon't be cloven (unless you use the axiom of choice to can pass from property to structure). $\endgroup$
    – Andrej Bauer
    Jan 30, 2021 at 6:55
  • 1
    $\begingroup$ With that said, it is pretty rare to encounter non-cloven fibrations. Most naturally-occurring categories with pullbacks have specified pullbacks -- at least, if Set does, which it does in ZFC and DTT, and you can choose to assume it does in ETCS. The only examples I can think of offhand of categories with pullbacks but not specified pullbacks are where the morphisms are quotiented by something and the construction of a pullback depends on choosing representative morphisms, and it's rare for such quotiented categories to have pullbacks at all. $\endgroup$
    – Mike Shulman
    Feb 1, 2021 at 17:20
  • 1
    $\begingroup$ Also perhaps worth noting is that in homotopy type theory, any fibration between univalent categories is automatically cloven, because of the "unique choice principle" for functors. So one might argue that the existence of non-cloven fibrations is an artifact of the formulation of category theory in set theory. $\endgroup$
    – Mike Shulman
    Feb 1, 2021 at 17:21

1 Answer 1

Reset to default
9
$\begingroup$

Just as an example, given a category $\mathcal{C}$ with finite limits, showing $\mathrm{cod}\colon \mathcal{C}^\mathbf{2}\to \mathcal{C}$ is a fibration does not involve choosing a cleaving. All that you need is that a pullback square exists for each piece of relevant data. A cleaving would be a specified choice of pullback square for each cospan.

More generally, any time that one uses a universal property to show the existence of a cartesian lift, then you aren't exactly constructing a cleaving, since you don't have to specify precisely which item with the universal property you are using.

I'm thinking also of the result at the nLab page on Grothendieck fibrations:

A functor $p \colon E \to B$ is a cloven fibration if and only if the canonical functor $i \colon E \to B\downarrow p$ has a right adjoint $r$ in $\mathbf{Cat} / B$.

where instead of asking that that the adjoint is given, one just has that an adjoint functor theorem is applicable. "Constructing" the adjoint is (probably) equivalent to choosing a cleaving.

Improve this answer
$\endgroup$
3
  • 2
    $\begingroup$ I also generally recommend Streicher's notes on fibrations, in which he give a lot of material from Bénabou which was otherwise unpublished: Fibred Categories à la Jean Bénabou, arxiv.org/abs/1801.02927 $\endgroup$
    – David Roberts ♦
    Jan 30, 2021 at 7:08
  • 1
    $\begingroup$ A comment about my choice of terminology: the English word "cleaving" also translates to French "clivage" (if I trust DeepL and Google Translate) and is, to my mind, a better option than "cleavage". $\endgroup$
    – David Roberts ♦
    Jan 30, 2021 at 11:50
  • 1
    $\begingroup$ It just occurred to me why cleaving might be a better choice when talking about this with my girlfriend, thank you for the recommendation haha. $\endgroup$
    – Alec Rhea
    Jan 30, 2021 at 18:26

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.