Showing math.AGShow all
2 papers · 1 filter
math.AG2024
Univalent Foundations of Constructive Algebraic Geometry
Max Zeuner
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…
math.AG2024
The Functor of Points Approach to Schemes in Cubical Agda
Max Zeuner, Matthias Hutzler
We present a formalization of quasi-compact and quasi-separated schemes (qcqs-schemes) in the Cubical Agda proof assistant. We follow Grothendieck's functor of points approach, whi…