The n-Category Café

Here is one of Blass’s proofs that the vanishing of the cohomology of all sets implies AC. Let $p:Y\to X$ be a surjection of sets, for which we want to find a section.

Suppose first that every fiber $Y_x = p^{-1}(x)$ is isomorphic to some fixed nonempty set $S$. Of course, if we were given specified isomorphisms $\phi_x:S \cong Y_x$ for all $x$, then we could fix a particular element $s\in S$ and define $f:X\to Y$ by $f(x) = \phi_x(s)$, but we are only assuming that such isomorphisms exist. (In HoTT language, they “merely” exist.)

In this special case, from a geometric point of view, we can consider $Y$ as a locally trivial bundle over $X$ with fiber $S$, and we know that such bundles are classified by the cohomology of the base with coefficients in the automorphism group of the fiber. Thus, if we let $G = Aut(S)$, we should be able to construct a “characteristic class” of $Y$ in $H^1(X;G)$.

The way to do this depends on the definition of $H^1$. Blass points out that many of the classical definitions are not correct in the absence of choice (his criterion of “correctness” being that they give rise to long exact sequences). He takes the route of simply defining $H^1(X;G)$ to be the set of isomorphism classes of $G$-torsors over $X$.

From a category-theoretic (or HoTT) point of view, it’s more natural to define $H^1(X;G)$ to be the set of natural isomorphism classes of functors $X\to \mathbf{B}G$, where $\mathbf{B}G$ is the one-object groupoid corresponding to $G$. It’s again easy to construct our characteristic class in this case, since for $G=Aut(S)$, the groupoid $\mathbf{B}G$ is equivalent to the groupoid $\mathbf{B}'G$, whose objects are sets isomorphic to $S$ and whose morphisms are all isomorphisms between them. Then $x\mapsto Y_x$ defines a functor from $X$ to $\mathbf{B}'G$, hence also to $\mathbf{B}G$.

(In ZF, this equivalence of groupoids is only a “weak equivalence”, i.e. there is a functor $\mathbf{B}G \to \mathbf{B}'G$ that is essentially surjective and fully faithful. Thus, our “functor” $X\to \mathbf{B}G$ is only an anafunctor, so we have to use those in the definition of cohomology. In HoTT, however, this is not a problem.)

Now by assumption, $H^1(X;G)=0$, so this characteristic class is trivial. This means that our functor $Y: X\to \mathbf{B}'G$ is naturally isomorphic to the one that is constant at $S$. Such a natural transformation assigns to each $x\in X$ an isomorphism $S\cong Y_x$, and as we remarked above this is sufficient to define a section of $p$.

This handles the special case when all the fibers of $p$ are isomorphic. In order to deal with the general case, Blass uses a trick: he defines $U$ to be the set of nonempty finite sequences of elements of $Y$, with $q:U\to X$ the function which selects the first element of a sequence and then maps it down to $X$ via $p$. Then the fiber $U_x$ is a subset of $U$, but there also exists an injection $U\hookrightarrow U_x$ that adjoins some fixed element of $Y_x$ at the front of each sequence. By the Schroeder-Bernstein theorem, therefore, $U\cong U_x$, and so we can apply the previous case to get a section of $q$, and hence (by selecting first elements) a section of $p$.

It’s important, of course, that the Schroeder-Bernstein theorem does not depend on the axiom of choice. It does, however, depend on the law of excluded middle, so we might wonder, is Blass’s theorem still valid constructively?

Now by a classical result of Bishop and Diaconescu, the axiom of choice implies the law of excluded middle. I will explain the proof in a moment; the crucial thing to note is that it only uses AC to obtain a section of a surjection all of whose fibers are isomorphic. Since the first part of Blass’s argument (when all fibers are isomorphic) seems perfectly constructive, it will therefore also imply LEM, so that the second part of the argument can freely use Schroeder-Bernstein.

Why does AC imply LEM? Suppose $P$ is a proposition for which we want to show “$P$ or not $P$”. Let $\Sigma P$ be the quotient of $2 = \{N,S\}$ by the equivalence relation which identifies $N\sim S$ exactly when $P$ holds. (In reproducing this proof in HoTT, Spitters and Rijke have observed that $\Sigma P$ is exactly the homotopy-theoretic suspension of $P$, hence the notation.) Then $p:2 \to \Sigma P$ is a surjection. If it has a section $f:\Sigma P \to 2$, then we can consider $f([N])$ and $f([S])$, each of which is either $N$ or $S$. This gives four cases, two of which easily imply $P$, and the other two of which easily imply “not $P$”.

Now what are the fibers of $p$? Every element of $\Sigma P$ is either $[N]$ or $[S]$ (though this is not necessarily an exclusive-or), so it suffices to show that the fibers over $[N]$ and $[S]$ are isomorphic. The fiber over $[N]$ always contains $N$, and it contains $S$ iff $P$. Similarly, the fiber over $[S]$ always contains $S$, and it contains $N$ iff $P$. Thus, the two are isomorphic by an isomorphism that interchanges $N$ and $S$.

Thus we recover, even constructively, Blass’s theorem that the vanishing of $H^1$ of sets is equivalent to the axiom of choice. Blass’s original theorem was actually sharper: the vanishing of $H^1(X;G)$ for all $G$ and a particular set $X$ is equivalent to projectivity of $X$. Can this sharper version also be obtained constructively? I don’t know.

Regardless, I think it’s quite cute that we can connect geometric ideas like characteristic classes of fiber bundles in cohomology with logical ideas like the axiom of choice. In some sense, this is what topos theory is supposed to be all about.