| Title:
|
Ext groups in Homotopy Type Theory (English) |
| Author:
|
Christensen, J. Daniel |
| Author:
|
Flaten, Jarl G. Taxerås |
| Language:
|
English |
| Journal:
|
Higher Structures |
| ISSN:
|
2209-0606 |
| Volume:
|
9 |
| Issue:
|
2 |
| Year:
|
2025 |
| Pages:
|
17-61 |
| Summary lang:
|
English |
| . |
| Category:
|
math |
| . |
| Summary:
|
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 [43] 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 large, we show that the 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 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 [14]. (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 $\Bbb{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. (English) |
| Keyword:
|
Ext |
| Keyword:
|
Yoneda Ext |
| Keyword:
|
homological algebra |
| Keyword:
|
homotopy type theory |
| MSC:
|
03B38 |
| MSC:
|
18D40 |
| MSC:
|
18G15 |
| MSC:
|
18N60 |
| idMR:
|
MR4994249 |
| DOI:
|
10.21136/HS.2025.09 |
| . |
| Date available:
|
2026-03-13T14:49:03Z |
| Last updated:
|
2026-03-13 |
| Stable URL:
|
http://hdl.handle.net/10338.dmlcz/153491 |
| . |
| Reference:
|
[1] Baer, Reinhold: Erweiterung von Gruppen und ihren Isomorphismen.Math. Z., Vol. 38, 375-416 10.1007/BF01170643 |
| Reference:
|
[2] Bauer, Andrej, Gross, Jason, Lumsdaine, Peter LeFanu, Shulman, Michael, Sozeau, Matthieu, Spitters, Bas: The HoTT library: A formalization of homotopy type theory in coq.J. Funct. Program., Vol. 27, Iss. 1, https://github.com/HoTT/Coq-HoTT, DOI:10.1017/S095679681700001X 10.1017/S095679681700001X |
| Reference:
|
[3] Blechschmidt, Ingo: Flabby and injective objects in toposes.https://arxiv.org/abs/1810.12708v1 |
| Reference:
|
[4] Blechschmidt, Ingo: Using the internal language of toposes in algebraic geometry.https://rawgit.com/iblech/internal-methods/master/notes.pdf |
| Reference:
|
[5] Buchholtz, Ulrik, Christensen, J. Daniel, Flaten, Jarl G. Taxerås, Rijke, Egbert: Central H-spaces and banded types.Journal of Pure and Applied Algebra, Vol. 229, Iss. 6, 107963, DOI:10.1016/j.jpaa.2025.107963 MR 4897668, 10.1016/j.jpaa.2025.107963 |
| Reference:
|
[6] Buchholtz, Ulrik, Doorn, Floris, Rijke, Egbert: Higher groups in homotopy type theory.Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science |
| Reference:
|
[7] Buchsbaum, David A.: Satellites and universal functors.Annals of Mathematics, Vol. 71, 199 |
| Reference:
|
[8] Christensen, J. Daniel: Non-accessible localizations.Journal of Topology, Vol. 17, Iss. 2, e12336, DOI:10.1112/topo.12336 MR 4821353, 10.1112/topo.12336 |
| Reference:
|
[9] Christensen, J. Daniel, Scoccola, Luis: The Hurewicz theorem in homotopy type theory.Algebraic & Geometric Topology, Vol. 23, Iss. 5, 2107-2140, DOI:10.2140/agt.2023.23.2107 MR 4621425, 10.2140/agt.2023.23.2107 |
| Reference:
|
[10] Boer, M.: A proof and formalization of the initiality conjecture of dependent type theory.Licentiate thesis, |
| Reference:
|
[11] Boer, M., Brunerie, G.: Agda formalization of the initiality conjecture.https://github.com/guillaumebrunerie/initiality |
| Reference:
|
[12] Flaten, Jarl G. Taxerås: Formalising Yoneda Ext in Univalent Foundations.14th international conference on interactive theorem proving (ITP 2023), pp 16:1-16:17, DOI:10.4230/LIPIcs.ITP.2023.16 MR 4627510, 10.4230/LIPIcs.ITP.2023.16 |
| Reference:
|
[13] Flaten, Jarl G. Taxerås: Univalent categories of modules.Mathematical Structures in Computer Science, Vol. 33, Iss. 2, 106-133, DOI:10.1017/S0960129523000178 MR 4613193, 10.1017/S0960129523000178 |
| Reference:
|
[14] Grothendieck, Alexander: Sur quelques points d’algèbre homologique, i.Tohoku Math. J., Vol. 9, 119-221 |
| Reference:
|
[15] Harting, Roswitha: Abelian groups in a topos: Injectives and injective effacements.Journal of Pure and Applied Algebra, Vol. 30, Iss. 3, 247-260 10.1016/0022-4049(83)90060-9 |
| Reference:
|
[16] Harting, Roswitha: Locally injective G-sheaves of abelian groups.Cahiers de topologie et géométrie différentielle, Vol. 22, Iss. 2, 115-122 |
| Reference:
|
[17] Harting, Roswitha: Locally injective abelian groups in a topos.Communications in Algebra, Vol. 11, 349-376 10.1080/00927878308822853 |
| Reference:
|
[18] Hartshorne, Robin: Algebraic geometry.Springer |
| Reference:
|
[19] Kapulkin, C., LeFanu Lumsdaine, P.: The homotopy theory of type theories.Adv. Math., Vol. 338, 1-38, DOI:10.1016/j.aim.2018.08.003 MR 3853043, 10.1016/j.aim.2018.08.003 |
| Reference:
|
[20] Kashiwara, Masaki, Schapira, Pierre: Categories and sheaves.Springer-Verlag Berlin Heidelberg, Volume 332 MR 2182076 |
| Reference:
|
[21] Lamiaux, Thomas, Ljungström, Axel, Mörtberg, Anders: Computing cohomology rings in cubical agda.Proceedings of the 12th ACM SIGPLAN international conference on certified programs and proofs, DOI:10.1145/3573105.3575677 10.1145/3573105.3575677 |
| Reference:
|
[22] LeFanu Lumsdaine, P., Shulman, M.: Semantics of higher inductive types.Math. Proc. Cambridge Philos. Soc., Vol. 169, Iss. 1, 159-208, DOI:10.1017/s030500411900015x MR 4120789, 10.1017/S030500411900015X |
| Reference:
|
[23] Lombardi, Henri, Quitté, Claude: Commutative algebra: Constructive methods: Finite projective modules.Springer Dordrecht MR 3408454 |
| Reference:
|
[24] Lurie, Jacob: Higher topos theory.Princeton University Press MR 2522659 |
| Reference:
|
[25] Mac Lane, Saunders: Homology.Springer |
| Reference:
|
[26] Mitchell, Barry: Theory of categories.Academic Press |
| Reference:
|
[27] Myers, David Jaz: Higher schreier theory.http://davidjaz.com/Talks/DJM_HoTT2020.pdf |
| Reference:
|
[28] Nikolaus, Thomas, Schreiber, Urs, Stevenson, Danny: Principal \infty-bundles: General theory.Journal of Homotopy and Related Structures, Vol. 10, Iss. 4, 749-801, DOI:10.1007/s40062-014-0083-6 MR 3423073, 10.1007/s40062-014-0083-6 |
| Reference:
|
[29] Retakh, Vladimir S.: Homotopic properties of categories of extensions.Russian Mathematical Surveys, Vol. 41, Iss. 6, 217-218, DOI:10.1070/rm1986v041n06abeh004237 10.1070/RM1986v041n06ABEH004237 |
| Reference:
|
[30] Rijke, Egbert: The join construction.https://arxiv.org/abs/1701.07538v1 |
| Reference:
|
[31] Scoccola, Luis: Nilpotent types and fracture squares in homotopy type theory.Mathematical Structures in Computer Science, Vol. 30, Iss. 5, 511-544, DOI:10.1017/S0960129520000146 MR 4122450, 10.1017/S0960129520000146 |
| Reference:
|
[32] Shulman, Michael: All (\infty,1)-toposes have strict univalent universes.https://arxiv.org/abs/1904.07004 |
| Reference:
|
[33] Shulman, Mike: Fibrations with fiber an eilenberg-MacLane space.https://homotopytypetheory.org/2014/06/30/fibrations-with-em-fiber/ |
| Reference:
|
[34] Shulman, Mike: Spectral sequences.https://homotopytypetheory.org/2013/08/08/spectral-sequences/ |
| Reference:
|
[35] Simpson, Alex: Pullback-stability of internally projective objects.https://mathoverflow.net/q/140262, Version dated 2013-08-23, MathOverflow |
| Reference:
|
[36] Stacks project authors, The: The stacks project.https://stacks.math.columbia.edu |
| Reference:
|
[37] Stenzel, Raffael: On notions of compactness, object classifiers, and weak tarski universes.Mathematical Structures in Computer Science, Vol. 33, Iss. 8, 661-678, DOI:10.1017/S0960129523000051 MR 4651602, 10.1017/S0960129523000051 |
| Reference:
|
[38] Univalent Foundations Program, The: Homotopy type theory: Univalent foundations of mathematics.https://homotopytypetheory.org/book MR 3204653 |
| Reference:
|
[39] Wärn, David: On internally projective sheaves of groups.https://arxiv.org/abs/2409.12835 |
| Reference:
|
[40] Weibel, Charles A.: An introduction to homological algebra.Cambridge studies in advanced mathematics, Cambridge University Press, DOI:10.1017/CBO9781139644136 10.1017/CBO9781139644136 |
| Reference:
|
[41] Wofsey, Eric: Ext$^{n}$ as the class of yoneda extensions of degree n.https://math.stackexchange.com/q/1766337, Mathematics Stack Exchange |
| Reference:
|
[42] Yoneda, Nobuo: On Ext and exact sequences.J. Fac. Sci. Univ. Tokyo Sect. I, Vol. 8, 507-576 |
| Reference:
|
[43] Yoneda, Nobuo: On the homology theory of modules.J. Fac. Sci. Univ. Tokyo. Sect. I., Vol. 7, 193-227 |
| . |
