11
$\begingroup$

It is well known that (working over ZF) AC implies that every fibration $p:\mathcal{E}\to\mathcal{B}$ can be equipped with a cleavage by choosing, for each arrow $u:I\to p(X)$ in the base category whose codomain is in the image of the fibration, a Cartesian arrow $\overline u(X):u^*(X)\to X$ in the overcategory above $u$ whose codomain is $X$.

Does the reverse implication hold?

Andrej Bauer mentions in this MO answer that he suspects the converse holds; I was wondering if anyone had a proof on hand.

$\endgroup$
8
  • 2
    $\begingroup$ Is this the same as asking if AC is equivalent to the axiom of choice for collections of sets which all have the same cardinality (i.e. for any two sets in the collection, there exists a bijection between them)? $\endgroup$
    – Will Sawin
    Commented Jan 20, 2021 at 0:19
  • $\begingroup$ @WillSawin Not that I can tell, but perhaps you're seeing something I'm not? The sets of Cartesian arrows parametrized by arrows in the base category and objects above their codomains in the overcategory need not have the same cardinality, unless I'm missing something. $\endgroup$
    – Alec Rhea
    Commented Jan 20, 2021 at 2:00
  • 2
    $\begingroup$ @Will: Yes. Given any collection of non-empty sets, $\{A_i\mid i\i I\}$, let $\alpha$ be an ordinal such that $A_i\subseteq V_\alpha$ for all $i$, and consider $\{A_i\times V_\alpha\mid i\in I\}$. Since $V_\alpha$ is equipotent with its square, all those sets are of the same cardinality: $|V_\alpha|$. Now if $F$ is a choice function from this family, we easily get a choice function for the original family by composing with the left projection. $\endgroup$
    – Asaf Karagila
    Commented Jan 20, 2021 at 16:34
  • $\begingroup$ @AsafKaragila That is cool, but how is this related to my question? I'm not salty, I enjoyed reading your comment, but I don't see the connection Will made between my question and the question about choice for equipotent sets. $\endgroup$
    – Alec Rhea
    Commented Jan 20, 2021 at 17:59
  • 1
    $\begingroup$ @AsafKaragila I'm trying to understand what connection Will saw between my question and the question he asked me; you answered his question with a yes, so I thought you sa the same connection he did. Your comment seems to be answering yes to the question "is choice for equipotent sets equivalent to full choice", but I never asked about choice for equipotent sets and I still don't see what connection Will saw without going through the construction given by Simon to go from your answer connecting equipotent choice to my question about fibrations. Am I missing something? $\endgroup$
    – Alec Rhea
    Commented Jan 20, 2021 at 18:18

1 Answer 1

17
$\begingroup$

Yes, in fact Grothendieck fibration between groupoids are enough.

Let $p:Y \to X$ be any surjection.

We construct the following groupoid $G$. Its set of objects is $X \amalg Y$. Its morphisms corresponds to the equivalence relation such that two elements of $y$ are equivalent if they have the same image by $p$ and an element of $y$ is equivalent to its image by $p$ in $X$ (and no distinct elements of $X$ are equivalent).

We then consider $I$ the walking isomorphisms, i.e. the anti-discrete groupoid on two objects, and the functor $G \to I$ that sends element of $Y$ on one object and element of $X$ on the other.

I claim that:

  1. it is a fibration. (easy to check)
  2. a cleavage produces a section of $p$: for each $x \in X$ a cartesian lift of the non-identity arrow $e \to p(x)$ corresponds to the choice of a $y \in Y$ such that $p(y)=x$.

Remark: a more conceptual way to understand this is that a fibration over $I$ is the same as an "anaequivalence" (in the sense of Makkai anafunctors) and a cleavage for such a fibration gives choice of a pair of inverse functors implementing this equivalence. So "anyfibration admit a cleavage" implies that every anaequivalence is implemented by a pair of inverse functor, and in particular that every fully faithful essentially surjective functor has an inverse. We then combine this with the usual proof that the existence of inverse functors imply the axiom of choice.

$\endgroup$
1
  • $\begingroup$ Very nice, thank you Simon. $\endgroup$
    – Alec Rhea
    Commented Jan 20, 2021 at 6:11

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .