← All papers
Graded Rings in Lean's Dependent Type Theory
cs.LO
Sep 1, 2022 · v1
TL;DR
Formalizes graded rings and their properties in Lean's mathlib using dependent type theory.
Abstract
This paper describes the formalization of graded rings and their properties in the Lean theorem prover using mathlib. Graded rings are algebraic structures that decompose as a direct sum of abelian groups indexed by a monoid, and they arise naturally in commutative algebra and algebraic geometry. The authors discuss design decisions for representing graded structures in dependent type theory and the challenges of working with direct sum decompositions.
Problem
Graded rings (algebraic structures decomposing as direct sums of abelian groups indexed by a monoid) arise naturally in commutative algebra and algebraic geometry, but representing them in dependent type theory raises non-trivial design questions.
Approach
The authors formalize graded rings and their properties in Lean using mathlib. The paper discusses design decisions for representing graded structures in dependent type theory and the challenges of working with direct sum decompositions within Lean's type system.
Results
A working formalization of graded rings is contributed to mathlib, with design decisions documented for representing indexed decompositions in dependent type theory.