Document Open Access Logo

The Functor of Points Approach to Schemes in Cubical Agda

Authors Max Zeuner , Matthias Hutzler

PDF
Thumbnail PDF

File

LIPIcs.ITP.2024.38.pdf
  • Filesize: 0.91 MB
  • 18 pages

Document Identifiers

Author Details

Max Zeuner
  • Department of Mathematics, Stockholm University, Sweden
Matthias Hutzler
  • Department of Computer Science and Engineering, Gothenburg University, Sweden

Funding

This paper is based upon research supported by the Swedish Research Council (SRC, Vetenskapsrådet) under Grant No. 2019-04545.

Acknowledgements

We would like to thank Felix Cherubini, Thierry Coquand and Anders Mörtberg for their support and feedback throughout this project.

Cite AsGet BibTex

Max Zeuner and Matthias Hutzler. The Functor of Points Approach to Schemes in Cubical Agda. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 38:1-38:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ITP.2024.38

Abstract

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Constructive mathematics
  • Theory of computation → Type theory
Keywords
  • Schemes
  • Algebraic Geometry
  • Category Theory
  • Cubical Agda
  • Homotopy Type Theory and Univalent Foundations
  • Constructive Mathematics

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. Carlo Angiuli, Evan Cavallo, Anders Mörtberg, and Max Zeuner. Internalizing Representation Independence with Univalence. Proc. ACM Program. Lang., 5(POPL), January 2021. URL: https://doi.org/10.1145/3434293.
  2. Ingo Blechschmidt. Using the internal language of toposes in algebraic geometry, 2021. URL: https://arxiv.org/abs/2111.03685.
  3. Anthony Bordg, Lawrence C. Paulson, and Wenda Li. Simple type theory is not too simple: Grothendieck’s schemes without dependent types. Exp. Math., 31(2):364-382, 2022. URL: https://doi.org/10.1080/10586458.2022.2062073.
  4. Kevin Buzzard, Chris Hughes, Kenny Lau, Amelia Livingston, Ramon Fernández Mir, and Scott Morrison. Schemes in lean. Exp. Math., 31(2):355-363, 2022. URL: https://doi.org/10.1080/10586458.2021.1983489.
  5. Tim Cherganov. Sheaf of rings on Spec R, 2022. URL: https://github.com/UniMath/UniMath/pull/1385.
  6. Felix Cherubini, Thierry Coquand, and Matthias Hutzler. A Foundation for Synthetic Algebraic Geometry, 2023. URL: https://arxiv.org/abs/2307.00073.
  7. Laurent Chicli. Une formalisation des faisceaux et des schémas affines en théorie des types avec coq. In Pierre Castéran, editor, Journées francophones des langages applicatifs (JFLA'01), Pontarlier, France, Janvier, 2001, number RR-4216 in Collection Didactique, pages 17-32. INRIA, June 2001. URL: https://hal.inria.fr/inria-00072403.
  8. Thierry Coquand, Henri Lombardi, and Peter Schuster. Spectral Schemes as Ringed Lattices. Annals of Mathematics and Artificial Intelligence, 56(3):339-360, 2009. URL: https://doi.org/10.1007/s10472-009-9160-7.
  9. Tom de Jong and Martín Hötzel Escardó. On Small Types in Univalent Foundations. Logical Methods in Computer Science, Volume 19, Issue 2, May 2023. URL: https://doi.org/10.46298/lmcs-19(2:8)2023.
  10. Pierre Deligne and Jean-François Boutot. Cohomologie étale: les points de départ. In Cohomologie Etale, pages 4-75, Berlin, Heidelberg, 1977. Springer Berlin Heidelberg. Google Scholar
  11. Pierre Deligne and Jean-François Boutot. Étale cohomology: starting points. Translated by J. S. Milne, 2022. URL: https://web.archive.org/web/20240511093708/https://www.jmilne.org/math/Documents/DeligneArcata.pdf.
  12. Michel Demazure and Peter Gabriel. Introduction to Algebraic Geometry and Algebraic Groups. Elsevier, 1980. Google Scholar
  13. David Eisenbud and Joe Harris. The Geometry of Schemes, volume 197. Springer Science & Business Media, 2006. Google Scholar
  14. Luis Español. Le spectre d'un anneau dans l'algèbre constructive et applications à la dimension. Cahiers de Topologie et Géométrie Différentielle Catégoriques, 24(2):133-144, 1983. URL: http://www.numdam.org/item/CTGDC_1983__24_2_133_0/.
  15. Ulrich Görtz and Torsten Wedhorn. Algebraic Geometry I: Schemes. Springer, 2020. Google Scholar
  16. Alexandre Grothendieck and Federico Gaeta. Introduction to Functorial Algebraic Geometry: After a Summer Course. State University of New York at Buffalo, Department of Mathematics, 1974. URL: https://web.archive.org/web/20221013161204/https://ncatlab.org/nlab/files/GrothendieckIntrodFunctorialGeometryI1973.pdf.
  17. Robin Hartshorne. Algebraic geometry, volume 52 of Graduate texts in mathematics. Springer, 1977. URL: https://doi.org/10.1007/978-1-4757-3849-0.
  18. Martin Hofmann and Thomas Streicher. Lifting Grothendieck Universes. https://web.archive.org/web/20240405155732/https://www2.mathematik.tu-darmstadt.de/~streicher/NOTES/lift.pdf, 1997. Unpublished note.
  19. Peter T Johnstone. Sketches of an Elephant: A Topos Theory Compendium: Volume 2, volume 2. Oxford University Press, 2002. Google Scholar
  20. André Joyal. Les théoremes de Chevalley-Tarski et remarques sur l'algèbre constructive. Cahiers Topologie Géom. Différentielle, 16:256-258, 1976. Google Scholar
  21. Nicolai Kraus. The General Universal Property of the Propositional Truncation. In Hugo Herbelin, Pierre Letouzey, and Matthieu Sozeau, editors, 20th International Conference on Types for Proofs and Programs (TYPES 2014), volume 39 of Leibniz International Proceedings in Informatics (LIPIcs), pages 111-145, Dagstuhl, Germany, 2015. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.TYPES.2014.111.
  22. F. William Lawvere. Categories: Grothendieck’s 1973 Buffalo Colloquium, 2003. Category mailing list, March 30. URL: https://web.archive.org/web/20240418015152/https://www.mta.ca/~cat-dist/archive/2003/03-3.
  23. Saunders Mac Lane and Ieke Moerdijk. Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer Science & Business Media, 2012. Google Scholar
  24. David Madore. Comment définir efficacement ce qu'est un schéma, 2013. David Madore’s WebLog. URL: https://web.archive.org/web/20240418040920/http://www.madore.org/~david/weblog/d.2013-09-21.2160.definition-schema.html.
  25. Per Martin-Löf. An Intuitionistic Theory of Types: Predicative Part. In H. E. Rose and J. C. Shepherdson, editors, Logic Colloquium '73, volume 80 of Studies in Logic and the Foundations of Mathematics, pages 73-118. North-Holland, 1975. URL: https://doi.org/10.1016/S0049-237X(08)71945-1.
  26. Marc Nieper-Wißkirchen. Algebraische Geometrie. unpublished lecture notes, 2008. Google Scholar
  27. nLab authors. coverage. https://ncatlab.org/nlab/show/coverage, May 2024. URL: https://ncatlab.org/nlab/revision/coverage/42.
  28. nLab authors. matching family. https://ncatlab.org/nlab/show/matching+family, May 2024. URL: https://ncatlab.org/nlab/revision/matching+family/7.
  29. nLab authors. relative adjoint functor. https://ncatlab.org/nlab/show/relative+adjoint+functor, May 2024. URL: https://ncatlab.org/nlab/revision/relative+adjoint+functor/17.
  30. Marshall Harvey Stone. Topological Representations of Distributive Lattices and Brouwerian Logics. Časopis pro pěstování matematiky a fysiky, 67(1):1-25, 1938. Google Scholar
  31. Thomas Streicher. Investigations Into Intensional Type Theory. Habilitation thesis, Ludwig-Maximilians-Universität München, 1993. URL: https://web.archive.org/web/20240324013847/https://www2.mathematik.tu-darmstadt.de/~streicher/HabilStreicher.pdf.
  32. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  33. Ravi Vakil. The Rising Sea: Foundations of Algebraic Geometry. Preprint, 2024. URL: https://web.archive.org/web/20240507025011/http://math.stanford.edu/~vakil/216blog/FOAGfeb2124public.pdf.
  34. Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types. Journal of Functional Programming, 31:e8, 2021. URL: https://doi.org/10.1017/S0956796821000034.
  35. V. Voevodsky, B. Ahrens, D. Grayson, et al. UniMath: Univalent Mathematics. Available at URL: https://github.com/UniMath.
  36. Vladimir Voevodsky. Univalent Foundations, September 2010. Notes from a talk in Bonn. URL: https://web.archive.org/web/20240418032908/https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/Bonn_talk.pdf.
  37. Vladimir Voevodsky. Resizing Rules - their use and semantic justification, 2011. Slides from a talk at TYPES, Bergen, 11 September. URL: https://web.archive.org/web/20240405160805/https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/2011_Bergen.pdf.
  38. Vladimir Voevodsky. An experimental library of formalized mathematics based on the univalent foundations. Mathematical Structures in Computer Science, 25(5):1278-1294, 2015. URL: https://doi.org/10.1017/S0960129514000577.
  39. Max Zeuner and Anders Mörtberg. A Univalent Formalization of Constructive Affine Schemes. In Delia Kesner and Pierre-Marie Pédrot, editors, 28th International Conference on Types for Proofs and Programs (TYPES 2022), volume 269 of Leibniz International Proceedings in Informatics (LIPIcs), pages 14:1-14:24, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.TYPES.2022.14.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact