Kollár's Theorem 35: functorial principalization

The main theorem AlgebraicGeometry.exists_functorial_principalization [Kol07, Theorem 35], with the principalization sequence Hironaka.Sequence.BP as its blow-up sequence functor on the category AlgebraicGeometry.Triple k of the triples of [Kol07, Notation 64]. Each clause is the corresponding theorem of Hironaka/Resolution/Algebraic/Kol07/Thm35/Principalization/*.lean: (1) the centres are smooth and have simple normal crossings with the total transform of E (BP_center_smooth_hasSncWith), (2) the pull-back of I is the ideal sheaf of a simple normal crossing divisor (BP_isIdealOfSncDivisor), (3) the sequence is an isomorphism over X ∖ (cosupp I ∪ Sing E) (BP_isIso_restrict), (4) it commutes with smooth surjections, with every smooth morphism up to the deletion of empty blow-ups [Kol07, 34.1] (BP_pullback_of_surjective, BP_pullback_eraseEmpty) and with change of fields [Kol07, 34.2] (BP_baseChange), and (5) it commutes with closed embeddings when E = ∅ [Kol07, 34.3] (BP_pushforward_of_closedEmbedding).

A morphism of triples h : T' ⟶ T is a k-morphism along which I and E pull back, so it carries the pull-back data Triple.IsPullbackOf of the functoriality lemmas (the over-Spec k equation is HomIsOver.comp_over), and a base change of triples is a cartesian square along which I and E pull back, Triple.IsBaseChangeOf. In clause (5) the boundary of the embedded triple Y is any family with empty index type; the value of BP does not depend on it (BP_eq_of_isEmpty), so it may be replaced by the restriction E.comap j of the boundary of the ambient triple, which is what Triple.ClosedEmbedding asks.

theorem AlgebraicGeometry.exists_functorial_principalization : ∃ (BP : (k : Type u) → [inst : Field k] → [CharZero k] → BlowUpSequenceFunctor (Triple k)), (∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k] (T : Triple k), T.IsPrincipalizedBy (BP k T)) ∧ (∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k], CommutesWithSmoothMorphisms (BP k)) ∧ CommutesWithChangeOfFields BP ∧ ∀ (k : Type u) [inst : Field k] [inst_1 : CharZero k], CommutesWithClosedEmbeddingsOfEmptyBoundary (BP k)

Kollár's functorial principalization [Kol07, Theorem 35]. There is a family BP of blow-up sequence functors on triples (BlowUpSequenceFunctor (Triple k)), one for each field k of characteristic zero, such that

• every value BP(X, I, E), with composite Π : X_r → X, is a principalization of the triple (Triple.IsPrincipalizedBy): (1) every centre is smooth over k and has simple normal crossings with the total transform of E at its stage; (2) Π^* I is the ideal sheaf of a simple normal crossing divisor; (3) Π is an isomorphism over X ∖ (cosupp I ∪ Sing E);
• (4) BP commutes with smooth morphisms [Kol07, 34.1] (CommutesWithSmoothMorphisms) and with change of fields [Kol07, 34.2] (CommutesWithChangeOfFields);
• (5) BP commutes with closed embeddings when the boundary is empty [Kol07, 34.3] (CommutesWithClosedEmbeddingsOfEmptyBoundary).

A triple (Triple, [Kol07, Notation 64]) is a smooth, equidimensional algebraic k-scheme X with an ideal sheaf I nonzero at every point and a simple normal crossing divisor family E.

Relation to the source.

• Translation. S.pullback h is Kollár's pull-back $h^* S$ [Kol07, 30.1], (S.pullback h).eraseEmpty the same with the blow-ups with empty centre deleted [Kol07, 32], and S.pushforward j the push-forward $j_* S$ along a closed embedding [Kol07, 30.3]; T.I.comap S.composite is $\Pi^* I$, and T.E.singularLocus is $\operatorname{Sing} E$, the set of points on at least two components of $E$.
• Correction. Clause (3) is stated over $X \setminus (\operatorname{cosupp} I \cup \operatorname{Sing} E)$ (Triple.IsPrincipalizedBy): $\Pi$ is an isomorphism away from the cosupport of $I$ and from the points on at least two components of $E$. Kollár prints $X \setminus \operatorname{cosupp} I$, but his functor first blows up the intersections of the components of $E$ [Kol07, 72], which need not lie in $\operatorname{cosupp} I$; the two loci agree when $E = \emptyset$.
• Correction. The order reduction $BMO_1$ of [Kol07, Theorem 107] that the proof runs splits a marked ideal as $I = M(I) \cdot N(I)$ with the monomial part $M(I) = \prod_D \mathcal{I}_D^{\operatorname{ord}_D I}$ taking one exponent per irreducible component $D$ of the boundary members (Hironaka.BMO.monomialPart; the split of [Wlo05, Section 3, Step 2]). Kollár's construction [Kol07, 111] takes one exponent per member, the minimum of $\operatorname{ord}_D I$ over the member's components; that split does not commute with open immersions, so clause (2) of [Kol07, Theorem 107] fails for it: on $\mathbb{A}^2$ with $E^1 = V(x(x-1))$, $E^2 = V(y(y-1))$ and $I = (xy)$ both exponents are $0$, and both are $1$ on the open set $x \ne 1$, $y \ne 1$. The fine split commutes with smooth pull-back, since orders at generic points are preserved.
• Gap. The inputs are the triples $(X, I, E)$ of [Kol07, Notation 64] (Triple), under which Kollár proves the theorem: their ambient scheme $X$ is smooth and equidimensional, whereas Theorem 35 as printed does not ask $X$ to be equidimensional. The base change of a triple along a field extension is again a triple.
• Gap. Kollár's $E$ is an unordered simple normal crossing divisor. Here it is an ordered family (DivisorFamily), and clause (4) compares values on families with the induced orders; nothing relates the values at two orderings of one divisor.

Source statement: [Kol07, Theorem 35]