arXiv · 2407.17362
Univalent Foundations of Constructive 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.
Explore related subjects
Keep this discovery
Max Zeuner. 2024-07-24. Univalent Foundations of Constructive Algebraic Geometry. https://arxiv.org/abs/2407.17362
Cite the original work for its findings. Save a collection to share your selection of sources.