← All papers
Formalising the Proj Construction in Lean
cs.LO
Jan 1, 2020 · v1
TL;DR
Formalizes the Proj scheme construction from algebraic geometry in Lean's mathlib library.
Abstract
This paper presents a formalization of the Proj construction in algebraic geometry using the Lean theorem prover and its mathlib library. The Proj construction associates to a graded ring a scheme, and is fundamental in algebraic geometry for constructing projective varieties and projective space. The formalization covers the construction of the homogeneous spectrum, its structure sheaf, and the proof that the result is a scheme.
Problem
The Proj construction in algebraic geometry (associating a scheme to a graded ring) is fundamental for constructing projective varieties, but it had not been formalized in a theorem prover.
Approach
The authors formalize the Proj construction in Lean using the Mathlib library. The formalization covers the homogeneous spectrum, its structure sheaf, and the proof that the result is a scheme.
Results
A complete formalization of the Proj construction is achieved in Lean with Mathlib, covering all steps from the homogeneous spectrum through the structure sheaf to the final scheme result.