Formalizing Multi-graded Brenner–Schröer Proj Schemes and Dilatations of Rings in Lean4

Abstract

Abstract We present a formalization in Lean4 of some multi-graded algebraic geometry constructions, focusing on the Brenner–Schröer Proj construction and algebraic dilatations of rings. Multi-graded Proj schemes, defined from rings graded by more general monoids than $$\mathbb {N}$$ N or $$\mathbb {Z}$$ Z , have recently attracted increasing attention and play an important role in several areas of modern algebraic geometry. Our work follows the algebraic approach developed in the literature and provides a formal implementation of multi-graded Proj within the Lean4 theorem prover. In addition, we formalize dilatations of rings, an operation in commutative algebra closely related to localization and to blowup constructions. This article gives a comprehensive account of the definitions, main results, and design choices underlying the formalization. It is intended both as documentation of the development and as a foundation for future extensions in formalized algebraic geometry. The corresponding code is made publicly available, supporting further developments in the formalization of advanced geometric structures.