Graded Rings in Lean’s Dependent Type Theory

Abstract

In principle, dependent type theory should provide an ideal foundation for formalizing graded rings, where each grade can be of a different type. However, the power of these foundations leaves a plethora of choices for how to proceed with such a formalization. This paper explores various different approaches to how formalization could proceed, and then demonstrates precisely how the authors formalized graded algebras in Lean’s mathlib. Notably, we show how this formalization was used as an API; allowing us to formalize various graded structures such as those on tuples, free monoids, tensor algebras, and Clifford algebras.