Given an ideal I in a commutative ring A, a divided power structure on I is a collection of maps I -> I, indexed by the natural numbers, which behave like the family x^n/n!, but which can be defined even if division by integers is not defined in A. From a divided power structure on I and an ideal J in an A-algebra B, one can construct the “divided power envelope” D_B(J), consisting of a B-algebra D with a given ideal J_D and a divided power structure satisfying a universal property and a compatibility condition. The divided power envelope is needed for the highly technical definition of the Fontaine period ring B_cris, which is used to identify crystalline Galois representations and in the comparison theorem between étale and crystalline cohomology.
In this talk I will describe ongoing joint work with Antoine Chambert-Loir towards formalizing the divided power envelope in the Lean 4 theorem prover. This project has already resulted in numerous contributions to the Mathlib library, including in particular the theory of weighted polynomial rings, and substitution of power series.
