2026-07-25T20:49:14Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20766 2024-09-02T10:03:25Z ddc:004 open_access

The Functor of Points Approach to Schemes in Cubical Agda Zeuner, Max Hutzler, Matthias Schemes Algebraic Geometry Category Theory Cubical Agda Homotopy Type Theory and Univalent Foundations Constructive Mathematics 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, which defines schemes, the quintessential notion of modern algebraic geometry, as certain well-behaved functors from commutative rings to sets. This approach is often regarded as conceptually simpler than the standard approach of defining schemes as locally ringed spaces, but to our knowledge it has not yet been adopted in formalizations of algebraic geometry. We build upon a previous formalization of the so-called Zariski lattice associated to a commutative ring in order to define the notion of compact open subfunctor. This allows for a concise definition of qcqs-schemes, streamlining the usual presentation as e.g. given in the standard textbook of Demazure and Gabriel. It also lets us obtain a fully constructive proof that compact open subfunctors of affine schemes are qcqs-schemes. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Max Zeuner and Matthias Hutzler 2024 Is Part Of LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2024.38 urn:nbn:de:0030-drops-207667 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.38 eng https://creativecommons.org/licenses/by/4.0/legalcode