44th Autumn School in Algebraic Geometry
Condensed mathematics and the liquid tensor experiment
Teachers: Johan M. Commelin (Freiburg) and Lucas Mann (Bonn)
Lecture series:
- Lucas Mann: 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 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).
- Johan M. Commelin : Liquid Tensor Experiment
This lecture course revolves 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 start by giving an introduction of computer verified mathematics, using the Lean theorem prover as example to get hands on experience. We get familiar with algebra and topology in Lean, which motivates why it is in principle possible to completely verify something like condensed mathematics. Then we 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.
Resources:
Organizers: Karin Schaller (Freie Uni, Berlin), Jaroslaw Wisniewski (University of Warsaw)
The school was supported by:
Institute of Mathematics,
Faculty of Mathematics, Informatics and Mechanics, the University of
Warsaw, IDUB, Banach Center
Conference picture
September Schools Homepage