Andrew Swan: The cohomology of the natural numbers in cubical assemblies

Abstract: Cohomology groups have a natural definition for types internal to homotopy type theory (HoTT), and so can also be defined for objects of any model of HoTT. Since the cohomology groups are trivial for projective objects, one way of thinking about cohomology is as a “measure” of how the axiom of choice fails. In particular the cohomology group of the natural numbers being non trivial witnesses the failure of countable choice.

In the first half of the talk I will introduce cohomology in HoTT and in the cubical assemblies model of HoTT. In particular following the internal HoTT definition of cohomology does not directly give a group, but instead a group object inside the model. I'll show that for a suitable choice of “externalisation” we get a non trivial group external to the model.

In the second half I'll show some basic properties of the resulting group: it is countable, torsion free and abelian, and using some “computability style” arguments we can further show it has infinite rank, contains infinitely many copies of the rational numbers, contains infinitely many pure elements, i.e. $g$ such that no $n > 1$ divides $g$, and that it cannot be written as a direct sum $A \oplus B$ where $A$ is c.e. and contains a pure element (so in particular cannot be written as $\mathbb{Z} \oplus B$ for any $B$).