Cellular cohomology in homotopy type theory

Ulrik Buchholtz; Kuen Bang Hou

doi:10.23638/LMCS-16(2:7)2020

Cellular cohomology in homotopy type theory

Ulrik Buchholtz, Kuen Bang Hou

Computer Science and Engineering

Research output: Contribution to journal › Article › peer-review

4 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)
Article number	7
Pages (from-to)	1-21
Number of pages	21
Journal	Logical Methods in Computer Science
Volume	16
Issue number	2
DOIs	https://doi.org/10.23638/LMCS-16(2:7)2020
State	Published - 2020

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 the 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:
© Ulrik Buchholtz and Kuen-Bang Hou (Favonia).

Copyright:
Copyright 2020 Elsevier B.V., All rights reserved.

Keywords

Cellular cohomology
Homotopy type theory
Mechanized reasoning

Publisher link

10.23638/LMCS-16(2:7)2020

Find It

Find It at U of M Libraries

Cite this

@article{2a6f67a89d714ad0add98b371174b2ba,

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 Hou, {Kuen Bang}",

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 the 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} Ulrik Buchholtz and Kuen-Bang Hou (Favonia). Copyright: Copyright 2020 Elsevier B.V., All rights reserved.",

year = "2020",

doi = "10.23638/LMCS-16(2:7)2020",

language = "English (US)",

volume = "16",

pages = "1--21",

journal = "Logical Methods in Computer Science",

issn = "1860-5974",

publisher = "Technischen Universitat Braunschweig",

number = "2",

}

TY - JOUR

T1 - Cellular cohomology in homotopy type theory

AU - Buchholtz, Ulrik

AU - Hou, Kuen Bang

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 the 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: © Ulrik Buchholtz and Kuen-Bang Hou (Favonia). Copyright: Copyright 2020 Elsevier B.V., All rights reserved.

PY - 2020

Y1 - 2020

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=85086890320&partnerID=8YFLogxK

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

U2 - 10.23638/LMCS-16(2:7)2020

DO - 10.23638/LMCS-16(2:7)2020

M3 - Article

AN - SCOPUS:85086890320

SN - 1860-5974

VL - 16

SP - 1

EP - 21

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

IS - 2

M1 - 7

ER -

Cellular cohomology in homotopy type theory

Abstract

Bibliographical note

Keywords

Publisher link

Find It

Other files and links

Fingerprint

Cite this