We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

math.LO

Change to browse by:

References & Citations

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Mathematics > Logic

Title: A Univalent Formalization of Affine Schemes

Abstract: We present a formalization of affine schemes in the Cubical Agda proof assistant. This development is fully constructive and 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 Zariski spectrum, but otherwise proceeds by defining the structure sheaf on basic opens and then lift it to the whole spectrum. This approach 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 give a formal account of this "lift from basis" approach and obtain a fully formalized constructive account of affine schemes.
Subjects: Logic (math.LO)
Cite as: arXiv:2212.02902 [math.LO]
  (or arXiv:2212.02902v1 [math.LO] for this version)

Submission history

From: Max Zeuner [view email]
[v1] Tue, 6 Dec 2022 11:55:00 GMT (54kb)

Link back to: arXiv, form interface, contact.