Colloque - Formalisation des mathématiques et types dépendants - Antoine Chambert-Loir : Sur la formalisation des puissances divisées
Description
Collège de France
Thierry Coquand
Informatique et sciences numériques (2024-2025)
Année 2024-2025
Colloque - Formalisation des mathématiques et types dépendants - Antoine Chambert-Loir : Sur la formalisation des puissances divisées
Antoine Chambert-Loir
Professeur, université Paris Cité
Résumé
Je ferai le point sur un travail de formalisation de la théorie des puissances divisées que je mène avec María-Inés de Frutos Fernández. Découvert par Cartan dans un contexte de topologie algébrique, cet outil algébrique a été développé dans les années 60 par Roby et est au cœur de la construction de la cohomologie cristalline. J'évoquerai en particulier la construction des puissances divisées sur l'idéal d'augmentation de l'algèbre à puissances divisées.
Antoine Chambert-Loir
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.
United States
