Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

July 28, 2013

Cohomology Detects Failures of Classical Mathematics

Posted by Mike Shulman

Ordinarily I try to avoid cross-posting between here and the Homotopy Type Theory blog, but this remark seems probably of interest to the crowd here as well. After my recent post there about how to define cohomology in HoTT, Zhen Lin kindly pointed me to a very nice paper of Andreas Blass called Cohomology detects failures of the axiom of choice. A main result of this paper is that the following two statements are equivalent (over ZF):

  • The axiom of choice.
  • For any discrete set XX and any (not necessarily abelian) group GG, the cohomology H 1(X;G)H^1(X;G) vanishes.

The fact that discrete spaces have no higher cohomology is “obvious” in classical algebraic topology, but this shows that if we want to do homotopy theory “constructively” then we need to give up that expectation. In this post I want to explain one of Blass’s proofs from a geometric point of view, and then consider what cohomology has to say about the law of excluded middle.

Here is one of Blass’s proofs that the vanishing of the cohomology of all sets implies AC. Let p:YXp: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)Y_x = p^{-1}(x) is isomorphic to some fixed nonempty set SS. Of course, if we were given specified isomorphisms ϕ x:SY x\phi_x:S \cong Y_x for all xx, then we could fix a particular element sSs\in S and define f:XYf:X\to Y by f(x)=ϕ x(s)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 YY as a locally trivial bundle over XX with fiber SS, 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)G = Aut(S), we should be able to construct a “characteristic class” of YY in H 1(X;G)H^1(X;G).

The way to do this depends on the definition of H 1H^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)H^1(X;G) to be the set of isomorphism classes of GG-torsors over XX.

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

