Formalizing multi-graded Brenner-Schr\"oer Proj schemes and dilatations of rings in Lean4

Computer Science > Logic in Computer Science [Submitted on 31 May 2026] Title:Formalizing multi-graded Brenner-Schröer Proj schemes and dilatations of rings in Lean4 View PDFAbstract: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. References & Citations Loading... Bibliographic and Citation Tools Bibliographic Explorer (What is the Explorer?) Connected Papers (What is Connected Papers?) Litmaps (What is Litmaps?) scite Smart Citations (What are Smart Citations?) Code, Data and Media Associated with this Article alphaXiv (What is alphaXiv?) CatalyzeX Code Finder for Papers (What is CatalyzeX?) DagsHub (What is DagsHub?) Gotit.pub (What is GotitPub?) Hugging Face (What is Huggingface?) ScienceCast (What is ScienceCast?) Demos Recommenders and Search Tools Influence Flower (What are Influence Flowers?) CORE Recommender (What is CORE?) arXivLabs: experimental projects with community collaborators Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.