← All papers
Formalizing multi-graded Brenner-Schröer Proj schemes and dilatations of rings in Lean4
cs.LO
May 31, 2026 · v1
TL;DR
Formalizes multigraded Brenner-Schroeer Proj schemes and algebraic dilatations of rings in Lean4.
Abstract
We present a detailed formalization in Lean4 of some multigraded algebraic geometry constructions, focusing on the Brenner--Schröer Proj construction and algebraic dilatations of rings.
Problem
Multigraded algebraic-geometry constructions such as the Brenner-Schroeer Proj and algebraic dilatations of rings lacked a formal treatment.
Approach
The authors give a detailed Lean4 formalization of these multigraded constructions, focusing on the Brenner-Schroeer Proj construction and algebraic dilatations of rings.
Results
A formalized development of the multigraded Proj construction and ring dilatations in Lean4.