A Univalent Formalization of Constructive Affine Schemes

TL;DR

This paper formalizes constructive affine schemes in Cubical Agda using univalence, providing a fully constructive, predicative approach that differs from traditional non-constructive formalizations.

Contribution

It introduces a novel formalization of constructive affine schemes leveraging univalence and point-free topology, enabling a constructive and predicative development.

Findings

Successfully formalized the structure sheaf on the Zariski lattice

Demonstrated the use of univalence to lift from basis in formalization

Achieved a fully constructive and predicative formalization of affine schemes

Abstract

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.