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)
• Tuesday 10 June 2025, 15:30-16:30
• Seminar Room 1, Newton Institute.

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

BPRW03 - Big proof: formalizing mathematics at scale

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.

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

• All CMS events
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• Seminar Room 1, Newton Institute
• bld31

Note that ex-directory lists are not shown.