Cellular cohomology in homotopy type theory

Ulrik Buchholtz, Kuen Bang Hou Favonia

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Scopus citations

Abstract

We present a development of cellular cohomology in homotopy type theory. Cohomology associates to each space a sequence of abelian groups capturing part of its structure, and has the advantage over homotopy groups in that these abelian groups of many common spaces are easier to compute. Cellular cohomology is a special kind of cohomology designed for cell complexes: these are built in stages by attaching spheres of progressively higher dimension, and cellular cohomology defines the groups out of the combinatorial description of how spheres are attached. Our main result is that for finite cell complexes, a wide class of cohomology theories (including the ones defined through Eilenberg-MacLane spaces) can be calculated via cellular cohomology. This result was formalized in the Agda proof assistant.

Original languageEnglish (US)
Title of host publicationProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages521-529
Number of pages9
ISBN (Electronic)9781450355834, 9781450355834
DOIs
StatePublished - Jul 9 2018
Externally publishedYes
Event33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018 - Oxford, United Kingdom
Duration: Jul 9 2018Jul 12 2018

Publication series

NameProceedings - Symposium on Logic in Computer Science
ISSN (Print)1043-6871

Conference

Conference33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018
Country/TerritoryUnited Kingdom
CityOxford
Period7/9/187/12/18

Bibliographical note

Funding Information:
This research was sponsored by the National Science Foundation under grant number DMS-1638352 and the Air Force Office of Scientific Research under grant number FA9550-15-1-0053. The authors would also like to thank the Isaac Newton Institute for Mathematical Sciences for its support and hospitality during the program “Big Proof” when part of work on this paper was undertaken; the program was supported by Engineering and Physical Sciences Research Council under grant number EP/K032208/1. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of any sponsoring institution, government or any other entity.

Publisher Copyright:
© 2018 ACM.

Keywords

  • Cellular cohomology
  • Homotopy type theory
  • Mechanized reasoning

Fingerprint

Dive into the research topics of 'Cellular cohomology in homotopy type theory'. Together they form a unique fingerprint.

Cite this