LIPIcs.ITP.2023.16.pdf
- Filesize: 0.79 MB
- 17 pages
Document
Formalising Yoneda Ext in Univalent Foundations
Author
Jarl G. Taxerås Flaten 
-
Part of:
Volume:
14th International Conference on Interactive Theorem Proving (ITP 2023)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2023-07-26
File
Document Identifiers
Author Details
Acknowledgements
The theory of Yoneda Ext in HoTT is joint work with Dan Christensen, to whom I am also grateful for discussions and contributions related to the formalisation. I thank Jacob Ender for contributions to the formalisation of the Baer sum, and the collaborators of the Coq-HoTT library - and Ali Caglayan in particular - for their review of, and contributions to, the various pull requests related to this project. I also thank the anonymous reviewers for valuable feedback.
Cite AsGet BibTex
Jarl G. Taxerås Flaten. Formalising Yoneda Ext in Univalent Foundations. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 16:1-16:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ITP.2023.16
https://doi.org/10.4230/LIPIcs.ITP.2023.16
Abstract
Ext groups are fundamental objects from homological algebra which underlie important computations in homotopy theory. We formalise the theory of Yoneda Ext groups [Yoneda, 1954] in homotopy type theory (HoTT) using the Coq-HoTT library. This is an approach to Ext which does not require projective or injective resolutions, though it produces large abelian groups. Using univalence, we show how these Ext groups can be naturally represented in HoTT. We give a novel proof and formalisation of the usual six-term exact sequence via a fibre sequence of 1-types (or groupoids), along with an application. In addition, we discuss our formalisation of the contravariant long exact sequence of Ext, an important computational tool. Along the way we implement and explain the Baer sum of extensions and how Ext is a bifunctor.
Subject Classification
ACM Subject Classification
- Mathematics of computing → Algebraic topology
- Theory of computation → Logic and verification
- Theory of computation → Type theory
Keywords
- homotopy type theory
- homological algebra
- Yoneda Ext
- formalisation
- Coq
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Ulrik Buchholtz, J. Daniel Christensen, Jarl G. Taxerås Flaten, and Egbert Rijke. Central H-spaces and banded types, 2023. URL: https://doi.org/10.48550/ARXIV.2301.02636.
- J. Daniel Christensen and Jarl G. Taxerås Flaten. Ext groups in homotopy type theory, 2023. URL: https://arxiv.org/abs/2305.09639.
- Coq-HoTT. The Coq-HoTT library. URL: https://github.com/HoTT/Coq-HoTT.
- René Guitart and Luc Van den Bril. Calcul des satellites et présentations des bimodules à l'aide des carrés exacts. Cahiers de Topologie et Géométrie Différentielle Catégoriques, 24(3):299-330, 1983. URL: http://archive.numdam.org/item/CTGDC_1983__24_3_299_0/.
- René Guitart and Luc Van den Bril. Calcul des satellites et présentations des bimodules à l'aide des carrés exacts (2e partie). Cahiers de Topologie et Géométrie Différentielle Catégoriques, 24(4):333-369, 1983. URL: http://archive.numdam.org/item/CTGDC_1983__24_4_333_0/.
-
Saunders Mac Lane. Homology. Springer, 1963.
-
Barry Mitchell. Theory of categories. Academic Press, 1965.
- Vladimir S. Retakh. Homotopic properties of categories of extensions. Russian Mathematical Surveys, 41(6):217-218, December 1986. URL: https://doi.org/10.1070/rm1986v041n06abeh004237.
-
Egbert Rijke. Introduction to Homotopy Type Theory. Cambridge University Press, 2023. To appear.
- The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
- Floris van Doorn. On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory. PhD thesis, Carnegie Mellon University, 2018. URL: https://doi.org/10.48550/arXiv.1808.10690.
-
Nobuo Yoneda. On the homology theory of modules. Journal of the Faculty of Science, the University of Tokyo Section I, 7:193-227, 1954.
-
Nobuo Yoneda. On Ext and exact sequences. Journal of the Faculty of Science, the University of Tokyo Section I, 8:507-576, 1960.