Internal Yoneda Ext Groups, Central H-spaces, and Banded Types
Abstract
We develop topics in synthetic homotopy theory using the language of homotopy type theory, and study their semantic counterparts in an ∞-topos. Specifically, we study Grothendieck categories and Yoneda Ext groups in this setting, as well as a novel class of central H-spaces along with their associated bands. The former are fundamental notions from homological algebra that support important computations in traditional homotopy theory. We develop these tools with the goal of supporting similar computations in our setting. In contrast, our results about central H-spaces and bands are new, even when interpreted into the ∞-topos of spaces.
In Chapter 2 we define and study Grothendieck categories in HoTT, which are abelian categories that satisfy additional axioms. The main subtlety in this development is the construction of left-exact coproducts (the AB4 axiom) from exactness of filtered colimits (AB5) in a cocomplete abelian category. In particular, it follows that coproducts of modules over a ring are left-exact, and this is one of our main results. Traditionally, it is easy to deduce AB4 from AB5 using that the finite subsets of a set X form a filtered category. However, the concept of "finite" bifurcates into multiple nonequivalent concepts in our constructive setting. Instead we consider lists of elements of X, inspired by Roswitha Harting's construction of internal coproducts of abelian groups in an elementary topos [Har82].
These results lay the foundation for our study of Yoneda Ext groups [Yon60, Mac63]. Chapter 3 describes our formalization of higher Ext groups of abelian groups, and their expected (contravariant) long exact sequence. We give a novel proof of the usual six-term exact sequence from a fibre sequence of spaces of short exact sequences (Theorem 3.4.1). We also emphasize that our formalization can be adapted to modules over a ring, and that these higher Ext groups are interesting even for abelian groups. In Chapter 4 we further develop the theory of our Ext groups and relate their semantic counterparts to sheaf Ext [Gro57] in certain ∞-topos models. We also carry out a detailed study of internal injectivity and projectivity of modules an ∞-topos, and show that our Ext groups can be computed using resolutions of such in certain cases.
The final Chapter 5 is mostly independent. In it, we study generalizations of Eilenberg–Mac Lane spaces called central H-spaces. Such H-spaces admit an astonishingly simple notion of torsor (independently studied in [Wär23]), namely that of a banded type. The type of such torsors form a delooping of a central H-space, analogously to how the type of torsors of a group G form a K(G,1). Using centrality, we define a tensor product on banded types, producing an H-space structure which makes the type of torsors into a central H-space itself. Iterating this procedure, we obtain arbitrary deloopings of A (and also of pointed self-maps of A) which are in fact unique.