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.

Joel Riou attended the conference virtually; his talk was about formalising homological algebra and the theory of derived categories in Lean. One thing the Lean community learnt about five years ago, and which I believe was very well-known by other formalisation communities many years before that, was the key role played by universal properties in mathematics. It is an unwise idea to prove theorems about, for example, "the" field of fractions of a commutative ring. Why? Because you might find that the rational numbers are not equal to "the" field of fractions of the integers, but rather just canonically isomorphic to it: Lean is of course fussy about this sort of thing. Instead you should prove all your theorems about all rings which satisfy the universal property of fields of fractions; that way your theorems are guaranteed to apply to the rationals, whether they are defined to be equal to the field of fractions of the integers under the hood or not. With that in mind, what is the universal property of the cohomology groups of a complex? There are many answers to this question; Joel has isolated an answer which is both usable, and stable under applying the opposite functor, and showed how he can use this to develop a working theory of derived categories and other examples; in particular he has a new definition of Ext groups which is easier to work with.

Oliver Nash spoke on topological K-theory. His delightful talk proposed several definitions of K-groups and higher K-groups, each of which are nearly but not quite ready to be formalised; work went on during the week to fill in the various holes which he had highlighted, and I am confident that soon we will be able to get K-theory into mathlib. As mentioned above, it's not good enough to just give a definition which is strictly speaking mathematically correct; one also needs to show that the definition is actually usable within the system. Reid Barton suggested that a good test theorem for this would be Bott periodicity; Oliver has already begun to think about this.

Emily Witt gave a talk on local cohomology, a theory which was not formalised in Lean when she gave the talk, but was formalised in Lean later that day by Emily herself and Scott Morrison. The work was merged into mathlib by the end of the week. Emily, Jake Levinson, and Sam van Gool spent some of the week developing a basic API for local cohomology. Sam himself spoke about adjunctions in the theory of topological spaces, and he has since also made a PR formalising some of the work presented in the talk.

María Inés de Frutos Fernández talked about her work on formalising Fontaine theory, some of it with Antoine Chambert-Loir. A consequence of her work is that we will soon be able to state comparison isomorphisms between different cohomology theories which show up in arithmetic. One obstruction to doing this now is the unfortunate fact that we still have no definition of étale cohomology and my impression was that little progress was made here, despite many of the ingredients being available. One area where there was some progress was the theory of sheaves of modules, which is still not in mathlib; I am beginning to wonder whether we will end up with three different implementations of the concept, plus isomorphisms between them, with different implementation choices being useful for different applications. Scott Morrison has started by PRing the "hands-on" definition.

On the airporter back to Calgary, Heather and I initiated a "Riemann-Roch Race". People talk about "the Riemann-Roch theorem" but this is a misnomer -- there are two Riemann-Roch theorems, one a theorem about algebraic line bundles on complete algebraic curves, the other a theorem about complex line bundles on compact Riemann surfaces. Some people might claim that these are "the same thing", the way mathematicians do, but the bottom line is that these are not the same thing unless you prove some theorems like GAGA which are much harder than the Riemann-Roch theorem. To be honest I am surprised that places like Wikipedia do not stress this fact. Claims like "the Grothendieck-Riemann-Roch theorem is a generalisation of the Riemann-Roch theorem" and "The Atiyah-Singer index theorem is a generalisation of the Riemann-Roch theorem" are slightly misleading to the extent that they are generalisations of different theorems; by this point, neither of these theorems imply the other one: they are theorems belonging to two different branches of mathematics. So, given that there are two Riemann-Roch theorems, which one will be formalised first in Lean? Hopefully the algebraists and analysts will take up the challenge, because it is quite clear that we need both. Note that there are several different ways of stating these theorems, some of which use cohomology. Even showing that various different statements are equivalent to each other will be an interesting exercise.

There were many other talks during the week; videos of them can be found on the BIRS website. On behalf of all the attendees I would like to thank BIRS for hosting us; this was a conference unlike any other I have ever been to. It was broad mathematically and yet still coherent, to the extent that we had analysts, geometers, topologists, algebraists and number theorists interacting in meaningful ways throughout the week.