Thesis Format
Integrated Article
Degree
Doctor of Philosophy
Program
Mathematics
Supervisor
Christensen, John Daniel
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.
Summary for Lay Audience
In homotopy theory, we study properties of shapes which are preserved by continuous deformations. Some of these shapes are easy to visualize, like circles, spheres, and tori. Others are higher-dimensional (even infinite-dimensional) and therefore impossible to visualize, but they are still important for various reasons. A basic homotopical property is how many connected components a shape has, or how many holes it has---but there are also much more sophisticated properties which give deep insight into the nature of a shape.
There are many kinds of shapes, and many ways of studying them. For instance, instead of taking a point as the basic building block of shapes, one can take another shape as the basic building block. Using the circle as the basic building block, drawing a circle produces a torus (since each "point" is replaced by a circle). In this thesis we study shapes from an internal perspective, which encompasses many ways of studying shapes. This approach can also be represented on a computer, meaning it can check that our proofs are correct.
This internal approach is presently being developed. We contribute to this endeavour by developing certain computational tools, called Ext groups, which are useful for computing properties of shapes. Roughly, Ext groups measure in how many ways two structures can be knitted together to form a new structure. (Such a "knitted structure" is called an extension, which is where the name Ext comes from.) In the context of shapes, they let us compute new properties from old ones. Ext groups play an important role in traditional computations, but have not been previously studied from the internal viewpoint.
We also introduce and study a new form of symmetry we call centrality. A shape is central whenever there is precisely one symmetry (of a certain kind) of the shape which sends its base point any other point. The circle, for example, is central because there is only one way of rotating the base point to any other point without going backwards or doing a full loop. Though a seemingly simple condition, centrality has surprising consequences.
Recommended Citation
Flaten, Jarl Gunnar Taxerås, "Internal Yoneda Ext Groups, Central H-spaces, and Banded Types" (2023). Electronic Thesis and Dissertation Repository. 9343.
https://ir.lib.uwo.ca/etd/9343
Creative Commons License
This work is licensed under a Creative Commons Attribution 4.0 License.