Kollár's Theorems 36 and 27: functorial and strong resolution #

The functorial resolution theorem (AlgebraicGeometry.exists_functorial_resolution, at the end of this file) is stated on the category AlgebraicGeometry.ReducedEquidimensionalScheme k (Hironaka.Scheme.Resolution.Defs), the full subcategory of the algebraic k-schemes X with X.left.IsReducedEquidimensional k: the reduced algebraic k-schemes whose smooth locus over k has one relative dimension — Kollár's standing convention that his schemes are equidimensional [Kol07, Notation 64], as a hypothesis; the irreducible components may meet. The proof works on the underlying schemes of the inputs, the membership being X.property: clauses (1)–(3) are Hironaka.Resolution.Algebraic.Kol07.Thm36.Theorem36Assembly, the change of fields (4b) is Hironaka.Resolution.Algebraic.Kol07.Thm36.BaseChangeAffine, and the two statements of the smooth-morphism clause (4a) [Kol07, 34.1] are derived here: a smooth k-morphism h : Y ⟶ X between class members has the constant relative dimension dY - dX (smoothOfRelativeDimension_sub_of_smoothLocus, Hironaka.Resolution.Algebraic.Kol07.Thm36.RelativeDimensionConstancy), and at that dimension the versions of (4a) taking the relative dimension as an input (BR_eq_eraseEmpty_pullback_of_smooth, BRAffine_eq_eraseEmpty_pullback_of_smooth) give BR_pullback_smooth_of_class and BRAffine_pullback_smooth_of_class: for surjective h the resolution of Y is the pullback of the resolution of X, and in general it is the pullback with its empty blow-ups deleted.

Kollár's strong resolution [Kol07, Theorem 27] (AlgebraicGeometry.exists_strong_resolution) follows, at the end of the file, by applying the functorial resolution to an integral algebraic k-scheme, a class member (isReducedEquidimensional_of_isIntegral); so does Hironaka's Main Theorem I (Hironaka.Resolution.Algebraic.Hir64.MainTheoremI).

source

(Function.Surjective ⇑h → (BRFunctor k).seq Y = ((BRFunctor k).seq X).pullback h) ∧ (BRFunctor k).seq Y = (((BRFunctor k).seq X).pullback h).eraseEmpty

Clause (4a) of [Kol07, Theorem 36], the smooth morphisms [Kol07, 34.1], on the class: for a smooth k-morphism h : Y ⟶ X between class members, the resolution of Y is the pullback of the resolution of X when h is surjective, and in general the pullback with its empty blow-ups deleted. The relative dimension of h is dY - dX (smoothOfRelativeDimension_sub_of_smoothLocus, from the second conjuncts of the two class hypotheses); the two statements are BR_eq_pullback_of_smooth_surjective and BR_eq_eraseEmpty_pullback_of_smooth at that dimension.

source

theorem Hironaka.Resolution.BRAffine_pullback_smooth_of_class {k : Type u} [Field k] [CharZero k] (X : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsAffine X] (hX : AlgebraicGeometry.Scheme.IsReducedEquidimensional k X) (Y : AlgebraicGeometry.Scheme) [Y.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.LocallyOfFiniteType (Y ↘ AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsAffine Y] (hY : AlgebraicGeometry.Scheme.IsReducedEquidimensional k Y) (h : Y ⟶ X) [AlgebraicGeometry.Scheme.Hom.IsOver h (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.Smooth h] :

(Function.Surjective ⇑h → BRAffine k Y = (BRAffine k X).pullback h) ∧ BRAffine k Y = ((BRAffine k X).pullback h).eraseEmpty

Clause (4a) [Kol07, 34.1] for the affine construction BRAffine on the class. The relative dimension of h is dY - dX (smoothOfRelativeDimension_sub_of_smoothLocus); the second statement is BRAffine_eq_eraseEmpty_pullback_of_smooth at that dimension with admissible embeddings of X and Y (exists_admissibleEmbedding), and the first follows for surjective h (eraseEmpty_pullback_of_flat_surjective, eraseEmpty_BRAffine).

source

theorem AlgebraicGeometry.exists_functorial_resolution :

∃ (BR : (k : Type u) → [inst : Field k] → [CharZero k] → BlowUpSequenceFunctor (ReducedEquidimensionalScheme k)), (∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k] (X : ReducedEquidimensionalScheme k), (BR k X).IsStrongResolution) ∧ (∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k], CommutesWithSmoothMorphisms (BR k)) ∧ CommutesWithChangeOfFields BR

Kollár's functorial resolution [Kol07, Theorem 36]. There is a family BR of blow-up sequence functors on reduced equidimensional algebraic k-schemes (BlowUpSequenceFunctor (ReducedEquidimensionalScheme k)), one for each field k of characteristic zero, such that

every value BR(X), with composite Π : X_r → X, is a strong resolution of X [Kol07, (3)] (BlowUpSequence.IsStrongResolution): Π is projective and birational, and (1) X_r is smooth over k; (2) Π is an isomorphism over the smooth locus X^{ns}; (3) Π⁻¹(Sing X) is the support of a simple normal crossing divisor;
(4) BR commutes with smooth morphisms [Kol07, 34.1] (CommutesWithSmoothMorphisms) and with change of fields [Kol07, 34.2] (CommutesWithChangeOfFields).

A smooth equidimensional scheme is an input, and Π may then be the identity. The irreducible components of an input may meet: the two axes xy = 0 in the plane are an input.

