For people interested in doing homotopy theory in homotopy type theory, Chapter 8 of the HoTT Book is a pretty good record of a lot of what was accomplished during the IAS year. However, there are a few things it’s missing, so I thought it would be a good idea to record some of those for the benefit of those wanting to push the theory further. (Hopefully at some point, papers will be written about all of these things…)
Today I want to talk about cohomology. Chapter 8 of the book focuses mostly on calculating homotopy groups, which are an important aspect of homotopy theory, but most working algebraic topologists spend more time on homology and cohomology, which (classically) are more easily computable. It’s an open question whether they will be similarly easier in homotopy type theory, but we should still be interested in defining and studying them.
Most of what I’m going to say in this post is not original or new, and should be attributed to lots of people (e.g. many of the people mentioned in the Notes to Chapter 8). At the end I’ll remark on a recent surprise that came up on the mailing list.
I’m going to use the notation of the book, such as for the n-truncation, with simply for the propositional truncation in the case . I’ll also adopt the book’s convention that the adjective merely indicates application of the propositional truncation.
The definition of cohomology
Classically, there are many definitions of cohomology, but the one that seems most correct and tractable in homotopy type theory is the representable one. In its most general form, for any types X and Y, we define the (nonabelian) cohomology of X with coefficients in Y to be the 0-truncation of the mapping space from X to Y:
It is, of course a set. This should seem like a fairly natural thing to study, since maps between types are important, and big types with lots of homotopy are complicated, so we might hope that their 0-truncations are simpler.
More precisely, the above definition is the 0th cohomology, . The nth cohomology for is defined by adding loop spaces:
Note that if , then is always a group (it inherits the loop composition operation from ), while if then it is an abelian group by the Eckmann-Hilton argument. For positive n, the nth cohomology is only defined if Y is a loop space, so that we can “un-loop” it. Namely, if for some , then we can define
This notation is a bit misleading, though, because this set depends not only on the type Y but on the choice of its “delooping” . In general, a type may admit lots of different deloopings (and some types have none at all). Classically, algebraic topologists are most interested in cohomology with coefficients in types that have all deloopings in a specified way. Such a type is called a spectrum.
More precisely, a spectrum is a family of types such that for all n we have (a specified equivalence) . For such a Y, we define the (abelian) cohomology of X with coefficients in Y to be
where k is sufficiently large so that . (The assumptions mean that the definition is independent of k as long as it is sufficiently large.) Note that these are all abelian groups, which is part of what makes them easier to calculate with.
Where do spectra come from? The “standard” spectra are built out of Eilenberg-Mac Lane spaces, which are mentioned briefly in the book but not expanded on. For an abelian (set) group G and , an Eilenberg-Mac Lane space of type is a pointed, -connected, -type Y such that (and all other homotopy groups are trivial, by the assumptions). For instance, the higher inductive circle is an Eilenberg-Mac Lane space of type .
One result that was proven last spring (by Dan Licata) is that Eilenberg-Mac Lane spaces exist for all G and n. It’s easy to see that they are unique, and that . Thus, for fixed G, we have an Eilenberg-Mac Lane spectrum , defined by . Cohomology with coefficients in HG is called ordinary cohomology with coefficients in G,
The Eilenberg-Steenrod axioms
Now as I mentioned, in classical algebraic topology, cohomology has lots of equivalent definitions. Some of them, like cellular and simplicial cohomology, seem difficult or impossible to mimic in homotopy type theory. But another very useful classical characterization of cohomology is via what are called the Eilenberg-Steenrod axioms. One writes down a list of properties satisfied by the family of functors , and then it is a theorem that any family of functors satisfying these axioms is equal to for some abelian group G. In many cases, cohomology groups can be calculated using only the axioms, without needing to invoke any particular definition. So it’s natural to want to show at least that our definition in homotopy type theory satisfies the axioms.
Actually, the axioms don’t quite apply to the cohomology functors we’ve defined above, but rather to the reduced cohomology functors , defined whenever X is a pointed space (i.e. equipped with an element ) by replacing the type of maps by the type of pointed maps (those which send the basepoint to the basepoint). If X is unpointed, then is pointed and we have , so these groups are actually more general. (An equivalent list of axioms can also be formulated for relative cohomology, in which the input is a map of unpointed types.)
Here are the axioms, which apply to a collection of contravariant functors from pointed types to abelian groups.
1. Exactness: For any map with cofiber , the sequence is exact.
2. Suspension: We have natural isomorphisms , where is the suspension of X.
3. Additivity: For a set-indexed family of pointed spaces , with their wedge (joint pushout over the basepoints), the induced map is an isomorphism.
A collection of such functors is called a cohomology theory, and it is said to be ordinary if for (note that the reduced cohomology of is the unreduced cohomology of a point). Ordinary cohomology theories correspond to the Eilenberg-Mac Lane spectra H G, where G is the 0th unreduced cohomology of a point. In this case, the above axioms are enough to compute the cohomology of any CW complex, and this is how the uniqueness theorem can be proven in classical algebraic topology. Namely, a CW complex X can be stratified into subspaces , where is obtained from by attaching n-discs. Then the cofiber of the inclusion is a wedge of n-spheres, so that its cohomology is determined by the suspension and additivity axioms; hence by induction we can calculate the cohomology of each . Unraveling all this yields the usual definition of cellular cohomology.
Now recall that in homotopy type theory, for any spectrum Y, our definition of reduced cohomology is
where denotes the type of pointed maps. Unlike in classical homotopy theory, not every type is equivalent to a CW complex, so we shouldn’t expect a uniqueness theorem, but if we could show the axioms, then we could hope to at least calculate cohomology of all types that are CW complexes. So let’s try to prove the axioms.
For exactness, the universal property of the cofiber says essentially that for any Z, we have a fiber sequence
Passing to 0-truncation from this yields the desired exact sequence. For the suspension axiom, the adjointness between suspension and loop spaces yields
so that passing to 0-truncation yields the desired isomorphism. Finally, since wedges are coproducts of pointed types, given we have
for any Z. Now we can pass to 0-truncation and conclude the additivity axiom… if commutes with 0-truncation! This is true if the indexing set I is finite, but in general, it is a sort of axiom of choice, and can fail even if I is an otherwise well-behaved type like the natural numbers.
The finite additivity axiom, along with the other axioms, is enough to show (by the above sort of arguments) that the ordinary cohomology of any finite CW complex (such as a sphere or a torus) agrees with its value in classical algebraic topology. This is nice; but what about the infinite case?
The cohomology of sets
In fact, it seems that there are models where infinite additivity fails, and where the cohomology of infinite complexes can look very different from its classical value. On the mailing list a few days ago, I sketched an argument that the cohomology
can be nontrivial. Here denotes the usual (infinite) set of natural numbers, which is in particular a set, having no higher homotopy above dimension 0. It even has decidable equality. Nevertheless, the claim is that in some models, it can have nontrivial higher cohomology!
This may seem extremely bizarre at first, but it seems less strange if you know something about the models in question. On the one hand, we already knew that in some toposes there are sets with nontrivial cohomology. For instance, there are "cohesive" toposes which contain all classical smooth manifolds as objects, and in which their internally defined cohomology agrees with their usual cohomology (and hence is nontrivial). Note that although such manifolds are of course not “discrete sets” in the usual sense, they are still “sets” in the sense of the model, i.e. 0-truncated objects. (There is another, unrelated, internal notion of “discreteness” in such models.) However, these models don’t explain how a set like , which is discrete in all possible senses, could have nontrivial cohomology.
On the other hand, there are toposes of sheaves on topological spaces, in which we might naturally expect the (external) cohomology of the space on which we are considering sheaves to be visible in some way. The relationship isn’t completely straightforward, though, because as I mentioned above, internally, weird things can only happen in the cohomology of infinite spaces (like ).
To see how this can happen, note first that since , calculating is about looking for maps , i.e. sequences of points on the circle. The basic idea of the argument is that there can be nonstandard points on the circle, i.e. points which are not provably equal to the basepoint. (Of course, like all points on the circle, they are merely equal to the basepoint, i.e. is inhabited, though may not be.)
To produce a nonstandard point of the circle, suppose we have mere propositions P, Q, R, S such that (the “mere disjunction” of P and Q) holds, and such that . Now it is a fact that the mere disjunction is equivalent to the join , i.e. the pushout of P and Q under . This can be proven by a fairly tedious calculation; Nicolai Kraus and Christian Sattler have recently given a slicker argument that also doesn’t require having in hand to begin with.
Thus, since holds by assumption, we may define a point of by induction on , which is to say we have to give functions and and a proof that they agree on . We take both functions to be constant at the basepoint (what else could we do?). But on , which is equal to , we divide into cases: if R, we take the proof of equality to be reflexivity, while if S we take it to be some nontrivial loop (such as the generating loop of the circle).
This yields a point of the circle, but it is not obvious how to prove that this point is equal to the basepoint. And indeed, in some models it is not equal to it. For instance, in the topos of sheaves on the topological circle, with P and Q the complements of two antipodal points, these “nonstandard” points form the external degree-1 cohomology of the topological circle with coefficients in , which is certainly nontrivial. A less topological example is the topos of presheaves on the poset with and and and , where P and Q are the representables at c and d. (Note that the geometric realization of this poset is the topological circle.)
However, the internal cohomology is still trivial: these nonstandard points are all still merely equal to the basepoint, hence become equal upon 0-truncation. But we can obtain nontrivial internal cohomology by invoking the failure of the axiom of choice. Roughly, if we define such that each is a nonstandard point defined using a different collection of P, Q, R, S, then we have , but that won’t necessarily imply , so that f may represent a nontrivial element of . The best concrete example I’ve thought of so far is the topos of sheaves on the topological Hawaiian earring, where we have countably many circles that we can use to define countably many nonstandard points, but only finitely many of these points can be trivialized over any open cover.
So what are we to make of a theory where can be nontrivial? On the one hand, we might find it a bit depressing for the prospect of doing homotopy theory in homotopy type theory: we can’t even determine the ordinary cohomology of such a simple space as the natural numbers. On the other hand, it’s also kind of exciting. We have an entirely new thing to study, which is apparently only visible in constructive homotopy type theory: the cohomology of sets!
What does the cohomology of a set mean? This example suggests that as long as the “ambient logic” has sufficiently nontrivial cohomology (i.e. there are enough nonstandard points of the circle, or more generally nonstandard points of Eilenberg-Mac Lane spaces), then the cohomology of a set X “measures” the failure of the axiom of choice for certain X-indexed families. This shouldn’t be surprising, since geometrically, cohomology can be said to measure the existence of “nontrivial coverings” of a space. But it suggests that we could use cohomological methods in logic. For instance, the exactness and finite additivity axioms are still true for the cohomology of sets, hence give us ways to calculate that cohomology when a complicated set is constructed out of simpler ones. The same would apply to other calculational tools, like spectral sequences, once we establish them in homotopy type theory.