Formalizing multi-graded Brenner-Schr\"oer Proj schemes and dilatations of rings in Lean4
1 Pith paper cite this work. Polarity classification is still indexing.
1
Pith paper citing it
abstract
We present a detailed formalization in Lean4 of some multigraded algebraic geometry constructions, focusing on the Brenner--Schr\"oer Proj construction and algebraic dilatations of rings.