Formalizing Polynomial Laws and the Universal Divided Power Algebra

TL;DR

This paper formalizes Roby's universal divided power algebra within the Lean/Mathlib framework, focusing on polynomial laws and the construction of divided power structures, with implications for algebraic geometry and number theory.

Contribution

It introduces a formalization of polynomial laws and the universal divided power algebra in Lean, advancing the mechanization of algebraic structures used in cohomology theories.

Findings

Formalization of polynomial laws in Lean

Identification of graded pieces with universal structures

Discussion of challenges in formalizing algebraic universes

Abstract

The goal of this paper is to present an ongoing formalization, in the framework provided by the Lean/Mathlib mathematical library, of the construction by Roby (1965) of the universal divided power algebra. This is an analogue, in the theory of divided powers, of the classical algebra of polynomials. It is a crucial tool in the development of crystalline cohomology; it is also used in $p$-adic Hodge theory to define the crystalline period ring. As an algebra, this universal divided power algebra has a fairly simple definition that shows that it is a graded algebra. The main difficulty in Roby's theorem lies in constructing a divided power structure on its augmentation ideal. To that aim, Roby identified the graded pieces with another universal structure: homogeneous polynomial laws.We formalize the first steps of the theory of polynomial laws and show how future work will allow to complete the formalization of the above-mentioned divided power structure. We report on various difficulties that appeared in this formalization: taking care of universes, extending to semirings some aspects of the Mathlib library, and coping with several instances of "invisible mathematics".