Cellular cohomology in homotopy type theory

Ulrik Buchholtz; Kuen Bang Hou Favonia

doi:10.1145/3209108.3209188

Cellular cohomology in homotopy type theory

Ulrik Buchholtz, Kuen Bang Hou Favonia

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

7 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 language	English (US)
Title of host publication	Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	521-529
Number of pages	9
ISBN (Electronic)	9781450355834, 9781450355834
DOIs	https://doi.org/10.1145/3209108.3209188
State	Published - Jul 9 2018
Externally published	Yes
Event	33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018 - Oxford, United Kingdom Duration: Jul 9 2018 → Jul 12 2018

Publication series

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

Conference

Conference	33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018
Country/Territory	United Kingdom
City	Oxford
Period	7/9/18 → 7/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

Access

10.1145/3209108.3209188

OpenUrl availability

Full text

Cite this

Cellular cohomology in homotopy type theory. / Buchholtz, Ulrik; Favonia, Kuen Bang Hou.
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018. Institute of Electrical and Electronics Engineers Inc., 2018. p. 521-529 (Proceedings - Symposium on Logic in Computer Science).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Buchholtz, U & Favonia, KBH 2018, Cellular cohomology in homotopy type theory. in Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018. Proceedings - Symposium on Logic in Computer Science, Institute of Electrical and Electronics Engineers Inc., pp. 521-529, 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, United Kingdom, 7/9/18. https://doi.org/10.1145/3209108.3209188

@inproceedings{9814b1cf670d4f1c8cad21e07c9ae875,

title = "Cellular cohomology in homotopy type theory",

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.",

keywords = "Cellular cohomology, Homotopy type theory, Mechanized reasoning",

author = "Ulrik Buchholtz and Favonia, {Kuen Bang Hou}",

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: {\textcopyright} 2018 ACM.; 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018 ; Conference date: 09-07-2018 Through 12-07-2018",

year = "2018",

month = jul,

day = "9",

doi = "10.1145/3209108.3209188",

language = "English (US)",

series = "Proceedings - Symposium on Logic in Computer Science",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "521--529",

booktitle = "Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018",

}

TY - GEN

T1 - Cellular cohomology in homotopy type theory

AU - Buchholtz, Ulrik

AU - Favonia, Kuen Bang Hou

N1 - 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.

PY - 2018/7/9

Y1 - 2018/7/9

N2 - 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.

AB - 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.

KW - Cellular cohomology

KW - Homotopy type theory

KW - Mechanized reasoning

UR - http://www.scopus.com/inward/record.url?scp=85051127902&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85051127902&partnerID=8YFLogxK

U2 - 10.1145/3209108.3209188

DO - 10.1145/3209108.3209188

M3 - Conference contribution

AN - SCOPUS:85051127902

T3 - Proceedings - Symposium on Logic in Computer Science

SP - 521

EP - 529

BT - Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018

PB - Institute of Electrical and Electronics Engineers Inc.

T2 - 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018

Y2 - 9 July 2018 through 12 July 2018

ER -

Cellular cohomology in homotopy type theory

Abstract

Publication series

Conference

Bibliographical note

Keywords

Access

OpenUrl availability

Other files and links

Fingerprint

Cite this