A Formalization of Divided Powers in Lean

Abstract

Given an ideal $I$ in a commutative ring $A$, a divided power structure on $I$ is a collection of maps $\{{\hat{I}}_n^3: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.

16th International Conference on Interactive Theorem Proving (ITP '25), 2025, Reykjavik, Iceland