Ext groups in Homotopy Type Theory
J. Daniel Christensen, Jarl G. Taxerås Flaten
TL;DR
This work develops Yoneda Ext groups for modules over a ring within Homotopy Type Theory, defining Ext^1 via short exact sequences and extending to higher Ext with a universal δ-functor structure, all without relying on resolutions. It proves Ext^1 is essentially small and connects to six-term and long exact sequences, while providing resolution-based computation when available. By interpreting these HoTT constructions in ∞-toposes, the authors recover sheaf Ext in sets-cover contexts and relate Ext to internal/external injectivity and to Ext over group rings in slice categories, with concrete analysis in ZG-modules and BG. The results illuminate when HoTT Ext matches classical sheaf Ext, clarify the relationships between various notions of projectivity/injectivity, and supply formalization guidance and concrete examples that anchor the theory in both abstract topos-theoretic and concrete algebraic settings.
Abstract
Ext groups are fundamental homological invariants which have important applications in homotopy theory and algebra. In particular, they appear in the classical universal coefficient theorem, a key computational tool in homotopy theory. Motivated by the goal of extending such tools to synethetic homotopy theory, we develop the theory of Yoneda Ext groups [Yon54] over a ring in homotopy type theory (HoTT) and describe their interpretation into an $\infty$-topos. The Yoneda approach to Ext groups does not require projective or injective resolutions, which is a crucial in HoTT since we do not know that such resolutions exist. While it produces group objects that are a priori, we show that the $\mathrm{Ext}^1$ groups are equivalent to small groups, leaving open the question of whether the higher Ext groups are essentially small as well. We also show that the $\mathrm{Ext}^1$ groups take on the usual form as a product of cyclic groups whenever the input modules are finitely presented and the ring is a PID (in the constructive sense). When interpreted into an $\infty$-topos of sheaves on a 1-category, our Ext groups recover (and give a resolution-free approach to) sheaf Ext groups, which arise in algebraic geometry [Gro57]. (These are also called "local" Ext groups.) We may therefore interpret results about Ext from HoTT and apply them to sheaf Ext. To show this, we prove that injectivity of modules in HoTT interprets to internal injectivity in these models. It follows, for example, that sheaf Ext can be computed using resolutions which are projective or injective in the sense of HoTT, when they exist, and we give an example of this in the projective case. We also discuss the relation between internal $\mathbb{Z} G$-modules (for a $0$-truncated group object $G$) and abelian groups in the slice over $BG$, and study the interpretation of our Ext groups in both settings.