Compatible families of finite successions over the compact subsets #

Włodarczyk's compatible-family form of principalization Wlo09, Theorem 2.0.3; Definition 3.2.6; Theorem 3.5.1 (2), the form in which Hironaka's Main Theorem II''(N) and the real-analytic principalization theorem are stated: a proper analytic map M̃ → M which over an open neighbourhood of every compact set is a finite composite of blow-ups with smooth centres, compatibly across compacts. Włodarczyk's principalization is "locally but not globally a sequence of blow-ups at smooth centers" [Wlo09, Introduction]: over a neighbourhood U of a compact set Z the morphism splits into a finite sequence of blow-ups U = U_0 ← U_1 ← ⋯ ← U_r with smooth centres C_{i-1} ⊆ U_{i-1}, and for Z_1 ⊆ Z_2 with U_1 ⊆ U_2 the restriction of the sequence over U_2 to U_1 "determines" the sequence over U_1 — it is an extension of it in the sense of [Wlo09, Definition 3.2.6]: the same blow-ups with isomorphisms (blow-ups with empty centre) interspersed.

FiniteSuccession.restrict S h: the restriction of a succession over U_2 to an open U_1 ≤ U_2 (stages the preimages of U_1, centres and maps restricted; a blow-up restricted to an open subset is the blow-up of the restricted centre), and FiniteSuccession.IsExtensionOf T S, Włodarczyk's "T is an extension of S".
FiniteSuccession.Hom R S φ: a morphism of successions over φ : N → M, an index map from the stages of S to those of R with maps between the stages over φ, compatible with the blow-downs; the two relations below are such morphisms with conditions on the maps and centres.
FiniteSuccession.IsPullbackUpToEmptyAlong R S g: for a local analytic isomorphism g : N → M, the succession R over an open of N is the pull-back of the succession S over an open of M along g, up to blow-ups with empty centre — the induced sequence g^*(S) is an extension of R, the form of [Wlo09, Theorem 3.5.1 (2)] in which the commutation of principalization with local analytic isomorphisms is stated.
FiniteSuccession.IsPushforwardUpToEmptyAlong S R τ: for a closed embedding τ : N → M, the succession S over an open U of M is the push-forward along τ of the succession R over an open U' of N with τ(U') ⊆ U, up to blow-ups whose centres lie outside the part over τ(U') — Kollár's j_* B [Kol07, Definition 30.3], the form in which the commutation of principalization with closed embeddings [Kol07, 34.3] is stated over the compact sets.
ExtensionCompatibleFamily M: Włodarczyk's data in [Wlo09, Theorem 2.0.3 (1), (4)] — a manifold space = M̃ with an analytic map map : M̃ → M; for every compact K ⊆ M (Mathlib's Compacts M) an open neighbourhood nhd K ⊇ K, monotone in K, and a finite succession seq K over nhd K whose end result is identified with map⁻¹(nhd K) over nhd K (toSpace, map_toSpace, toSpace_isIso); and the compatibility isExtensionOf_restrict: for K_1 ⊆ K_2 the restriction of seq K_2 to nhd K_1 is an extension of seq K_1. The properness of map is a clause of the main theorems, not of the structure.
ExtensionCompatibleFamily.IsPullbackAlong F' F g and ExtensionCompatibleFamily.IsPushforwardAlong F F' τ: the two relations between successions, over every pair of compacts K' ⊆ N, K ⊆ M whose neighbourhoods correspond under the map.

Compatible families of finite successions over the compact subsets #

The restriction of a finite succession to an open subset #

Włodarczyk's extension relation #

Compatible families of finite successions over the compact subsets #