Resolution of Singularities in Characteristic Zero

4.1. Resolution of singularities in Mathlib's language🔗

Lean names in this section are shown relative to AlgebraicGeometry, TopologicalSpace, Topology, Filter, Set.

The two theorems of this section state resolution of singularities in its most familiar forms, using only Mathlib's definitions and three short ones given in full here. A reader who knows Mathlib can check that they say what they claim without learning any of the library's own definitions.

  • Every variety in characteristic zero is resolved by a single blow-up (Theorem 4.1.1.3). An integral scheme, separated and of finite type over a field of characteristic zero, has a blow-up along an ideal sheaf supported exactly on its singular locus. The result is smooth over the field, and the map is proper and an isomorphism away from the singular locus. The blow-up is given by its universal property (Definition 4.1.1.2), in terms of effective Cartier ideal sheaves (Definition 4.1.1.1), the two notions Mathlib lacks.

  • Every real-analytic function is locally a monomial after a proper change of variables (Theorem 4.1.2.2). The Jacobian determinant of the change of variables is a monomial in the same coordinates, both up to a unit (Definition 4.1.2.1). This is the form resolution takes in analysis, as in Atiyah's division of distributions.

Both follow from the main theorems of the next two sections. Those theorems are stronger and closer to their sources, but are stated in the library's own vocabulary.

4.1.1. Resolution of a variety🔗

Definition4.1.1.1source[Sta, Tag 01WR] ↗
uses 0used by 1✓L∃∀N

An ideal sheaf J on a scheme X is effective Cartier, J.IsEffectiveCartier, the ideal sheaf of an effective Cartier divisor, if near every point it is generated by a single non-zero-divisor: every point has an affine open neighbourhood U with J(U) = (g) for a non-zero-divisor g of \Gamma(X, U). Equivalently, J is an invertible sheaf (locally free of rank one), which is the Stacks project's definition of an effective Cartier divisor [TSPA, Tag 01WR]; [TSPA, Tag 01WS]. It is the library's invertible ideal sheaf (Definition 2.1.4.1), restated from Mathlib's notions alone (isEffectiveCartier_iff_isInvertible).

Lean code for Definition4.1.1.1●1 definition
Definition4.1.1.2source[Sta, Tag 0806] ↗
uses 0used by 1✓L∃∀N

A morphism \pi \colon B \to X is a blow-up of X along an ideal sheaf I, π.IsBlowUpAlong I, if the inverse image of the centre is an effective Cartier divisor (the inverse image of I on B is effective Cartier, Definition 4.1.1.1) and every f \colon Y \to X along which the inverse image of the centre is an effective Cartier divisor factors as f = \pi \circ g for a unique g \colon Y \to B [TSPA, Tag 0806]. The universal property is the definition, so a statement asking for a blow-up needs no construction of it, and a blow-up is unique up to unique isomorphism over X. It is the library's predicate IsBlowUp of the universal property (The universal property), restated from Mathlib's notions alone (isBlowUpAlong_iff_isBlowUp); the blow-up of the library (Definition 2.2.2.2) is a blow-up in this sense.

Lean code for Definition4.1.1.2●1 definition
Theorem4.1.1.3source[Hir64, Main Theorem I, p. 132] ↗
uses 1used by 0✓L∃∀N

Let k be a field of characteristic zero and X an integral scheme, separated and of finite type over k. Then there is a blow-up \pi \colon X' \to X along an ideal sheaf I whose support is exactly the singular locus of X, the complement of the smooth locus X^{ns}, with X' smooth over k. In particular \pi is proper and restricts to an isomorphism \pi^{-1}(X^{ns}) \to X^{ns}.

This is Hironaka's Main Theorem I (Theorem 4.2.8.1): X is resolved by the single blow-up with centre its singular locus. Here a blow-up is any morphism with the universal property of the blow-up along I (Definition 4.1.1.2), unique up to unique isomorphism over X. Smoothness over k stands for Hironaka's "non-singular", and the complement of the smooth locus for his singular locus; for a scheme of finite type over a field of characteristic zero the two agree [TSPA, Tag 00TV]. His "say reduced and irreducible" is the hypothesis that X is integral. The smooth locus is open and dense, so \pi is birational.

