We present a formalization of constructive affine schemes in the Cubical Agda
proof assistant. This development is not only fully constructive and
predicative, it also makes crucial use of univalence. By now schemes have been
formalized in various proof assistants. However, most existing formalizations
follow the inherently non-constructive approach of Hartshorne's classic
"Algebraic Geometry" textbook, for which the construction of the so-called
structure sheaf is rather straightforwardly formalizable and works the same
with or without univalence. We follow an alternative approach that uses a
point-free description of the constructive counterpart of the Zariski spectrum
called the Zariski lattice and proceeds by defining the structure sheaf on
formal basic opens and then lift it to the whole lattice. This general strategy
is used in a plethora of textbooks, but formalizing it has proved tricky. The
main result of this paper is that with the help of the univalence principle we
can make this "lift from basis" strategy formal and obtain a fully formalized
account of constructive affine schemes.
José A. Alonso
All GNU social JP content and data are available under the Creative Commons Attribution 3.0 license.