# Schedule for: 23w5124 - Formalization of Cohomology Theories

Beginning on Sunday, May 21 and ending Friday May 26, 2023

All times in Banff, Alberta time, MDT (UTC-6).

Sunday, May 21 | |
---|---|

16:00 - 16:01 | Check-in begins (Juniper Front Desk) |

17:30 - 18:30 | Dinner Seating 1 (Juniper Bistro) |

18:30 - 19:30 | Dinner Seating 2 (Juniper Bistro) |

19:30 - 20:30 | Dinner Seating 3 (Juniper Bistro) |

20:30 - 21:30 |
Informal gathering ↓ 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). (Other (See Description)) |

Monday, May 22 | |
---|---|

07:30 - 08:30 | Breakfast Buffet (Juniper Bistro) |

08:55 - 09:00 | Introduction from BIRS Staff (Kiguli Room) |

09:00 - 10:00 |
Iurii Kudriashov: The path to the formalization of de Rham cohomology ↓ TBA (Kiguli Room) |

10:00 - 10:30 | Coffee Break (Kiguli Room) |

10:30 - 11:30 |
Emily Witt: Local cohomology and Macaulay2 ↓ 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. (Kiguli Room) |

11:30 - 12:00 | Discussion / Coffee Break (Kiguli Room) |

12:00 - 13:30 | Lunch Buffet (Juniper Bistro) |

13:30 - 13:45 | Group Photo (Meet at Bistro Patio (Weather Permitting)) |

14:00 - 15:00 |
Oliver Nash: On the formalisation of topological K-theory ↓ 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. (Kiguli Room) |

15:00 - 15:30 | Coffee Break (Kiguli Room) |

15:30 - 17:30 |
Group work Coordination ↓ Group work in several rooms (Other (See Description)) |

17:30 - 18:30 | Dinner Seating 1 (Juniper Bistro) |

18:30 - 19:30 | Dinner Seating 2 (Juniper Bistro) |

19:30 - 20:30 | Dinner Seating 3 (Juniper Bistro) |

Tuesday, May 23 | |
---|---|

07:30 - 08:30 | Breakfast Buffet (Juniper Bistro) |

09:00 - 10:00 | Scott Morrison (Kiguli Room) |

10:00 - 10:30 | Coffee Break (Kiguli Room) |

10:30 - 11:30 |
Brendan Murphy: Formalizing the Brouwer Fixed Point Theorem in Lean ↓ 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. (Kiguli Room) |

11:30 - 12:00 | Discussion / Coffee Break (Kiguli Room) |

12:00 - 13:30 | Lunch Buffet (Juniper Bistro) |

13:30 - 14:30 |
Matthieu Piquerez: Formalization of diagram chasing as a first-order logic in Coq ↓ 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. (Kiguli Room) |

14:30 - 14:45 | Coffee Break (Kiguli Room) |

14:45 - 15:45 |
María Inés de Frutos Fernández: Cohomology in Number Theory ↓ 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. (Kiguli Room) |

15:45 - 17:45 | Group work / Discussion (Kiguli Room) |

17:30 - 18:30 | Dinner Seating 1 (Juniper Bistro) |

18:30 - 19:30 | Dinner Seating 2 (Juniper Bistro) |

19:30 - 20:30 | Dinner Seating 3 (Juniper Bistro) |

Wednesday, May 24 | |
---|---|

07:30 - 08:30 | Breakfast Buffet (Juniper Bistro) |

09:00 - 09:50 |
Sam van Gool: Frames, profinite structures and sheaves ↓ 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. (Kiguli Room) |

09:50 - 10:05 | Coffee Break (Kiguli Room) |

10:05 - 10:55 |
Dagur Ásgeirsson: Discrete Condensed Sets ↓ 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. (Kiguli Room) |

10:55 - 11:10 | Discussion / Coffee Break (Kiguli Room) |

11:10 - 12:00 |
Joël Riou: Formalization of derived categories in Lean ↓ 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+.) (Kiguli Room) |

12:00 - 13:30 | Lunch Buffet (Juniper Bistro) |

13:30 - 17:30 | Free Afternoon - Shuttle Service to Banff town (Banff National Park) |

17:30 - 18:30 | Dinner Seating 1 (Juniper Bistro) |

18:30 - 19:30 | Dinner Seating 2 (Juniper Bistro) |

19:30 - 20:30 | Dinner Seating 3 (Juniper Bistro) |

Thursday, May 25 | |
---|---|

07:30 - 08:30 | Breakfast Buffet (Juniper Bistro) |

09:00 - 10:00 |
Floris van Doorn: What can we learn from formalizations in homotopy type theory? ↓ 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. (Kiguli Room) |

10:00 - 10:30 | Coffee Break (Kiguli Room) |

10:30 - 11:30 | Reid Barton (Kiguli Room) |

11:30 - 12:00 | Discussion / Coffee Break (Kiguli Room) |

12:00 - 13:30 | Lunch Buffet (Juniper Bistro) |

13:30 - 14:00 | lunch break (Kiguli Room) |

14:00 - 15:00 |
Axel Ljungström: Cohomology Theory and Brunerie Numbers in Cubical Agda ↓ 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. (Kiguli Room) |

15:00 - 15:30 | Coffee Break (Kiguli Room) |

15:30 - 17:30 | Group work / Discussion (Kiguli Room) |

17:30 - 18:30 | Dinner Seating 1 (Juniper Bistro) |

18:30 - 19:30 | Dinner Seating 2 (Juniper Bistro) |

19:30 - 20:30 | Dinner Seating 3 (Juniper Bistro) |

Friday, May 26 | |
---|---|

07:30 - 08:30 | Breakfast Buffet (Juniper Bistro) |

08:30 - 09:30 |
Amelia Livingston: Group cohomology in Lean ↓ 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. (Kiguli Room) |

09:30 - 10:30 |
Bohua Zhan: Formalizations in set theory: challenges and opportunities ↓ 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. (Kiguli Room) |

10:30 - 11:00 | Group discussions and closing (Kiguli Room) |

11:00 - 11:01 | Check-out by 11AM (Juniper Front Desk) |

12:00 - 13:30 | Lunch Buffet (Juniper Bistro) |