LIPIcs.ITP.2023.35.pdf
- Filesize: 0.87 MB
- 17 pages
Document
Formalising the Proj Construction in Lean
Author
Jujian Zhang 
-
Part of:
Volume:
14th International Conference on Interactive Theorem Proving (ITP 2023)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2023-07-26
File
Document Identifiers
Author Details
Acknowledgements
I want to thank Eric Wieser for his contribution and suggestion in formalising homogeneous ideals and homogeneous localisation; Andrew Yang and Junyan Xu for their review and comments on my code; Kevin Buzzard for suggesting this project and all the contributors to mathlib for otherwise this project would not have been possible.
Cite AsGet BibTex
Jujian Zhang. Formalising the Proj Construction in Lean. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 35:1-35:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ITP.2023.35
https://doi.org/10.4230/LIPIcs.ITP.2023.35
Abstract
Many objects of interest in mathematics can be studied both analytically and algebraically, while at the same time, it is known that analytic geometry and algebraic geometry generally do not behave the same. However, the famous GAGA theorem asserts that for projective varieties, analytic and algebraic geometries are closely related; the proof of Fermat’s last theorem, for example, uses this technique to transport between the two worlds [Serre, 1955]. A crucial step of proving GAGA is to calculate cohomology of projective space [Neeman, 2007; Godement, 1958], thus I formalise the Proj construction in the Lean theorem prover for any ℕ-graded R-algebra A and construct projective n-space as Proj A[X₀,… , X_n]. This is the first family of non-affine schemes formalised in any theorem prover.
Subject Classification
ACM Subject Classification
- Theory of computation → Logic and verification
- Mathematics of computing → Topology
Keywords
- Lean
- formalisation
- algebraic geometry
- scheme
- Proj construction
- projective geometry
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Anthony Bordg, Lawrence Paulson, and Wenda Li. Simple type theory is not too simple: Grothendieck’s schemes without dependent types. Experimental Mathematics, 31(2):364-382, 2022. URL: https://doi.org/10.1080/10586458.2022.2062073.
-
Kevin Buzzard, Chris Hughes, Kenny Lau, Amelia Livingston, Ramon Fernández Mir, and Scott Morrison. Schemes in Lean. Experimental Mathematics, 31(2):355-363, 2022.
-
Laurent Chicli. Une formalisation des faisceaux et des schémas affines en théorie des types avec Coq. PhD thesis, INRIA, 2001.
- Wei-Liang Chow. On compact complex analytic varieties. American Journal of Mathematics, 71(4):893-914, 1949. URL: http://www.jstor.org/stable/2372375.
- Mathlib Contributors. Lean mathlib. https://github.com/leanprover-community/mathlib, 2022.
- Mathlib Contributors. Mathlib documentation. https://leanprover-community.github.io/mathlib_docs, 2023.
-
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). In International Conference on Automated Deduction, pages 378-388. Springer, 2015.
-
Roger Godement. Topologie algébrique et théorie des faisceaux. Publications de, 1, 1958.
-
Robin Hartshorne. Graduate texts in mathematics. Algebraic Geometry, 52, 1977.
-
Saunders MacLane and Ieke Moerdijk. Sheaves in geometry and logic: A first introduction to topos theory. Springer Science & Business Media, 2012.
-
Anders Mörtberg and Max Zeuner. Towards a formalization of affine schemes in cubical agda.
-
Amnon Neeman. Algebraic and analytic geometry. Cambridge University Press, 2007.
-
Jean-Pierre Serre. Géométrie analytique et géométrie algébrique. Ann. Inst. Fourier, VI (1955-56), pages 1-42, 1955.
- The Stacks Project Authors. Stacks Project. https://stacks.math.columbia.edu, 2018.
-
Ravi Vakil. The rising sea: Foundations of algebraic geometry. 2017. URL http://virtualmath1. stanford. edu/~ vakil/216blog, 24:29, 2017.
- Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et al. UniMath - a computer-checked library of univalent mathematics. available at http://unimath.org. URL: https://github.com/UniMath/UniMath.
-
Eric Wieser and Jujian Zhang. Graded rings in Lean’s dependent type theory. In International Conference on Intelligent Computer Mathematics, pages 122-137. Springer, 2022.