Formalizing Polynomial Laws and the Universal Divided Power Algebra
Antoine Chambert-Loir, María Inés de Frutos-Fernández
TL;DR
The work targets a Lean/Mathlib formalization of Roby’s universal divided power algebra, a foundational tool in crystalline cohomology and $p$-adic Hodge theory. It develops the theory of polynomial laws, including coefficients, homogeneity, and divided differentials, and constructs the universal divided power algebra $\Gamma_R(M)$ with its graded structure and base-change behavior. The authors confront substantial formalization challenges—universes, semiring generality, and implicit "invisible" mathematics—while delivering a robust API and groundwork toward a complete DP-structure and the divided power envelope. Future efforts will complete the Taylor formula and DP structure, enabling formalization of the divided power envelope and connections to Fontaine $B_{crys}$ within Lean.
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".