eng
episciences.org
Logical Methods in Computer Science
1860-5974
2020-06-01
Volume 16, Issue 2
10.23638/LMCS-16(2:7)2020
5274
journal article
Cellular Cohomology in Homotopy Type Theory
Ulrik Buchholtz
Kuen-Bang Hou
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.
https://lmcs.episciences.org/5274/pdf
Computer Science - Logic in Computer Science
Mathematics - Algebraic Topology