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:20241114T170000Z
DTEND:20241114T180000Z
UID:TALK222778@talks.cam.ac.uk
CONTACT:Jonas Bayer
DESCRIPTION:Given an ideal I in a commutative ring A\, a divided power str
 ucture on I is a collection of maps $\\gamma_n : I \\to I$ indexed by $\\m
 athbb{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 structu
 re 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 high
 ly technical definition of the Fontaine period ring B_cris\, which is used
  to identify crystalline Galois representations and in the comparison theo
 rem between étale and crystalline cohomology.\n\nIn this talk I will desc
 ribe ongoing joint work with Antoine Chambert-Loir towards formalizing the
  divided power envelope in the Lean 4 theorem prover. This project has alr
 eady resulted in numerous contributions to the Mathlib library\, including
  in particular the theory of weighted polynomial rings\, and substitution 
 of power series.\n\nRecording: https://youtu.be/QCRLwC5JQw0
LOCATION:MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR