Graded Rings in Lean’s Dependent Type Theory

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.

1. 1.

   Or “a graded algebra of type \(\mathbb {N}\) over the ring R with graduation A” in the language of [6, III, §3, 1.].

2. 2.

   Where \(\mathcal {C}\ell (V, Q)\) is notation to specify the quadratic form Q and vector space V.

3. 3.

   At least, when \(Q\ne 0\). If \(Q = 0\) then \(\mathcal {C}\ell (V, Q) = \mathcal {\bigwedge }(V)\) and we can proceed as above.

4. 4.

   Note that literature referring to an \(\mathbb {N}\)-grading is referring to the grading on \(\mathcal {\bigwedge }(V)\) via the canonical module equivalence.

5. 5.

   https://en.wikipedia.org/wiki/Centipede_mathematics.

6. 6.

   Some sources use a more general definition of graded R-modules and R-algebras, where R is itself a graded ring such that \(R_iM_j \subseteq M_{i+j}\). For brevity we will not discuss these here (in essence considering only the special case when R has the trivial graduation), but our approach would extends to this straightforwardly .

7. 7.

   In the absence of our work a proof via convexity was used instead.

8. 8.

   Chosen for brevity due to having the fewest axioms, not because they are interesting.

9. 9.

   Lean 4 lifts this notation restriction, but the algebraic typeclasses provided by mathlib would need reworking.

10. 10.

    The syntax in Lean for an incomplete proof.

11. 11.

    After enabling the appropriate by-default-disabled instances.

12. 12.

    Thus resolving the further work in [14, §8.1].

13. 13.

    source lines of code.

14. 14.

    Tracked in https://github.com/leanprover-community/mathlib/projects/12.

15. 15.

    In geometric algebra and algebraic geometry, respectively!.

The authors would like to thank Kevin Buzzard for his justified insistence on needing an interface to talk about internal gradings, Anne Baanen for picking up the mantle dropped by the first author on the rest of the set_like refactor, and the rest of the mathlib community for the extraordinarily collaborative work providing the context for this paper. The first author is funded by a scholarship from the Cambridge Trust. The second author is funded by the Schrödinger Scholarship Scheme from Imperial College London.

Authors and Affiliations

1. Cambridge University Engineering Department, Cambridge, UK

   Eric Wieser

2. Imperial College London, London, UK

   Jujian Zhang

Corresponding author

Correspondence to Eric Wieser .

Editors and Affiliations

1. Imperial College London, London, UK

   Kevin Buzzard

2. Johannes Kepler University Linz, Linz, Austria

   Temur Kutsia

Reprints and permissions

© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG

Policies and ethics