License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2022.14
URN: urn:nbn:de:0030-drops-184574
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18457/
Zeuner, Max ;
Mörtberg, Anders
A Univalent Formalization of Constructive 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.
BibTeX - Entry
@InProceedings{zeuner_et_al:LIPIcs.TYPES.2022.14,
author = {Zeuner, Max and M\"{o}rtberg, Anders},
title = {{A Univalent Formalization of Constructive Affine Schemes}},
booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)},
pages = {14:1--14:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-285-3},
ISSN = {1868-8969},
year = {2023},
volume = {269},
editor = {Kesner, Delia and P\'{e}drot, Pierre-Marie},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18457},
URN = {urn:nbn:de:0030-drops-184574},
doi = {10.4230/LIPIcs.TYPES.2022.14},
annote = {Keywords: Affine Schemes, Homotopy Type Theory and Univalent Foundations, Cubical Agda, Constructive Mathematics}
}
