Given an ideal I in a commutative ring A, a divided power structure on I is a collection of maps $\gamma_n : I \to I$ indexed by $\mathbb{N}$ which behave like the family $x^n/n!$, but which can be defined even if the characteristic of A is positive. 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.
=== Hybrid talk ===
Join Zoom Meeting https://cam-ac-uk.zoom.us/j/87143365195?pwd=SELTNkOcfVrIE1IppYCsbooOVqenzI.1
Meeting ID: 871 4336 5195
Passcode: 541180
