Institution
Axiom (United States)
UScompany
Recent research
- AI & ComputingOpen access
Formalizing Multi-graded Brenner–Schröer Proj Schemes and Dilatations of Rings in Lean4
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...