Programme
Contents of lectures, summary.
Condensed mathematics.
Condensed mathematics solves one of the fundamental defects of topological spaces, namely that they do not mix well with algebraic structures. For example, the category of topological abelian groups behaves quite poorly, with no good notion of kernel, cokernel or image available. In the condensed world we replace topological spaces by so-called condensed sets, which are very close to topological spaces but allow for more flexibility and in particular provide a beautiful theory of condensed abelian groups. After establishing the foundations of this formalism, we will explore some of its applications. An important notion is that of "completion", which leads to the theory of solid and liquid modules. With the theory of solid modules at hand, we can then reprove coherent duality on schemes in a very conceptual way (without any noetherianess assumptions).
Liquid Tensor Experiment.
The second lecture course will revolve around computer verified mathematics, explaining the principles behind a computer verification of a fundamental theorem in condensed mathematics: the main theorem of liquid vector spaces. We will start by giving an introduction of computer verified mathematics, using the Lean theorem prover as example to get hands on experience. We will get familiar with algebra and topology in Lean, which motivates why it is in principle possible to completely verify something like condensed mathematics. We will then switch to the theory of liquid vector spaces, give an overview of the main theorem, and explain how it can be applied in complex geometry.
Schedule od lectures and exercises.
Monday
- Condensed: Condensed sets
- Lean/LTE: Hands-on introduction to proof assistants
- Exercises: On the Lean side, the goal would be that everybody has a working installation, and maybe do some levels from the Natural Number Game
Tuesday
- Condensed: Condensed abelian groups
- Lean/LTE: Algebra in Lean
Wednesday
- Condensed: Solid abelian groups
- Lean/LTE: Topology in Lean
Thursday
- Condensed: Analytic rings
- Lean/LTE: The analytic ring structure on the real numbers
Friday
- Condensed: Application to coherent duality for schemes
- Lean/LTE: Applications of liquid mathematics
Preparation at home
- If possible, bring a laptop with ≥ 8GB RAM.
- Try to install Lean on your laptop, following the "Regular install" instructions at https://leanprover-community.github.io/get_started.html#regular-install
- If you get stuck, please ask for help at https://leanprover.zulipchat.com/
- If you want, you can try the Natural Number Game to gain a bit of experience: https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/