A Formalization of Divided Powers in Lean

TL;DR

This paper formalizes the theory of divided power structures within Lean 4, enabling rigorous reasoning in algebraic geometry and related fields, and extends formalization to multivariate power series rings.

Contribution

It provides the first formalization of divided power structures in a theorem prover, including morphisms, sub-ideals, quotients, and sums, with an extension to power series rings.

Findings

First formalization of divided power structures in a theorem prover

Includes fundamental constructions like quotients and sums

Extends formalized theory to multivariate power series rings

Abstract

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