Univalent Foundations of Constructive Algebraic Geometry

TL;DR

This paper proves in Homotopy Type Theory that two different constructive definitions of quasi-compact and quasi-separated schemes are equivalent, establishing a foundational link in algebraic geometry.

Contribution

It provides the first univalent proof showing the equivalence of two constructive approaches to qcqs-schemes within Homotopy Type Theory.

Findings

Constructive proof of equivalence between two definitions of qcqs-schemes.

Establishment of an equivalence between categories of qcqs-schemes.

Application of Homotopy Type Theory to foundational algebraic geometry.

Abstract

We investigate two constructive approaches to defining quasi-compact and quasi-separated schemes (qcqs-schemes), namely qcqs-schemes as locally ringed lattices and as functors from rings to sets. We work in Homotopy Type Theory and Univalent Foundations, but reason informally. The main result is a constructive and univalent proof that the two definitions coincide, giving an equivalence between the respective categories of qcqs-schemes.