A Formalization of Divided Powers in Lean
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915376350101504 |
|---|---|
| author | Chambert-Loir, Antoine de Frutos-Fernández, María Inés |
| author_facet | Chambert-Loir, Antoine de Frutos-Fernández, María Inés |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2507_05327 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Formalization of Divided Powers in Lean Chambert-Loir, Antoine de Frutos-Fernández, María Inés Logic in Computer Science Commutative Algebra 14F30 (Primary) 13J05 (Secondary) 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. |
| title | A Formalization of Divided Powers in Lean |
| topic | Logic in Computer Science Commutative Algebra 14F30 (Primary) 13J05 (Secondary) |
| url | https://arxiv.org/abs/2507.05327 |