Formalizing Polynomial Laws and the Universal Divided Power Algebra
Antoine Chambert-Loir, María Inés de Frutos-Fernández
cs.LO
Dec 5, 2025 · v1
TL;DR
Formalizes polynomial laws and the universal divided power algebra and its graded structure in Lean/Mathlib.
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".
Problem
The universal divided power algebra, constructed by Roby (1965), is needed for crystalline cohomology and p-adic Hodge theory, but its construction involves subtle algebraic steps (polynomial laws, divided power structures on augmentation ideals) that had not been formalized.
Approach
The authors formalize polynomial laws and the initial steps of the universal divided power algebra construction in Lean 4 / Mathlib. They define polynomial laws as natural transformations on tensor products satisfying a homogeneity condition, and identify the graded pieces with homogeneous polynomial laws. The formalization confronts universe management, extension from rings to semirings, and instances of invisible mathematics.
Results
The first steps of the theory of polynomial laws are formalized. The paper reports on difficulties including universe polymorphism, extending Mathlib to semirings, and handling mathematically implicit constructions. Full construction of the divided power structure is identified as future work.
