A Formalization of Divided Powers in Lean
Antoine Chambert-Loir, María Inés de Frutos-Fernández
cs.LO
Jul 7, 2025 · v1
TL;DR
First formalization in Lean 4 of divided power structures, including morphisms, sub-ideals, quotients, and sums.
Abstract
Given an ideal $I$ in a commutative ring $A$, a divided power structure on $I$ is a collection of maps $\{γ_n \colon I \to A\}_{n \in \mathbb{N}}$, subject to axioms that imply that it behaves like the family $\{x \mapsto \frac{x^n}{n!}\}_{n \in \mathbb{N}}$, but which can be defined even when division by factorials is not possible in $A$. Divided power structures have important applications in diverse areas of mathematics, including algebraic topology, number theory and algebraic geometry. In this article we describe a formalization in Lean 4 of the basic theory of divided power structures, including divided power morphisms and sub-divided power ideals, and we provide several fundamental constructions, in particular quotients and sums. This constitutes the first formalization of this theory in any theorem prover. As a prerequisite of general interest, we expand the formalized theory of multivariate power series rings, endowing them with a topology and defining evaluation and substitution of power series.
Problem
Divided power structures (maps behaving like x^n/n! even when division by factorials is impossible) have important applications in algebraic topology, number theory, and algebraic geometry, but no formalization of this theory existed in any theorem prover.
Approach
The formalization in Lean 4 covers the basic theory of divided power structures, including divided power morphisms, sub-divided power ideals, and fundamental constructions (quotients and sums). As a prerequisite, the authors expand the formalized theory of multivariate power series rings, endowing them with a topology and defining evaluation and substitution of power series.
Results
This constitutes the first formalization of divided power theory in any theorem prover. The development includes the exponential module construction built on a newly formalized topology for multivariate power series rings in Lean 4/Mathlib.