Lean code for Theorem4.1.1.3●1 theorem
Proof for Theorem 4.1.1.3
Proof uses 3
Proof dependency previews
Preview
Definition 2.1.1.1
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.

Main Theorem I (Theorem 4.2.8.1) gives an ideal sheaf D on X with support the singular locus whose blow-up \pi \colon X' \to X is regular; the library's blow-up has the universal property (Definition 4.1.1.2). The blow-up of a locally Noetherian scheme along an ideal sheaf is proper and an isomorphism over the complement of the support of D; over a perfect field the singular locus is the complement of the smooth locus, and a regular scheme locally of finite type is smooth [TSPA, Tag 00TV].

4.1.2. Local monomialization of a real-analytic function🔗

Definition4.1.2.1
uses 0used by 1✓L∃∀N

A real function g on an n-dimensional manifold M is a monomial at p up to a unit, IsMonomialAt n g p, if near p, in the coordinates y of the chart of M at p, g = u \cdot y_1^{\alpha_1} \cdots y_n^{\alpha_n} for exponents \alpha_i \ge 0 and a real-analytic function u that does not vanish at p. For n = 1 and the identity chart this is Mathlib's description of an analytic function of order \alpha_1 at p (AnalyticAt.analyticOrderAt_eq_natCast), with the coordinate not centred at p: a coordinate that does not vanish at p contributes only a unit.

Lean code for Definition4.1.2.1●1 definition
Theorem4.1.2.2source[Ati70, Resolution Theorem, p. 147] ↗
uses 1used by 0✓L∃∀N

Let f be a real-analytic function on an open set U \subseteq \mathbb{R}^n, not identically zero near any point of U. Then there is a proper real-analytic map \pi \colon M \to U from an n-dimensional real-analytic manifold M, an analytic isomorphism over the set where f does not vanish, such that near every point p of M, in the coordinates y of the chart of M at p, f \circ \pi = u \cdot y_1^{\alpha_1} \cdots y_n^{\alpha_n}, \qquad \det D(\pi \circ y^{-1})(y) = v \cdot y_1^{\beta_1} \cdots y_n^{\beta_n} with u and v analytic and nonzero at p.

This is Atiyah's Resolution Theorem over the whole of U rather than near a point, with Bierstone–Milman's monomial form of the Jacobian determinant in the same coordinates [BM97, Theorem 1.10]: the change of variables x = \pi(y) turns integrals of functions of f into integrals of functions of monomials against monomial densities. Atiyah uses it to divide distributions; Bernstein and Gelfand, independently, for the meromorphic continuation of \int |P|^\lambda \varphi [BG69]; and Watanabe for the asymptotics of Bayesian learning [Wat09, Theorem 2.3]. The manifold M is a type with Mathlib's charted-space structure modelled on \mathbb{R}^n and analytic chart changes, and the chart at p is the one that structure prefers at p.

Lean code for Theorem4.1.2.2●1 theorem
Proof for Theorem 4.1.2.2
Proof uses 13
Proof dependency previews
Preview
Definition 3.1.1.1
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.

Bierstone–Milman's principalization (Theorem 4.3.2.1) applied to the principal ideal sheaf (f) on the manifold U, which has nonzero stalks because f is not identically zero near any point, gives a proper analytic map \sigma \colon \tilde M \to U which is an analytic isomorphism off the zero set of f and along which the pull-back of (f), generated by f \circ \sigma, is a normal-crossings divisor, and so is its product with the Jacobian ideal, generated by the Jacobian determinant of \sigma. At every point of \tilde M the regular system of parameters in which the product is a monomial consists of analytic functions with independent differentials, which by the inverse function theorem are the coordinates of an analytic chart; they are primes of the stalk, a unique factorization domain, so the two factors f \circ \sigma and the Jacobian determinant are units times monomials in the same coordinates. The manifold M is \tilde M with these charts as its preferred charts.