Schedule for: 23w5124 - Formalization of Cohomology Theories

This is an informal gathering. If you are around, please stop by and say hi! Location: The Juniper Hotel Bistro Patio (in case of bad weather, use the Keguli room).

TBA

Introduced by Grothendieck in the 1960s, local cohomology is an essential tool in commutative algebra, and also capture geometric and topological properties. These modules, associated to an ideal of a Noetherian ring and module over this ring, are typically very large (e.g., not finitely generated), making it difficult to access this data. We touch on some steps needed to formalize local cohomology, while also giving a brief introduction to the open-source computer algebra system Macaulay2.

After providing some motivation I will explore various approaches to the formalisation of topological K-theory using Lean's Mathlib library. In fact we shall see that we can get quite far, though of course some gaps in the library will be encountered. As a result I will assemble a list of attractive formalisation targets, some easy, some not-so-easy.

Group work in several rooms

This talk discusses the results and methodology of a project to formalize the Brouwer Fixed Point theorem in Lean. There was no prior formalization of a (co)homology theory in Lean, so we decided to develop the basic theory of singular homology (i.e. prove the Eilenberg-Steenrod axioms for it). Notably this formalization uses the acyclic models theorem to prove homotopy invariance of singular homology; we discuss this and other design choices. This project depends on mathlib and on (the homological algebra developed for) the Liquid Tensor Experiment.

Diagram chasing is at the heart of many powerful tools in mathematics, for instance spectral sequences. Unfortunately, their usage requires a lot of tedious and technical calculations. For instance, one has to check the commutativity of many diagrams. These technicalities are often not detailed in papers, and can be a source of mistakes. This motivates the development of a formalized library to do diagram chasing on computer. In particular, a large part of the above mentioned computations can be automatized. In this talk, I will present the key points of such a library I am developing with Assia Mahboubi in Coq. In particular, I will explain that all the diagram chasing statements can be restated in a very simple language (in a first order logic), and I will state a formalized version of the often used duality meta-theorem. I hope that this library will be the first step of the development of a powerful library of tools in homological algebra.

I will discuss recent and ongoing work in two relatively long-term number theory formalization projects. The first one, joint with Filippo Nuccio, consists on formalizing the theory of local fields and the main statements and proofs of Local Class Field Theory, following the cohomological approach. The second one consists on formalizing the definition and basic properties of Fontaine’s period rings, in particular B_HT , B_dR and B_crys, as a starting point towards a formalization of p-adic Hodge theory. Part of this formalization is joint work with Antoine Chambert-Loir.

This talk will be about an algebraic way of looking at topological, profinite structures. While it will be mostly a "traditional pen and paper" talk, I hope that, in the context of this workshop, it will provide an impulse to think together about how these things might be formalized, and about how they might fit with previous work done already in Mathlib and the LTE.

There are several reasonable ways to give a “discrete” condensed structure to a set, modelling the behaviour of discrete topological spaces. In this talk I will present a formalisation in Lean of three of those, each useful in its own way, and isomorphisms between them. I will recall the few prerequisites from condensed mathematics before telling the story of the formalisation process. This work builds on definitions and theorems from the Liquid Tensor Experiment, and by extension the Lean mathematical library mathlib.

Since they were introduced in the 1960s by Grothendieck and Verdier, derived categories of abelian categories have played a crucial role in the formulation of cohomological statements and their proofs. In this talk, I shall discuss a formalization of derived categories in Lean/mathlib (initially in Lean 3, but a significant part has already been ported to Lean 4). This project includes a refactor of the definition of the homology of complexes, the verification of the axioms of triangulated categories for the homotopy category of cochain complexes in an additive category, and a localization theorem for triangulated categories. Some of these ingredients were already obtained in the Liquid Tensor Experiment, but the newest part is the localization theorem which allows the definition of the derived category as the localization of the homotopy category of cochain complexes with respect to quasi-isomorphisms. I have also obtained various basic results involving derived categories, e.g. the full embedding of an abelian category in its derived category. (The Lean 4 code is available in my mathlib4 branch \verb+jriou_localization+.)

Only the very basics of homotopy theory have been formalized in proof assistants in the usual way. However, using a special kind of type theory - called homotopy type theory , or HoTT for short - one can do various arguments in homotopy theory in a purely synthetic way. The types of the type theory are themselves considered to be (nice) topological spaces, and the equality type corresponds to paths in this space. HoTT provides very convenient concepts such as path induction, univalence and higher inductive types. Using these techniques many important theorems of homotopy theory have been proved and even formalized in HoTT, such as Blaker's-Massey theorem and the Serre spectral sequence.

In his 2016 PhD thesis, Guillaume Brunerie gave a constructive definition, in Homotopy Type Theory, of a number n satisfying $\pi_4(S^3) = Z/nZ$. This number, nowadays called the 'Brunerie number', quickly rose to infamy in the type theory community: despite being constructively defined, it is not at all obvious that the Brunerie number is actually \pm 2. In fact, with the advent of constructive proof assistants such as Cubical Agda, we should not have to figure this out by ourselves---Agda should be able to compute/normalise n for us. Unfortunately, also this fails: Agda runs out of memory. For this reason, Brunerie had to 'manually' show that n = \pm 2. This talk is loosely based on the recent formalisation of this 'manual' calculation of the Brunerie number. Since the key component in this calculation is cohomology theory, I will give you a brief introduction to the definition of cohomology in HoTT. I will also discuss which related constructions and theorems we have (and have not yet) formalised. On a more practical note, I will show you how new 'Brunerie numbers' appear everywhere in the computation of cohomology rings of spaces and try to convince you that, from this point of view, a fast constructive/fully computational proof assistant could potentially save you hours of work when formalising cohomology computations.

Mathlib now has a definition of group cohomology, and a proof it agrees with some Ext groups. I will talk about the code this involved, which used the existing simplicial objects library. I will also describe the group cohomological results I have formalised but which are not yet in Mathlib. Finally, I will discuss the rest of the group cohomology to-do list, much of which will require porting material from the Liquid Tensor Experiment.

Set theory is widely considered to be the "standard" foundation of mathematics. However, the use of set theory to formalize mathematics is rare today. Some possible reasons include that lack of type checking leads to many nonsensical expressions, and many deductions that could be performed by type inference need to be done by hand. However, it may be possible to address such difficulties using appropriate abstractions and proof automation, after which the advantages of set theory will become more significant. I will discuss my past experiences with such issues, and speculate what could be done to make set theory more viable for formalized mathematics in the future.