From 9973a388a68685c44007436bdc7246a6b84fa2b4 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Sat, 3 Jun 2023 14:31:38 +0100 Subject: [PATCH 1/8] add cohomology conference write-up --- posts/banff-cohomology.md | 37 +++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) create mode 100644 posts/banff-cohomology.md diff --git a/posts/banff-cohomology.md b/posts/banff-cohomology.md new file mode 100644 index 00000000..823fea28 --- /dev/null +++ b/posts/banff-cohomology.md @@ -0,0 +1,37 @@ +--- +author: 'Kevin Buzzard' +category: 'overview' +date: 2023-06-03 07:42:45+00:00 +description: '' +has_math: false +link: '' +slug: banff-cohomology +tags: '' +title: Formalising cohomology theories +type: text +--- + +Kevin Buzzard rounds up the BIRS conference on formalising cohomology theories. + + +# Formalising cohomology theories + +Last week a group of formalisation enthusiasts, many of them Lean experts, met together at a [BIRS workshop](http://www.birs.ca/events/2023/5-day-workshops/23w5124) 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, which had been defined by Brendon Seamus Murphy, and group cohomology, which had been defined by Amelia Livingston. Amelia's work is already in Lean's mathematics library `mathlib`, and Brendon's is on the way. But just writing down the definition of a cohomology theory is *not good enough*. One needs to prove theorems using the cohomology theory, to demonstrate that the definition is actually usable in practice (for example, one could imagine developing some huge 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, Brendon outlined his 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 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. + +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 etale 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 choices of definition being useful for different applications. + +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. + +There were many other talks during the week; videos of them can be found on the [BIRS website](http://www.birs.ca/events/2023/5-day-workshops/23w5124/videos) . 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. \ No newline at end of file From 8ede6bd3c111c8bbb4c3229e6fa2dbfc02d87d09 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Sun, 4 Jun 2023 19:21:51 +0100 Subject: [PATCH 2/8] Update posts/banff-cohomology.md Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com> --- posts/banff-cohomology.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/posts/banff-cohomology.md b/posts/banff-cohomology.md index 823fea28..ef34033d 100644 --- a/posts/banff-cohomology.md +++ b/posts/banff-cohomology.md @@ -22,7 +22,7 @@ There are many cohomology theories in the mathematical literature, and some have Successes which had already been achieved before the conference were singular homology, which had been defined by Brendon Seamus Murphy, and group cohomology, which had been defined by Amelia Livingston. Amelia's work is already in Lean's mathematics library `mathlib`, and Brendon's is on the way. But just writing down the definition of a cohomology theory is *not good enough*. One needs to prove theorems using the cohomology theory, to demonstrate that the definition is actually usable in practice (for example, one could imagine developing some huge 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, Brendon outlined his 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 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. +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. From 406371bee25c0b17cf238fc35300aa8115677830 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Sun, 4 Jun 2023 19:34:34 +0100 Subject: [PATCH 3/8] fix Brendan name and attribution; other minor fixes --- posts/banff-cohomology.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/posts/banff-cohomology.md b/posts/banff-cohomology.md index ef34033d..2ef79688 100644 --- a/posts/banff-cohomology.md +++ b/posts/banff-cohomology.md @@ -20,7 +20,7 @@ Last week a group of formalisation enthusiasts, many of them Lean experts, met t 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, which had been defined by Brendon Seamus Murphy, and group cohomology, which had been defined by Amelia Livingston. Amelia's work is already in Lean's mathematics library `mathlib`, and Brendon's is on the way. But just writing down the definition of a cohomology theory is *not good enough*. One needs to prove theorems using the cohomology theory, to demonstrate that the definition is actually usable in practice (for example, one could imagine developing some huge 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, Brendon outlined his 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. +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. @@ -32,6 +32,6 @@ Emily Witt gave a talk on local cohomology, a theory which was not formalised in 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 etale 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 choices of definition being useful for different applications. -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. +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](http://www.birs.ca/events/2023/5-day-workshops/23w5124/videos) . 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. \ No newline at end of file From 9041a13f4b2b70e06e3474edfc5104850e98c1da Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Sun, 11 Jun 2023 12:10:20 +0100 Subject: [PATCH 4/8] fix space Co-authored-by: Scott Morrison --- posts/banff-cohomology.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/posts/banff-cohomology.md b/posts/banff-cohomology.md index 2ef79688..e673e0b9 100644 --- a/posts/banff-cohomology.md +++ b/posts/banff-cohomology.md @@ -34,4 +34,4 @@ María Inés de Frutos Fernández talked about her work on formalising Fontaine 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](http://www.birs.ca/events/2023/5-day-workshops/23w5124/videos) . 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. \ No newline at end of file +There were many other talks during the week; videos of them can be found on the [BIRS website](http://www.birs.ca/events/2023/5-day-workshops/23w5124/videos). 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. \ No newline at end of file From 4ebf73ff2db715f8897321e301fb51a03f59e191 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Sun, 11 Jun 2023 12:14:18 +0100 Subject: [PATCH 5/8] Riemann-Roch Co-authored-by: Scott Morrison --- posts/banff-cohomology.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/posts/banff-cohomology.md b/posts/banff-cohomology.md index e673e0b9..39c40229 100644 --- a/posts/banff-cohomology.md +++ b/posts/banff-cohomology.md @@ -32,6 +32,6 @@ Emily Witt gave a talk on local cohomology, a theory which was not formalised in 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 etale 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 choices of definition being useful for different applications. -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. +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](http://www.birs.ca/events/2023/5-day-workshops/23w5124/videos). 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. \ No newline at end of file From 9a8042607c947467d4c98176f0220db284ec8543 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Sun, 11 Jun 2023 12:15:22 +0100 Subject: [PATCH 6/8] accent on etale Co-authored-by: Scott Morrison --- posts/banff-cohomology.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/posts/banff-cohomology.md b/posts/banff-cohomology.md index 39c40229..bf4d711b 100644 --- a/posts/banff-cohomology.md +++ b/posts/banff-cohomology.md @@ -30,7 +30,7 @@ Oliver Nash spoke on topological K-theory. His delightful talk proposed several 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. -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 etale 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 choices of definition being useful for different applications. +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 choices of definition being useful for different applications. 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. From c7423acdc480fc8ec7ed4a3aeedaebf639b869ea Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Sun, 11 Jun 2023 12:23:32 +0100 Subject: [PATCH 7/8] add links to various Banff-inspired PRs --- posts/banff-cohomology.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/posts/banff-cohomology.md b/posts/banff-cohomology.md index bf4d711b..a40ff400 100644 --- a/posts/banff-cohomology.md +++ b/posts/banff-cohomology.md @@ -28,9 +28,9 @@ Joel Riou attended the conference virtually; his talk was about formalising homo 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. +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](https://github.com/leanprover-community/mathlib/pull/19061) by the end of the week. Emily, Jake Levinson, and Sam van Gool spent some of the week [developing a basic API](https://github.com/leanprover-community/mathlib/pull/19105) 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](https://github.com/leanprover-community/mathlib4/pull/4593). -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 choices of definition being useful for different applications. +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](https://github.com/leanprover-community/mathlib4/pull/4670). 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. From 8e55acb93b2653cb7ad95aca3d3bb1d3c25aa678 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Mon, 12 Jun 2023 17:58:11 +0100 Subject: [PATCH 8/8] fix last week; update date --- posts/banff-cohomology.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/posts/banff-cohomology.md b/posts/banff-cohomology.md index a40ff400..a60bceb9 100644 --- a/posts/banff-cohomology.md +++ b/posts/banff-cohomology.md @@ -1,7 +1,7 @@ --- author: 'Kevin Buzzard' category: 'overview' -date: 2023-06-03 07:42:45+00:00 +date: 2023-06-12 07:42:45+00:00 description: '' has_math: false link: '' @@ -16,7 +16,7 @@ Kevin Buzzard rounds up the BIRS conference on formalising cohomology theories. # Formalising cohomology theories -Last week a group of formalisation enthusiasts, many of them Lean experts, met together at a [BIRS workshop](http://www.birs.ca/events/2023/5-day-workshops/23w5124) 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. +At the end of May a group of formalisation enthusiasts, many of them Lean experts, met together at a [BIRS workshop](http://www.birs.ca/events/2023/5-day-workshops/23w5124) 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.