(In ZF, this equivalence of groupoids is only a “weak equivalence”, i.e. there is a functor BGBG\mathbf{B}G \to \mathbf{B}'G that is essentially surjective and fully faithful. Thus, our “functor” XBGX\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)=0H^1(X;G)=0, so this characteristic class is trivial. This means that our functor Y:XBGY: X\to \mathbf{B}'G is naturally isomorphic to the one that is constant at SS. Such a natural transformation assigns to each xXx\in X an isomorphism SY xS\cong Y_x, and as we remarked above this is sufficient to define a section of pp.

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

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 PP is a proposition for which we want to show “PP or not PP”. Let ΣP\Sigma P be the quotient of 2={N,S}2 = \{N,S\} by the equivalence relation which identifies NSN\sim S exactly when PP holds. (In reproducing this proof in HoTT, Spitters and Rijke have observed that ΣP\Sigma P is exactly the homotopy-theoretic suspension of PP, hence the notation.) Then p:2ΣPp:2 \to \Sigma P is a surjection. If it has a section f:ΣP2f:\Sigma P \to 2, then we can consider f([N])f([N]) and f([S])f([S]), each of which is either NN or SS. This gives four cases, two of which easily imply PP, and the other two of which easily imply “not PP”.

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

Thus we recover, even constructively, Blass’s theorem that the vanishing of H 1H^1 of sets is equivalent to the axiom of choice. Blass’s original theorem was actually sharper: the vanishing of H 1(X;G)H^1(X;G) for all GG and a particular set XX is equivalent to projectivity of XX. 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.

Posted at July 28, 2013 5:43 AM UTC

TrackBack URL for this Entry:

9 Comments & 0 Trackbacks

Re: Cohomology Detects Failures of Classical Mathematics

Nice! Are there structures other than discrete sets whose cohomology fails to behave as expected when the axiom of choice doesn’t hold? For example, algebraic gadgets of some sort?

I would imagine so, but my memory only conjures forth the Whitehead problem, “is every abelian group AA with Ext 1(A,)=0Ext^1(A,\mathbb{Z}) = 0 free?” This sounds vaguely choice-ish, since it’s about surjections and whether they split: it’s equivalent to “if every surjection f:BAf: B \to A with kernel \mathbb{Z} splits, is AA free?” But it’s independent of ZFC and related to more subtle axioms of set theory.

So, now I want to know quite generally: “What axioms of set theory does cohomology detect?”

Cohomology can be regarded as the art of counting holes, so we should use it to locate holes in the foundations of mathematics.

Posted by: John Baez on July 29, 2013 4:39 AM | Permalink | Reply to this

Re: Cohomology Detects Failures of Classical Mathematics

Perhaps the cohomology of a classifying topos of some of the set theory axioms could do it…

Posted by: David Roberts on July 29, 2013 6:24 AM | Permalink | Reply to this

Re: Cohomology Detects Failures of Classical Mathematics

…the Whitehead problem.

Talking of Whitehead, shouldn’t his theorem be relevant to this post. As Mike once said

Now I think we can think of Whitehead’s theorem as a “classicality” axiom which can fail in (,1)(\infty,1)-topoi, akin to the law of excluded middle and the axiom of choice (which can already fail in 1-topoi).

Anything cohomological there?

Posted by: David Corfield on July 29, 2013 7:35 AM | Permalink | Reply to this

Re: Cohomology Detects Failures of Classical Mathematics

Yeah, I’ve also been wondering whether the failure of Whitehead’s theorem could be detected cohomologically. However, it seems a bit unlikely, because cohomology is basically the homotopy groups of mapping spaces, while the failure of Whitehead’s theorem means precisely that there are things that can’t be detected by homotopy groups. (-: However, it’s conceivable that there’s some way to massage a failure of Whitehead’s theorem into some other invariant, that could be detected by homotopy groups.

Posted by: Mike Shulman on July 30, 2013 6:54 PM | Permalink | Reply to this

Re: Cohomology Detects Failures of Classical Mathematics

Good question! Here’s another example that came up recently in another thread. Classically, Ext n(A,B)Ext^n(A,B) for abelian groups AA and BB vanishes when n>1n\gt 1, but it seems unlikely to me that this will be the case without choice. Of course there is the question of the correct definition of Ext n(A,B)Ext^n(A,B). My current inclination is that the correct definition in homotopy type theory will be Ext n(A,B)=π nHom H(HA,HB).Ext^n(A,B) = \pi_{-n} Hom_{H\mathbb{Z}}(H A, H B). That is, the ExtExt groups are the (cohomologically reindexed) homotopy groups of a mapping spectrum of HH\mathbb{Z}-module spectra. (Here HAH A, for an abelian group AA, denotes the Eilenberg-Mac Lane spectrum with (HA) n=K(A,n)(H A)_n = K(A,n).) This is correct in classical mathematics, although many people might find it somewhat perverse as a definition.

To identify it with the more common definitions, we use the fact that HH\mathbb{Z}-modules are equivalent to unbounded chain complexes of abelian groups. Then the facts that free abelian groups are projective, and subgroups of free abelian groups are free abelian, imply that every abelian group has a 2-term projective resolution, causing Ext n(A,B)=0Ext^n(A,B)=0 for n>1n\gt 1. However, it seems unlikely to me that any of these facts is true constructively.

There is a slight obstacle in that we don’t currently know how to define HH\mathbb{Z}-modules or their mapping spaces in homotopy type theory—they have the same sort of infinity problems as simplicial types, (,1)(\infty,1)-categories, etc. We can, however, define some closely related groups Ext 𝕊 n(A,B)=π nHom(HA,HB)Ext^n_{\mathbb{S}}(A,B) = \pi_{-n} Hom(H A, H B) by taking the ordinary mapping spectrum (ignoring the HH\mathbb{Z}-module structures that we don’t know how to define). These groups are called “ExtExt over the sphere spectrum”.

There are equivalent definitions by classification. Namely, Ext 𝕊 n(A,B)Ext^n_{\mathbb{S}}(A,B) classifies fiber sequences of spectra Σ n1(HB)EHA \Sigma^{n-1} (H B) \to E \to H A while Ext H n(A,B)Ext^n_{H\mathbb{Z}}(A,B) (the usual ExtExt) classifies analogous fiber sequences of HH\mathbb{Z}-modules. When n=1n=1, this ought to reproduce the usual definition of Ext 1(A,B)Ext^1(A,B) in terms of extensions of abelian groups, but probably recovering the version of Ext n(A,B)Ext^n(A,B) for n>1n\gt 1 in terms of “iterated extensions” requires identifying HH\mathbb{Z}-modules with chain complexes.

Posted by: Mike Shulman on July 30, 2013 6:48 PM | Permalink | Reply to this

Re: Cohomology Detects Failures of Classical Mathematics

This is a very naive question, but I vaguely remember that, in the infinite dimensional context, Drinfeld has suggested that the usual definition of projective is “wrong”, and that is the source of a lot of the set-theoretic oddities. Instead, one should use flat and Mittag-Leffler. Would changing the definition in this way have any impact on the result here (presumably defining exts in terms of resolutions of this new definition of projective)?

Posted by: Aaron Bergman on July 31, 2013 1:39 AM | Permalink | Reply to this

Re: Cohomology Detects Failures of Classical Mathematics

I’m not sure exactly what you mean by “infinite-dimensional”, but my instinct is no. When you say “the result here” what exactly are you referring to? Blass’s theorem that cohomology detects failures of LEM and AC, or the discussion in the other comments of Ext?

One of the problems with defining (co)homological concepts in terms of resolutions constructively is that such resolutions may not exist. For instance, every abelian group still has a resolution by free ones, but free abelian groups are no longer necessarily projective, so this resolution doesn’t have the properties you want to get a good definition of cohomology. Can you show constructively that everything has a resolution by flat and Mittag-Leffler things? Do they have the behavior you want for cohomology? (In particular, does such a definition give you long exact sequences?)

Posted by: Mike Shulman on July 31, 2013 4:00 AM | Permalink | Reply to this

Re: Cohomology Detects Failures of Classical Mathematics

I’ll admit that I haven’t had a chance to read the post in detail, and this stuff is fairly far out of my (former) areas of expertise – hence the disclaimer – but I was thinking back to this old mathoverflow answer which refers to homological dimension depending on the continuum hypothesis. This is a far cry from a dependence on the continuum hypothesis, but it did make me a bit curious.

Posted by: Aaron on July 31, 2013 4:41 AM | Permalink | Reply to this

Re: Cohomology Detects Failures of Classical Mathematics

Interesting! I wonder whether free modules are constructively flat and Mittag-Leffler and whether they give a useful theory of resolutions. I don’t have time to work it out myself, though.

Posted by: Mike Shulman on July 31, 2013 5:52 PM | Permalink | Reply to this

Post a New Comment