Univalent Foundations of Constructive Algebraic Geometry

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 c...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2024-07
Main Author: Zeuner, Max
Format: Article
Language:English
Subjects:
Foundation construction
Foundations
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2331-8422