Relation to the source.

Translation. (X.left ↘ Spec (.of k)).smoothLocus, Mathlib's smoothLocus of the structure morphism, is Kollár's $X^{ns}$, and its complement is $\operatorname{Sing} X$; over a field of characteristic zero it is the set of points with regular local ring (Scheme.mem_smoothLocus_iff_isRegularAt).
Interpretation. Kollár's clause (3), "$\Pi^{-1}(\operatorname{Sing} X)$ is a divisor with simple normal crossings", is read with the reduced structure on $\Pi^{-1}(\operatorname{Sing} X)$: it is IsSncDivisor of that set of points.
Gap. Kollár states the theorem for all schemes of finite type over k. The inputs here (ReducedEquidimensionalScheme) are the reduced, equidimensional ones (Scheme.IsReducedEquidimensional), whose irreducible components may meet; the non-reduced schemes and the schemes with components of different dimensions are excluded, and (4) is asserted only between inputs. Kollár proves the theorem by feeding triples in the sense of [Kol07, Notation 64] (smooth equidimensional ambient schemes) to Theorem 35, and the construction here needs both restrictions: for a non-reduced X the strict transform at which the run is truncated need not be reduced; for components of different dimensions (4) fails. For X the cuspidal curve y² = x³, Y = X ⊔ (X × 𝔸¹) and the smooth surjection h = 𝟙 ⊔ pr₁, the run on an embedding of Y first blows up only the cusp line of the second piece, where the order is 2, whereas h^* BR(X) first blows up the preimage of the cusp point, which contains the cusp point of the first piece. Kollár's remark that 34.1 is a local property is where a proof for mixed dimensions would be needed; none is printed.
Restatement. Kollár's clauses (1)–(3) for the blow-up sequence $BR(X)$ are stated as IsStrongResolution, which also asks that $\Pi$ be projective and birational: a strong resolution in the sense of [Kol07, (3)], as the sentence introducing the theorem says ("we obtain strong and functorial resolution"). Both follow from the other clauses: the composite of a succession of blow-ups of a Noetherian scheme is projective, and by (2) $\Pi$ is an isomorphism over the smooth locus, which is dense.
Formalisation note. The class of inputs is stable under change of fields and under étale k-morphisms, so (4) covers the base change of every input along every field extension and every étale morphism to an input: over a field of characteristic zero a reduced scheme of finite type is geometrically reduced [TSPA, Tag 020I], smoothness is stable under base change [TSPA, Tag 01VB] and fpqc local on the base [TSPA, Tag 02VL], an étale morphism has reduced source when its target is reduced [TSPA, Tag 033B], and smoothness descends along smooth surjections [TSPA, Tag 02K5]. These stability facts are not formalized: applying (4) to a given base change requires showing that it is an input.

Source statement: [Kol07, Theorem 36]

source

theorem AlgebraicGeometry.exists_strong_resolution {k : Type u} [Field k] [CharZero k] (X : AlgScheme k) [IsIntegral X.left] :

∃ (S : X.left.BlowUpSequence), S.IsStrongResolution

Kollár's strong resolution of singularities [Kol07, Theorem 27]. Let X be a variety (an integral algebraic k-scheme) over a field k of characteristic zero. Then there is a birational and projective morphism Π : X' → X, the composite S.composite of a succession of blow-ups S of X, that is a strong resolution of X (BlowUpSequence.IsStrongResolution): (1) X' is smooth over k; (2) Π is an isomorphism over the smooth locus X^{ns}; (3) Π⁻¹(Sing X) is the support of a simple normal crossing divisor. Projectivity and birationality are part of BlowUpSequence.IsResolution; birationality is the isomorphism over a dense open subset of X, here the smooth locus.

This is resolution of singularities in its usual form: a smooth X' with a projective birational morphism to X, here a succession of blow-ups. Kollár's weaker form [Kol07, Corollary 22], a smooth X' with a birational projective morphism to X and no conditions (2) and (3), is the part BlowUpSequence.IsResolution of the conclusion.

Relation to the source.

Translation. Kollár's variety is an integral algebraic k-scheme, X : AlgScheme k with [IsIntegral X.left].
Translation. Kollár's "birational and projective morphism" is the projectivity (IsProjective, [TSPA, Tag 01W8]) and the birationality of BlowUpSequence.IsResolution.
Interpretation. Kollár's clause (3), "$\Pi^{-1}(\operatorname{Sing} X)$ is a divisor with simple normal crossing", is read with the reduced structure on $\Pi^{-1}(\operatorname{Sing} X)$, as in Theorem 36 (AlgebraicGeometry.exists_functorial_resolution).
Strengthening. Kollár assumes X quasi-projective, which his proof uses to embed X in a projective space; no such hypothesis is made here.
Strengthening. Here $\Pi$ (S.composite) is in addition the composite of a succession of blow-ups of X, whose centres are not asserted to be smooth; Theorem 27 as printed does not say this. It matches Kollár's construction: his $R(X)$ is the birational transform of $X$ that is a centre $Z_j$ of a succession of smooth blow-ups of an ambient smooth $P$, and by restriction [Kol07, 30.2] his $\Pi$ is the composite of the blow-ups of the birational transforms of $X$ along their intersections with the earlier centres, which may be singular [Kol07, Warning 23].

Source statement: [Kol07, Theorem 27]