Resolution of Singularities in Characteristic Zero🔗

This document presents the statements of the Lean library hironaka, a formalization over Mathlib of resolution of singularities in characteristic zero: Hironaka's theorems of 1964 and the functorial and analytic forms given later by Kollár, Włodarczyk, and Bierstone and Milman. Every theorem it presents is proved in the library and checked by Lean's kernel. The document explains what each theorem says, how the formal statement relates to the source it follows, and what every definition used by the statements means; the proofs are only sketched.

The document has five parts. The introduction recalls what resolution of singularities and principalization are, lists the theorems, and explains how to read a node. Two parts then describe the objects and operations in terms of which the theorems are stated, one for schemes and one for analytic geometry. The main theorems follow. They open with two statements whose files import Mathlib only: resolution of a variety by a single blow-up, which is Hironaka's Main Theorem I, and the local monomialization of a real-analytic function. Then come two strands: algebraic schemes, with Hironaka's Main Theorems I, II and II(N) and Corollaries 1 and 3, Kollár's functorial principalization and resolution and his strong resolution of a variety, and Włodarczyk's embedded desingularization; and analytic manifolds and spaces, with Hironaka's Main Theorem II″(N), Bierstone–Milman's principalization, Włodarczyk's functorial principalization and embedded desingularization, and the resolution of real- and complex-analytic spaces [Kol07, Theorem 45]. In the section of each theorem, the properties it asserts and the inputs particular to it are stated before the theorem; a property asserted by several theorems is stated at the first of them. The appendix holds a dictionary from the classical notions to their names in Mathlib and the library, the conventions and the sources. Every declaration on which a main theorem's statement depends is embedded at some node; the dependency graph and the summary at the end are computed from the Lean declarations.

The library was produced by an automated formalization process, directed and audited at Resolution, following the human-written sources of its bibliography.