Formalizing the divided power envelope in Lean

Add to your list(s) Download to your calendar using vCal

• María Inés de Frutos-Fernández (University of Bonn)
• Thursday 14 November 2024, 17:00-18:00
• MR14 Centre for Mathematical Sciences.

If you have a question about this talk, please contact Jonas Bayer.

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.

Recording: https://youtu.be/QCRLwC5JQw0

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Cambridge talks
• DPMMS Lists
• DPMMS Pure Maths study groups
• DPMMS info aggregator
• DPMMS lists
• Department of Computer Science and Technology talks and seminars
• Formalisation of mathematics with interactive theorem provers
• Hanchen DaDaDash
• Interested Talks
• MR14 Centre for Mathematical Sciences
• School of Physical Sciences
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.