# Formalising cohomology theories

Kevin Buzzard rounds up the BIRS conference on formalising cohomology theories.

## Formalising cohomology theories

At the end of May a group of formalisation enthusiasts, many of them Lean experts, met together at a BIRS workshop in Banff Canada, and discussed the formalisation of cohomology theories. Cohomology groups are linear invariants associated to typically nonlinear objects, and play an important role in several areas of mathematics. We list a few examples here: One can prove that two nonlinear objects are not isomorphic by showing that they have different cohomology. There are certain mathematical constructions that can be made (such as extending a map from a subgroup to a map from the whole group, or lifting a scheme over a base to a bigger base) if and only if some element of a cohomology group is zero, so if the entire cohomology group vanishes then the construction can always be made. The Hodge conjecture and the Tate conjecture are conjectures predicting that geometric resp. arithmetic behaviour of an appropriate mathematical object can be predicted from behaviour of its cohomology.

There are many cohomology theories in the mathematical literature, and some have already been formalised in other theorem provers. But this is, in my mind, not good enough: we need a system which knows all cohomology theories and which furthermore knows all definitions of all cohomology theories, enabling us to do things such as writing down isomorphisms between cohomology theories, and giving us access to all the homological algebra (exact sequences, spectral sequences, derived functors,...) associated to cohomology theories. My personal aim for the conference was to understand where we are, and where we need to be, with regards to definitions and basic properties of as many cohomology theories as possible.

Successes which had already been achieved before the conference were singular homology, defined by Adam Topaz in 2021, and group cohomology, defined by Amelia Livingston in 2022. Amelia's work is now in Lean's mathematics library `mathlib`, and singular homology is on the way. But just writing down the definition of a homology or cohomology theory is not good enough. One needs to prove theorems using the theory, to demonstrate that the definition is actually usable in practice (for example, one could imagine developing some abstract theory of derived functors, and then defining many cohomology theories as derived functors, and then being completely unable to compute the cohomology of anything at all). In his talk at the conference, Brendan Seamus Murphy outlined his formal proof of the Brouwer fixed point theorem using singular homology, and also his computation of the homology groups of spheres. Similarly, Amelia explained how she had proved the long exact sequence and inflation-restriction sequence for group cohomology. These are good signs: it means that the definitions are usable.

One cohomology theory which we do not have yet is de Rham cohomology. In his talk, Yury Kudriashov outlined what we will need in order to have a working definition -- it is perhaps a few person-weeks away, and progress is definitely being made. Heather Macbeth, Patrick Massot and Floris van Doorn have built a theory of smooth vector bundles on manifolds, for example. During the conference I challenged Heather to prove that their theory was usable, by using it to define Riemannian manifolds, and a few days later Heather showed me the Lean code she'd written which did this. This was enough to convince me that we are on the right track.