1. Formalising the Proj Construction in Lean
- Author
-
Jujian Zhang, Zhang, Jujian, Jujian Zhang, and Zhang, Jujian
- 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.
- Published
- 2023
- Full Text
- View/download PDF