BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Formalizing the divided power envelope in Lean - María Inés De F
 rutos Fernández (University of Bonn)
DTSTART:20250610T143000Z
DTEND:20250610T153000Z
UID:TALK230626@talks.cam.ac.uk
DESCRIPTION:Given an ideal I in a commutative ring A\, a divided power str
 ucture on I is a collection of maps I -> I\, indexed by the natural number
 s\, 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 &ldquo\;divi
 ded power envelope&rdquo\; D_B(J)\, consisting of a B-algebra D with a giv
 en ideal J_D and a divided power structure satisfying a universal property
  and a compatibility condition. The divided power envelope is needed for t
 he highly technical definition of the Fontaine period ring B_cris\, which 
 is used to identify crystalline Galois representations and in the comparis
 on theorem between &eacute\;tale and crystalline cohomology.\nIn this talk
  I will describe ongoing joint work with Antoine Chambert-Loir towards for
 malizing the divided power envelope in the Lean 4 theorem prover. This pro
 ject has already resulted in numerous contributions to the Mathlib library
 \, including in particular the theory of weighted polynomial rings\, and s
 ubstitution of power series.
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR