1.1. Resolution of singularities🔗

Let X be an algebraic variety over a field k of characteristic zero. Most points of X are smooth, but some may be singular, like the vertex of the cone x^2 + y^2 = z^2 or the origin of the cusp y^2 = x^3. A resolution of singularities of X is a proper morphism \pi \colon X' \to X from a smooth variety X' that is an isomorphism over a dense open subset of X: the singular variety is replaced by a smooth one that differs from it only over a nowhere dense set. In the strong form [Kol07, (3)], \pi is an isomorphism over the whole smooth locus X^{ns}, and the preimage \pi^{-1}(\operatorname{Sing} X) of the singular locus is a divisor with simple normal crossings: near every point of X' there are local coordinates z_1, \dots, z_n in which it is a union of coordinate hyperplanes z_i = 0 (Normal crossings).

Hironaka proved in 1964 that every variety over a field of characteristic zero has a resolution, together with a number of stronger statements [Hir64]. His resolution, and every one since, is built from blow-ups. The blow-up of a smooth variety along a smooth closed subvariety Z replaces every point of Z by the projective space of the directions normal to Z at that point; it changes nothing away from Z, and the preimage of Z becomes a smooth hypersurface, the exceptional divisor. For the cusp, one blow-up of the plane at the origin turns the curve into a smooth one (Example: resolving the cusp). In general one needs a finite succession of blow-ups X_r \to X_{r-1} \to \cdots \to X_0, each centre chosen in the previous stage (Finite successions of blow-ups), and the difficulty of the theorem is to choose the centres so that the process ends with something smooth.

Two variants recur. In embedded resolution the singular variety Y lies in a smooth ambient variety X, and one blows up X along smooth centres until the strict transform of Y (the closure of the part of its preimage lying off the exceptional divisors) is smooth and crosses the exceptional divisors normally. In the analytic setting the same questions are asked of real- and complex-analytic manifolds and spaces; a space that is not compact may need infinitely many blow-ups, finitely many over each compact subset.

1.2. Principalization🔗

The proofs reduce resolution to a problem about ideals. Let I be a sheaf of ideals on a smooth variety X, locally generated by functions f_1, \dots, f_m. A principalization of I is a finite succession of blow-ups with smooth centres, with composite \Pi \colon X_r \to X, such that the pulled-back ideal \Pi^* I is the ideal sheaf of a divisor with simple normal crossings: near every point of X_r it is generated by a single monomial z_1^{a_1} \cdots z_n^{a_n} in suitable local coordinates. Principalizing the ideal of a subvariety Y of a smooth X, and stopping at the right moment, gives an embedded resolution of Y; and since every variety is locally a subvariety of a smooth one, a resolution of any variety can be glued from such local pieces, provided the choices are compatible [Kol07, §3].

Principalization proceeds by order reduction. The order of I at a point x is the largest d with I_x \subseteq \mathfrak{m}_x^d, the vanishing order of the generic member of I at x. If I has order d along a smooth centre and one blows it up, the pulled-back ideal factors as the d-th power of the ideal of the exceptional divisor times an ideal called the weak transform of I. With well-chosen centres the maximal order of the weak transform drops after finitely many blow-ups. Hironaka's Main Theorem II is one round of this, which lowers the maximal order; his Main Theorem II(N) repeats it until the weak transform is the unit ideal, so that \Pi^* I is a product of powers of the exceptional divisors. Throughout, the exceptional divisors accumulated so far, together with a boundary divisor given at the start, are kept in simple normal crossings with each other and with the next centre.

1.3. Functorial resolution🔗

Hironaka's theorems assert that a resolution exists. Later proofs make every choice by an algorithm and give a stronger statement: one rule assigns a succession of blow-ups to every variety at once, compatibly with smooth morphisms and with change of the base field. Kollár's functorial principalization and resolution [Kol07, Theorems 35 and 36], Włodarczyk's embedded desingularization [Wlo05, Theorem 1.0.2] and his principalization on analytic manifolds [Wlo09, Theorem 2.0.3] are stated in this form (Blow-up sequence functors). What the compatibility says is explained with functorial principalization (Definition 4.2.4.3), and why it amounts to Kollár's resolution functor with functorial resolution (Functorial resolution).

1.4. The resolution theorems of the library🔗

The library states the following resolution theorems, each with its source. Each is stated in the form its source gives it, as far as Lean and Mathlib allow; where the formal statement differs from the printed one, the difference and the reason for it are recorded at the theorem (How to read a node).

In Mathlib's language (Resolution of singularities in Mathlib's language):

• Hironaka's Main Theorem I: resolution of an integral scheme of finite type over a field k of characteristic zero by a single blow-up along an ideal sheaf supported on the singular locus, from a scheme smooth over k, with blow-ups given by their universal property (Theorem 4.1.1.3);

• the local monomialization of a real-analytic function on an open subset of \mathbb{R}^n, with the Jacobian determinant in the same coordinates [Ati70] (Theorem 4.1.2.2).

Over a field k of characteristic zero, for schemes of finite type (Algebraic schemes):

• Hironaka's Main Theorem II, one round of order reduction (Theorem 4.2.1.2), and Main Theorem II(N), principalization of an ideal sheaf on a smooth scheme (Theorem 4.2.2.1);

• Hironaka's Corollary 1, which makes one of finitely many ideal sheaves the unit ideal at every point (Theorem 4.2.3.2), and Corollary 3, which turns the inverse image of a nowhere dense closed subscheme into a normal crossings divisor (Theorem 4.2.5.1);

• Kollár's functorial principalization (Theorem 4.2.4.6) and functorial resolution (Theorem 4.2.6.3), and his strong resolution of a variety (Theorem 4.2.7.1);

• Hironaka's Main Theorem I, which resolves a reduced and irreducible scheme by one blow-up with centre supported on the singular locus (Theorem 4.2.8.1), and its weak form (Theorem 4.2.9.1);

• Włodarczyk's embedded desingularization with smooth centres, in functorial form (Theorem 4.2.10.4).

For real- and complex-analytic manifolds and spaces (Analytic manifolds and analytic spaces):

• Hironaka's principalization on a real-analytic manifold, Main Theorem II″(N) (Theorem 4.3.1.2), and Bierstone–Milman's principalization with a condition on the Jacobian ideal (Theorem 4.3.2.1), both stated over every compact subset, compatibly;

• Włodarczyk's principalization on a real- or complex-analytic manifold, in functorial form: one rule for all manifolds of a given dimension, compatible with local analytic isomorphisms (Theorem 4.3.3.7);

• Włodarczyk's embedded desingularization of a closed analytic subspace of a manifold (Theorem 4.3.4.6);

• the resolution of reduced real- and complex-analytic spaces after Kollár and Włodarczyk (Theorem 4.3.5.5), and its form for a single reduced complex space (Theorem 4.3.6.1).

Every theorem is proved in the library and checked by Lean's kernel, with no axioms beyond the three standard ones of Lean and Mathlib; each is followed by a short sketch of the route its proof takes.

1.5. How to read a node🔗

Each main theorem, and each definition its statement uses, is a numbered node. The statement at the top is written by hand, in the source's notation; the Lean declaration below it is what Lean checks.

The boxes under a node record how the Lean statement relates to its source. A Translation matches Lean notation with the source's. Unformalised marks a source item with no Lean counterpart yet, Out of scope one left out by decision. A Correction repairs a claim false as printed; an Interpretation fixes one reading of underspecified wording. A Restatement is an equivalent form, a Strengthening implies the source's statement, and a Gap is weaker or incomparable; a node with a gap shows "Owes work". A Formalisation note is a remark that fits none of these.

Conventions shared by the statements, such as how an algebraic k-scheme is given to Lean, are in the appendix (Conventions and sources).

1.6. Where to start🔗

• New to schemes or blow-ups: the dictionary in the appendix gives the Lean name and the node of each classical notion (Dictionary), and the chapter on the blow-up states its universal property and resolves the cusp (The blow-up along an ideal sheaf); then Main Theorems II and II(N) (Theorem 4.2.1.2, Theorem 4.2.2.1), whose conditions are the classical ones.

• Resolution of a variety in its usual form: Kollár's strong resolution (Theorem 4.2.7.1), then his functorial resolution (Theorem 4.2.6.3) and what its compatibility with smooth morphisms means (Definition 4.2.4.3, Functorial resolution).

• Hironaka's paper: Main Theorems II and II(N), Corollaries 1 and 3, and Main Theorem I with its weak form, all in the chapter on the algebraic theorems; Main Theorem II″(N) opens the chapter on the analytic theorems (Theorem 4.3.1.2).

• The analytic theorems: the opening of their chapter explains the compatible families over the compact subsets of a manifold in which the manifold statements are made (Analytic manifolds and analytic spaces).

• A particular definition: the chapters on schemes and on analytic geometry are grouped by topic, the properties that a theorem asserts are stated in its section, and the chip "uses" of a theorem lists the definitions its statement depends on. The dependency graph and the summary at the end of the document are computed from the Lean declarations.