This is the central repository for the 2023 masterclass on the formalization of condensed mathematics, taking place in 2023 at Copehnagen.
This is the best way; you can edit files and experiment, and you won't lose them. It's also the hardest way: it involves typing stuff in on the command line.
In brief: first install Lean 4 following the installation instructions from the community webpage here.
Then download and install this project by typing
git clone git@github.com:adamtopaz/CopenhagenMasterclass2023
cd CopenhagenMasterclass2023
lake exe cache get
lake build
Finally, open the root directory of the project folder in VS Code (for example by typing code ., or by opening VS Code and then clicking File -> Open Folder and opening the CopenhagenMasterclass2023 folder). Say that you trust the authors of the code --
and you can now open the Lean files in the repository and Lean should run on them automatically.
Additional instructions for working on an existing Lean4 project can be found here.
This repository is configured for use with github's codespaces. To get started with codespaces in this repo, just click the green "code" icon to create a new codespace. More detailed instructions can be found here.
Each day is split in two, with lectures by KB and AT in the morning, and time for group work and discussions in the afternoon. The general plan for each day is listed below.
- Overview and logistics.
- Category theory in Lean4.
- Condensed objects in Lean4.
- Sheaves on
CompHaus,ProfiniteandExtrDisc. - Equivalences between the three categories of sheaves.
- Abelian Categories, Grothendieck's AB axioms.
- AB axioms for condensed abelian groups.