Ulrik Buchholtz ; Kuen-Bang Hou - Cellular Cohomology in Homotopy Type Theory

lmcs:5274 - Logical Methods in Computer Science, June 1, 2020, Volume 16, Issue 2 - https://doi.org/10.23638/LMCS-16(2:7)2020
Cellular Cohomology in Homotopy Type TheoryArticle

Authors: Ulrik Buchholtz ORCID; Kuen-Bang Hou ORCID

    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.


    Volume: Volume 16, Issue 2
    Published on: June 1, 2020
    Accepted on: April 17, 2020
    Submitted on: March 12, 2019
    Keywords: Computer Science - Logic in Computer Science,Mathematics - Algebraic Topology
    Funding:
      Source : OpenAIRE Graph
    • Isaac Newton Institute for Mathematical Sciences; Funder: UK Research and Innovation; Code: EP/K032208/1

    7 Documents citing this article

    Consultation statistics

    This page has been seen 1735 times.
    This article's PDF has been downloaded 382 times.