18. Schemes🔗

This page explains how to express common concepts in scheme theory using the definitions in Mathlib. We assume basic knowledge of both Lean and algebraic geometry in the language of schemes.

Most declarations are in the AlgebraicGeometry namespace and since we rely on the language of category theory, we recommend to have the following namespaces open.

In what follows, most definitions are noncomputable. Starting with a noncomputable section is therefore recommended.

The exposition is split in the following subsections:

1. 18.1. Prime spectrum
2. 18.2. The unbundled vs. bundled barrier.
3. 18.3. Schemes
4. 18.4. Affine schemes
5. 18.5. Stalks, residue fields and fibres
6. 18.6. Subschemes
7. 18.7. Properties of morphisms
8. 18.8. Reduction to the affine case
9. 18.9. More topics