License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2023.35
URN: urn:nbn:de:0030-drops-184105
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18410/
Zhang, Jujian
Formalising the Proj Construction in Lean
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.
BibTeX - Entry
@InProceedings{zhang:LIPIcs.ITP.2023.35,
author = {Zhang, Jujian},
title = {{Formalising the Proj Construction in Lean}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {35:1--35:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18410},
URN = {urn:nbn:de:0030-drops-184105},
doi = {10.4230/LIPIcs.ITP.2023.35},
annote = {Keywords: Lean, formalisation, algebraic geometry, scheme, Proj construction, projective geometry}
}
