The clauses of the analytic main theorems on a finite succession of monoidal transformations #

The clauses of Hironaka's Main Theorem II′(N) [Hir64, p. 156] on a finite succession of monoidal transformations U_0 ← U_1 ← ⋯ ← U_r of an analytic manifold (FiniteSuccession), in which the analytic principalization theorems state their conclusions over each compact set. They carry the names of the clauses of the algebraic Main Theorems II and II(N) and Corollary 1 on blow-up sequences of schemes, whose bodies they repeat with the manifold leaf predicates. One leaf predicate says more than its scheme namesake: the manifold IdealSheaf.IsSncBoundaryWith B D asserts simple normal crossings of B at every point and with D at the points of D, while the scheme IsSncBoundaryWith asserts the condition at the points of D only. So the first field of HasSncBoundaries here also asserts simple normal crossings of every intermediate boundary.

FiniteSuccession.HasSncBoundaries S B: the boundaries E_i (S.boundarySeq B), started at E_0 = B and continued by E_{i+1} = red(σ_{i+1}⁻¹(E_i) ∪ σ_{i+1}⁻¹(D_i)), have simple normal crossings with the centres, and the last one has simple normal crossings ([Hir64, Main Theorem II′(N) (iii) and the first half of (iv)]; [Wlo09, Theorem 2.0.3 (2)]).
FiniteSuccession.HasConstantPositiveOrderAlongCenters S J: the order of the weak transform of J is a positive constant along every centre ([Hir64, Main Theorem II′(N) (ii)]).

The clauses of Włodarczyk's locally finite embedded desingularization [Wlo09, Theorem 2.0.2] on the succession over each compact set are collected in one structure, named after the structure EmbeddedPair.IsDesingularizedBy of the algebraic embedded desingularization on blow-up sequences of schemes (the fields are named after the analytic notions they state):

IdealSheaf.IsDesingularizedBy I S: the closed subspace with ideal sheaf I is desingularized by S ([Wlo09, Theorem 2.0.2 (1)–(3), (6)]);
IdealSheaf.IsLocallyFinitelyDesingularizedBy I F: the family F is a locally finite embedded desingularization of the closed subspace with ideal sheaf I ([Wlo09, Theorem 2.0.2]: the map res_{Y,M} proper and an isomorphism off the singular locus, the succession over every compact desingularizing the subspace with no empty centre and every centre of codimension at least two or in the exceptional divisor, and an exceptional divisor and a strict transform on the whole space).

The clauses of Włodarczyk's locally finite principalization [Wlo09, Theorem 2.0.3], whose value is a compatible family of finite successions over the compact sets (ExtensionCompatibleFamily), are collected in a structure on the family, named after Włodarczyk's term:

IdealSheaf.IsLocallyFinitelyPrincipalizedBy I F: the family F is a locally finite principalization of the ideal sheaf I ([Wlo09, Theorem 2.0.3 (1)–(3)], with the properness of prin_I).

The functorial theorems assert the existence of an assignment of a compatible family to every input, with a property of each value and a functoriality package, as the algebraic functorial theorems assert a blow-up sequence functor (BlowUpSequenceFunctor); they differ in the inputs.

IdealSheafPair 𝕜: the pairs (M, I) of an analytic manifold M over 𝕜 on a finite-dimensional model space and an ideal sheaf I with nonzero stalks, the inputs of the principalization (Kollár's triples with an empty boundary); IdealSheafPair.pullback is the pair (N, g^*I) over a local analytic isomorphism g : N → M.
HasUnderlyingManifold C 𝕜: a type C of inputs each with an underlying manifold on a finite-dimensional model space; CompatibleFamilyAssignment C: a compatible family for every input.
IdealSheaf.IsPushforwardAlong I J τ: the ideal sheaf I on M is the push-forward of the ideal sheaf J on N along the closed embedding of analytic manifolds τ : N → M (an analytic embedding, Mathlib's IsSmoothEmbedding at ω, with closed image): I contains the ideal of τ(N) and J = τ^*I (Kollár's 𝒪_X/I_X = j_*(𝒪_Y/I_Y) [Kol07, 34.3]).
IdealSheafPair.CommutesWithLocalAnalyticIsomorphisms P: the last sentence of [Wlo09, Theorem 2.0.3] for local analytic isomorphisms, in its two forms — over every pair of compact sets, as the relation between two successions of [Wlo09, Theorem 3.5.1 (2)], and globally, as the lift of g : N → M to a unique map g̃ : Ñ → M̃ over g, a local analytic isomorphism identifying Ñ with the fibre product N ×_M M̃ (the "natural lifting" of [Wlo09, Theorem 2.0.1 (3)]).
IdealSheafPair.CommutesWithClosedEmbeddings P: the rest of that sentence, "embeddings of ambient varieties", read as [Kol07, Theorem 35 (5)] and [Kol07, 34.3], over every pair of compact sets.
EmbeddedPair 𝕜: the pairs (M, Y) of an analytic manifold on a finite-dimensional model space and a reduced closed analytic subspace, the inputs of the embedded desingularization (the analogue of the algebraic EmbeddedPair); EmbeddedPair.pullback is the pair (N, g^{-1}(Y)) over a local analytic isomorphism g : N → M.
EmbeddedPair.CommutesWithLocalAnalyticIsomorphisms R and EmbeddedPair.CommutesWithClosedEmbeddings R: the two halves of [Wlo09, Theorem 2.0.2 (4)], over every pair of compact sets, the second with Kollár's hypothesis that no component of the submanifold lies in the subspace.

The clauses of the analytic main theorems on a finite succession of monoidal transformations #

The inputs of the functorial theorems #

The functoriality of an assignment on pairs #

Embedded pairs #

The functoriality of an assignment on embedded pairs #