BCC

Condensed mathematics and the liquid tensor experiment

04.09.2022 - 10.09.2022 | Będlewo

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

 

 

 

Rewrite code from the image

Reload image

Reload image