Schemes in Lean
The content of this repository is the result of completely refactoring the lean-stacks-project, in which parts of The Stacks Project are formally verified using the Lean Theorem Prover. In particular, some bits of Chapters 6, 10 and 25 are formalized, culminating with the definition of a scheme. Having learnt from the many problems encountered in that first attempt, we present a cleaner and more robust approach. The main improvements are:
- The definition of a locally ringed space. Even though a scheme is technically a locally ringed space with a certain property, the previous definition, which is mathematically equivalent, did not involve locally ringed spaces.
- The use of the
is_localizationpredicate, defined by Prof Neil Strickland here, throughout instead of the concrete construction of a localized ring. Thanks to this, we avoided complicated arguments about canonically isomorphic rings.
- Usability. We have re-structured the previous repository and re-named all the files and many of the definitions and lemmas with the intention of providing a usable interface.
Note that this is still very much a work in progress. Some further clean-up is necessary, many proofs can be simplified and the API needs to be tested with more examples of schemes.
This is a general overview of the maths that you can find in this repository.
sheaves directory we have:
- Presheaves of sets and of rings on a topological space and on a basis. Similarly, we define sheaves and stalks and prove some basic lemmas about them.
- The construction of the extension of a presheaf on a basis to a presheaf on the whole space with the usual properties.
- Locally ringed spaces.
spectrum_of_a_ring, there is:
- The definition of the topological space Spec(R) together with some general properties such as compactness and some lemmas about the basic opens.
- The structure presheaf defined on the basic opens and the proof of the sheaf property, which spans several files.
- The proof that Spec(R) is a locally ringed space.
Finally, a scheme is defined in
scheme.lean and two examples (the empty scheme and affine schemes) are provided in
instances. There is also a
to_mathlib directory with some general results that we found useful.
To get it working, you will need Lean 3.4.2, available here. Clone the repository and type:
cd lean-scheme leanpkg configure leanpkg build
The main contributors to this project are: