2025/07/07 by Antoine Chambert-Loir, María Inés de Frutos-Fernández, Chambert-Loir, Antoine +1 · 1 citation
Computer Science · Mathematics · #14F30 (Primary) 13J05 (Secondary) #Algebraic Geometry and Number Theory #Commutative Algebra (math.AC) #Commutative Algebra and Its Applications #FOS: Computer and information sciences #FOS: Mathematics #Logic in Computer Science (cs.LO) #Polynomial and algebraic computation
paper · pdf · doi:10.48550/arxiv.2507.05327
openalex publication_date 2025/07/07 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Given an ideal I in a commutative ring A, a divided power structure on I is a collection of maps \γn \colon I → A\n ∈ ℕ, subject to axioms that imply that it behaves like the family \x ↦ (xn)/(n!)\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.