I'll report on a project I'm carrying out with María-Inés de Frutos Fernández to formalize the theory of divided powers. Discovered by Cartan in a context of algebraic topology, this algebraic tool was developed in the 1960s by Roby and is at the heart of the construction of crystalline cohomology. In particular, I will discuss the construction of divided powers on the augmentation ideal of the divided-power algebra.
Les travaux de recherche d'Antoine Chambert-Loir s'inscrivent le plus souvent en géométrie diophantienne (question de Manin sur les points de hauteur bornée) et en géométrie non archimédienne (construction d'une théorie de formes différentielles et courants réels). Depuis 2021, il s'intéresse à la formalisation mathématique, en concentrant son attention sur des résultats peu spectaculaires au premier abord, comme la théorie des actions de groupes ou celle des puissances divisées.
