Włodarczyk's functorial locally finite principalization

Włodarczyk's locally finite principalization of an ideal sheaf on an analytic manifold over 𝕜 = ℝ or ℂ together with its commutation with local analytic isomorphisms and with closed embeddings [Wlo09, Theorem 2.0.3], the analytic counterpart of Kollár's functorial principalization [Kol07, Theorem 35] for an empty boundary: the main theorem AnalyticManifold.exists_functorial_principalization at the end of this file.

On the standard model 𝕜ⁿ the value at an ideal sheaf I with nonzero stalks is Kollár's order reduction of the marked ideal (M, I, ∅, 1) [Kol07, 72], the marked family concreteBMOanFam of the concrete tower at the mark 1, glued along the exhaustion of M (principalizationExt):

• isLocallyFinitelyPrincipalizedBy_principalizationExt: the clauses of IdealSheaf.IsLocallyFinitelyPrincipalizedBy. Over every compact the value is a smooth blow-up sequence of order ≥ 1 for (I, ∅) whose marked transform has order < 1 at the end (BMOanFam.isOfOrderGe, BMOanFam.ord_lt): the centres have normal crossings with the exceptional divisors, which are simple normal crossings families (isSnc_totalTransformSeqFrom_and_boundarySeq_eq_of_forall_lt), the total transform of I is Kollár's monomial in the final exceptional divisor (exists_boundaryMonomial_of_isOfOrderGe_one, [Kol07, 72]), and the centres lie over the support of I (CentersOver.of_isOfOrderGe); properness, the divisor clause on M̃ and the isomorphism off the support are those of the gluing;
• isPullbackUpToEmptyAlong_principalizationExt: for a local analytic isomorphism g : N → M the triple (N, g^*I, ∅) carries the pull-back data of (M, I, ∅), so the values of the marked family correspond (BMOanFam.commutesWithLocalIsos, [Kol07, Theorem 107 (2)]) and the succession over a compact of N is the pull-back up to empty blow-ups of the succession over every compact of M whose neighbourhood contains its image (CompatibleFamily.isPullbackUpToEmptyAlong_seqOn);
• isPushforwardUpToEmptyAlong_principalizationExt: for a closed embedding τ : N → M with image a closed submanifold S of codimension s and I ⊇ I_S, the value at (M, I, ∅) is over every relatively compact open the push-forward of the value at (S, I|_S, ∅) in dimension n − s (concreteBMOanFam_commutesWithClosedEmbeddings, Kollár's Claim 71.2 from [Kol07, Theorem 107 (3)] and [Kol07, Theorem 103 (3)]), so the succession over a compact of M is the push-forward along τ of the succession over every compact of N whose neighbourhood maps into its neighbourhood, up to blow-ups whose centres lie away from the image (isPushforwardUpToEmptyAlong_toExtensionCompatibleFamily, Hironaka/Resolution/Analytic/Wlo09/FamilyPushforward.lean).

On an arbitrary model E the assignment principalizationAssignment 𝕜 E reads the value on the re-modelled manifold back along E ≃ 𝕜ⁿ (ExtensionCompatibleFamily.transportBack), with the clauses (isLocallyFinitelyPrincipalizedBy_transportBack), the pull-back relation along the re-modelled local isomorphism (IsPullbackUpToEmptyAlong.transportAlong, Hironaka/Resolution/Analytic/ModelTransport/Principalization.lean) and the push-forward relation along the re-modelled closed embedding (IsPushforwardUpToEmptyAlong.transportAlong, Hironaka/Resolution/Analytic/ModelTransport/Pushforward.lean; the embedding identifies N with the bundled submanifold τ(N) by IsClosedAnalyticEmbedding.toDiffeomorph, which fixes the dimension of N, dim_eq_of_diffeomorph).

The global lift of a local analytic isomorphism g : N → M to g̃ : Ñ → M̃ (liftsLocalAnalyticIsomorphisms_principalizationAssignment) is glued from the per-compact relation and the compact closures of the neighbourhoods (liftsLocalAnalyticIsomorphisms_of_commutes, Hironaka/Resolution/Analytic/Wlo09/FamilyLift.lean).

The principalization on the standard model

def Hironaka.Manifold.emptyBoundaryTriple {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (I : M.IdealSheaf) (hI : Manifold.IdealSheaf.IsNonzeroEverywhere I) : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) M

The triple (M, I, ∅) of an ideal sheaf with nonzero stalks and the empty boundary family, the input of the marked order reduction for Włodarczyk's principalization of I.

Equations

• Hironaka.Manifold.emptyBoundaryTriple I hI = { I := I, isNonzeroEverywhere := hI, F := Manifold.HypersurfaceFamily.empty M.carrier, isSnc := ⋯ }

theorem Hironaka.Manifold.bmoClass_emptyBoundaryTriple {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {M : AnalyticManifold 𝕜 (Fin n → 𝕜)} (I : M.IdealSheaf) (hI : Manifold.IdealSheaf.IsNonzeroEverywhere I) : Manifold.AnalyticTriple.BMOClass 1 (emptyBoundaryTriple I hI)

The triple (M, I, ∅) lies in the marked class at the mark 1: the mark is positive and no boundary member is nonempty.

noncomputable def Hironaka.Manifold.bmoPrincipalizationFam {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : Manifold.IdealSheaf.IsNonzeroEverywhere I) : CompatibleFamily (emptyBoundaryTriple I hI)

The principalization of I on the standard model over the relatively compact opens: Kollár's order reduction of the marked ideal (M, I, ∅, 1) [Kol07, 72], the value of the marked family concreteBMOanFam of the concrete tower at the mark 1.

Equations

• Hironaka.Manifold.bmoPrincipalizationFam M I hI = (Hironaka.concreteBMOanFam 𝕜 n).functor.fam (Hironaka.Manifold.emptyBoundaryTriple I hI) ⋯

noncomputable def Hironaka.Manifold.principalizationExt {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : Manifold.IdealSheaf.IsNonzeroEverywhere I) : M.ExtensionCompatibleFamily

The principalization of I on the standard model: the order reduction of (M, I, ∅, 1) glued along the exhaustion of M (CompatibleFamily.toExtensionCompatibleFamily).

Equations

• Hironaka.Manifold.principalizationExt M I hI = (Hironaka.Manifold.bmoPrincipalizationFam M I hI).toExtensionCompatibleFamily

theorem Hironaka.Manifold.restrictTriple_emptyBoundaryTriple_F_idealSheaf {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : Manifold.IdealSheaf.IsNonzeroEverywhere I) (U : TopologicalSpace.Opens M.carrier) : (restrictTriple (emptyBoundaryTriple I hI) U).F.idealSheaf = ⊤

The boundary ideal sheaf of (M, I, ∅) restricted to an open is the unit ideal.

theorem Hironaka.Manifold.isLocallyFinitelyPrincipalizedBy_principalizationExt {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : Manifold.IdealSheaf.IsNonzeroEverywhere I) : I.IsLocallyFinitelyPrincipalizedBy (principalizationExt M I hI)

The principalization on the standard model is a locally finite principalization of I (IdealSheaf.IsLocallyFinitelyPrincipalizedBy, [Wlo09, Theorem 2.0.3 (1)–(3)]): properness, the isomorphism off the support and the divisor clause on M̃ are those of the glued family; the neighbourhoods are pieces of the exhaustion; over every compact the value is a smooth blow-up sequence of order ≥ 1 for (I, ∅) whose marked transform has order < 1 at the end (BMOanFam.isOfOrderGe, BMOanFam.ord_lt), so its exceptional divisors are simple normal crossings families having simple normal crossings with the centres (isSnc_totalTransformSeqFrom_and_boundarySeq_eq_of_forall_lt, hasSncWith_totalTransformSeqFrom_center_of_forall_lt), the total transform of I is Kollár's monomial in the final exceptional divisor (exists_boundaryMonomial_of_isOfOrderGe_one, [Kol07, 72]), and the centres lie over the support of I (CentersOver.of_isOfOrderGe).

theorem Hironaka.Manifold.isPullbackUpToEmptyAlong_principalizationExt {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : Manifold.IdealSheaf.IsNonzeroEverywhere I) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (g : AnalyticMap N M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑g) (J : N.IdealSheaf) (hJ : Manifold.IdealSheaf.IsNonzeroEverywhere J) (hIJ : J = Manifold.IdealSheaf.pullback ⇑g ⋯ I) (K' : TopologicalSpace.Compacts N.carrier) (K : TopologicalSpace.Compacts M.carrier) (hK : ⇑g '' ↑((principalizationExt N J hJ).nhd K') ⊆ ↑((principalizationExt M I hI).nhd K)) : ((principalizationExt N J hJ).seq K').IsPullbackUpToEmptyAlong ((principalizationExt M I hI).seq K) g

The principalization on the standard model commutes with local analytic isomorphisms, over every pair of compacts ([Wlo09, Theorem 3.5.1 (2)]): for a local analytic isomorphism g : N → M and J = g^* I, the succession over U_{K'} is the pull-back along g of the succession over U_K up to empty blow-ups whenever g(U_{K'}) ⊆ U_K. The triple (N, J, ∅) carries the pull-back data of (M, I, ∅), so the marked family commutes with g (BMOanFam.commutesWithLocalIsos), and CompatibleFamily.isPullbackUpToEmptyAlong_seqOn reads the pull-back predicate.

theorem Hironaka.Manifold.isPushforwardUpToEmptyAlong_principalizationExt {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : Manifold.IdealSheaf.IsNonzeroEverywhere I) {s : ℕ} {N : AnalyticManifold 𝕜 (Fin (n - s) → 𝕜)} (τ : ContMDiffMap (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) N.carrier M.carrier ⊤) (hS : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (Set.range ⇑τ) s) (e : Diffeomorph (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) N.carrier hS.toAnalyticManifold.carrier ⊤) (he : ∀ (x : N.carrier), ↑(e x) = τ x) (hle : ∀ (x : ↑↧M.carrier), hS.idealSheaf.stalkIdeal x ≤ Manifold.IdealSheaf.stalkIdeal I x) (J : N.IdealSheaf) (hJ : Manifold.IdealSheaf.IsNonzeroEverywhere J) (hJI : J = Manifold.IdealSheaf.pullback ⇑τ ⋯ I) (K' : TopologicalSpace.Compacts N.carrier) (K : TopologicalSpace.Compacts M.carrier) (hK : ⇑τ '' ↑((principalizationExt N J hJ).nhd K') ⊆ ↑((principalizationExt M I hI).nhd K)) : ((principalizationExt M I hI).seq K).IsPushforwardUpToEmptyAlong ((principalizationExt N J hJ).seq K') τ

The principalization on the standard model commutes with closed embeddings, over every pair of compacts ([Kol07, 34.3]): for a closed embedding τ : N → M identified by e with the bundled closed submanifold S = τ(N) of codimension s, I ⊇ I_S and J = τ^*I, the succession over U_K is the push-forward along τ of the succession over U_{K'}, up to blow-ups whose centres lie away from τ(U_{K'}), whenever τ(U_{K'}) ⊆ U_K. The marked family of the concrete tower commutes with closed embeddings of empty divisor over the relatively compact opens (concreteBMOanFam_commutesWithClosedEmbeddings, Kollár's Claim 71.2), and isPushforwardUpToEmptyAlong_toExtensionCompatibleFamily reads the push-forward predicate for the glued families.

theorem Hironaka.Manifold.isPushforwardUpToEmptyAlong_principalizationExt_of_diffeomorph {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : Manifold.IdealSheaf.IsNonzeroEverywhere I) {m s : ℕ} {N : AnalyticManifold 𝕜 (Fin m → 𝕜)} [Nonempty N.carrier] (τ : ContMDiffMap (modelWithCornersSelf 𝕜 (Fin m → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) N.carrier M.carrier ⊤) (hS : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (Set.range ⇑τ) s) (e : Diffeomorph (modelWithCornersSelf 𝕜 (Fin m → 𝕜)) (modelWithCornersSelf 𝕜 (Fin (n - s) → 𝕜)) N.carrier hS.toAnalyticManifold.carrier ⊤) (he : ∀ (x : N.carrier), ↑(e x) = τ x) (hle : ∀ (x : ↑↧M.carrier), hS.idealSheaf.stalkIdeal x ≤ Manifold.IdealSheaf.stalkIdeal I x) (J : N.IdealSheaf) (hJ : Manifold.IdealSheaf.IsNonzeroEverywhere J) (hJI : J = Manifold.IdealSheaf.pullback ⇑τ ⋯ I) (K' : TopologicalSpace.Compacts N.carrier) (K : TopologicalSpace.Compacts M.carrier) (hK : ⇑τ '' ↑((principalizationExt N J hJ).nhd K') ⊆ ↑((principalizationExt M I hI).nhd K)) : ((principalizationExt M I hI).seq K).IsPushforwardUpToEmptyAlong ((principalizationExt N J hJ).seq K') τ

isPushforwardUpToEmptyAlong_principalizationExt for a nonempty N modelled on any 𝕜^m: the identification e of N with the bundled submanifold of codimension s forces m = n − s (dim_eq_of_diffeomorph).

theorem Hironaka.Manifold.isPushforwardUpToEmptyAlong_principalizationExt_of_isEmpty {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (M : AnalyticManifold 𝕜 (Fin n → 𝕜)) (I : M.IdealSheaf) (hI : Manifold.IdealSheaf.IsNonzeroEverywhere I) {s : ℕ} {E' : Type u_1} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [FiniteDimensional 𝕜 E'] {N : AnalyticManifold 𝕜 E'} [IsEmpty N.carrier] (τ : ContMDiffMap (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) N.carrier M.carrier ⊤) (hS : Manifold.IsClosedSubmanifold (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) (Set.range ⇑τ) s) (hle : ∀ (x : ↑↧M.carrier), hS.idealSheaf.stalkIdeal x ≤ Manifold.IdealSheaf.stalkIdeal I x) (F : N.ExtensionCompatibleFamily) (hF : ∀ (K' : TopologicalSpace.Compacts N.carrier), (F.seq K').NoEmptyCenters) (K' : TopologicalSpace.Compacts N.carrier) (K : TopologicalSpace.Compacts M.carrier) : ((principalizationExt M I hI).seq K).IsPushforwardUpToEmptyAlong (F.seq K') τ

isPushforwardUpToEmptyAlong_principalizationExt for an empty N modelled on any space: both successions are empty (isPushforwardUpToEmptyAlong_seqOn_of_isEmpty).

The assignment on an arbitrary model

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.modelEquiv (𝕜 : Type) [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] : E ≃L[𝕜] Fin (Module.finrank 𝕜 E) → 𝕜

The identification of E with its standard model 𝕜ⁿ, n = dim E.

Equations

• Hironaka.Manifold.modelEquiv 𝕜 E = ContinuousLinearEquiv.ofFinrankEq ⋯

noncomputable def Hironaka.Manifold.principalizationAssignment (𝕜 : Type) [RCLike 𝕜] : AnalyticManifold.CompatibleFamilyAssignment (AnalyticManifold.IdealSheafPair 𝕜)

Włodarczyk's principalization as an assignment on the pairs (M, I): the principalization of the re-modelled ideal sheaf on the re-modelled manifold (standard model 𝕜ⁿ, n = dim E, principalizationExt), read back on the manifold (transportBack).

Equations

• One or more equations did not get rendered due to their size.

theorem Hironaka.Manifold.isLocallyFinitelyPrincipalizedBy_principalizationAssignment {𝕜 : Type} [RCLike 𝕜] (T : AnalyticManifold.IdealSheafPair 𝕜) : T.I.IsLocallyFinitelyPrincipalizedBy (principalizationAssignment 𝕜 T)

Every value of the assignment is a locally finite principalization: the principalization on the standard model (isLocallyFinitelyPrincipalizedBy_principalizationExt) carried back (isLocallyFinitelyPrincipalizedBy_transportBack).

theorem Hironaka.Manifold.isPullbackUpToEmptyAlong_principalizationAssignment {𝕜 : Type} [RCLike 𝕜] (T : AnalyticManifold.IdealSheafPair 𝕜) {N : AnalyticManifold 𝕜 T.E} (g : AnalyticMap N T.M) (hg : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 T.E) (modelWithCornersSelf 𝕜 T.E) ⊤ ⇑g) (K' : TopologicalSpace.Compacts N.carrier) (K : TopologicalSpace.Compacts T.M.carrier) (hK : ⇑g '' ↑((principalizationAssignment 𝕜 (T.pullback g hg)).nhd K') ⊆ ↑((principalizationAssignment 𝕜 T).nhd K)) : ((principalizationAssignment 𝕜 (T.pullback g hg)).seq K').IsPullbackUpToEmptyAlong ((principalizationAssignment 𝕜 T).seq K) g

The successions of the assignment pull back along local analytic isomorphisms, over every pair of compacts: on the standard model the re-modelled map is a local analytic isomorphism along which the re-modelled ideal sheaves pull back (isLocalDiffeomorph_transport, IdealSheaf.transport_pullback), where the principalization commutes with it (isPullbackUpToEmptyAlong_principalizationExt); the pull-back predicate carries back to E (IsPullbackUpToEmptyAlong.transportAlong).

theorem Hironaka.Manifold.commutesWithLocalAnalyticIsomorphisms_principalizationAssignment {𝕜 : Type} [RCLike 𝕜] : AnalyticManifold.IdealSheafPair.CommutesWithLocalAnalyticIsomorphisms (principalizationAssignment 𝕜)

The assignment commutes with local analytic isomorphisms, over every pair of compacts and as the lift of the isomorphism: the pull-back relation (isPullbackUpToEmptyAlong_principalizationAssignment) and the compact closures of the neighbourhoods (isCompact_closure_nhd) glue the lift (IdealSheafPair.commutesWithLocalAnalyticIsomorphisms_of_isPullbackUpToEmptyAlong).

The commutation with closed embeddings across the model spaces

theorem Hironaka.Manifold.commutesWithClosedEmbeddings_principalizationAssignment {𝕜 : Type} [RCLike 𝕜] : AnalyticManifold.IdealSheafPair.CommutesWithClosedEmbeddings (principalizationAssignment 𝕜)

The assignment commutes with closed embeddings (IdealSheafPair.CommutesWithClosedEmbeddings, [Kol07, 34.3] over the compact sets): for a closed embedding of analytic manifolds τ : N → M along which I is the push-forward of J, the re-modelled map transportBetween is a closed embedding of the re-modelled manifolds with image a closed submanifold of the same codimension, along which the re-modelled ideal sheaves pull back and the containment of the ideal sheaf of the image carries over (Hironaka/Resolution/Analytic/Wlo09/ClosedEmbedding.lean). For a nonempty N the embedding identifies the re-modelled N with the bundled submanifold (IsClosedAnalyticEmbedding.toDiffeomorph), and the push-forward relation holds on the standard models (isPushforwardUpToEmptyAlong_principalizationExt_of_diffeomorph); for an empty N both successions are empty (isPushforwardUpToEmptyAlong_principalizationExt_of_isEmpty). The relation carries back to E and E' (IsPushforwardUpToEmptyAlong.transportAlong).

theorem AnalyticManifold.exists_functorial_principalization (𝕜 : Type) [RCLike 𝕜] : ∃ (P : CompatibleFamilyAssignment (IdealSheafPair 𝕜)), (∀ (T : IdealSheafPair 𝕜), T.I.IsLocallyFinitelyPrincipalizedBy (P T)) ∧ IdealSheafPair.CommutesWithLocalAnalyticIsomorphisms P ∧ IdealSheafPair.CommutesWithClosedEmbeddings P

Włodarczyk's functorial locally finite principalization [Wlo09, Theorem 2.0.3], over 𝕜 = ℝ or 𝕜 = ℂ, the analytic counterpart of Kollár's functorial principalization [Kol07, Theorem 35] for an empty boundary. There is a compatible family assignment P on the pairs (M, I) of an analytic manifold M over 𝕜, modelled on a finite-dimensional space, and an ideal sheaf I on M with nonzero stalks (CompatibleFamilyAssignment (IdealSheafPair 𝕜)) — to each pair an analytic map prin_I : M̃ → M which over an open neighbourhood U_K of every compact K ⊆ M splits, compatibly across compacts, into a finite succession of blow-ups U_K = U_0 ← U_1 ← ⋯ ← U_r with smooth centres C_i ⊆ U_i and composite σ_K : U_r → U_K — such that

• every value P(M, I) is a locally finite principalization of I (IdealSheaf.IsLocallyFinitelyPrincipalizedBy): with exceptional divisors E_i (the boundaries started at the empty boundary ⊤), prin_I is proper and every U_K has compact closure; (1) every centre C_i is smooth; (2) every E_i has simple normal crossings with C_i, and E_r has simple normal crossings (FiniteSuccession.HasSncBoundaries); (3) the total transform σ_K^*(I|_{U_K}) is, near every point, the ideal of an effective combination of the components of E_r through it (IdealSheaf.IsMulBoundaryMonomial, with the unit ideal ⊤ as its first factor), and the total transform prin_I^*(I) on M̃ is a normal-crossings divisor (IdealSheaf.IsNormalCrossingsDivisor); and prin_I is an isomorphism over the complement of the support of I (AnalyticMap.IsIsoOver);
• P commutes with local analytic isomorphisms (IdealSheafPair.CommutesWithLocalAnalyticIsomorphisms): for a local analytic isomorphism g : N → M of manifolds modelled on one space and the pair (N, g^*I) (IdealSheafPair.pullback), over every pair of compacts K' ⊆ N, K ⊆ M with g(U_{K'}) ⊆ U_K the succession of P(N, g^*I) over U_{K'} is the pull-back along g of the succession of P(M, I) over U_K, up to blow-ups with empty centre (FiniteSuccession.IsPullbackUpToEmptyAlong; [Wlo09, Theorem 3.5.1 (2)]); and there is a unique continuous map g̃ : Ñ → M̃ over g between the spaces of P(N, g^*I) and P(M, I), which is analytic, a local analytic isomorphism, and maps every fibre of prin_{g^*I} bijectively onto the fibre of prin_I over the image point, so that Ñ is the fibre product N ×_M M̃;
• P commutes with closed embeddings (IdealSheafPair.CommutesWithClosedEmbeddings): for pairs (M, I) and (N, J) and a closed embedding of analytic manifolds τ : N → M (an analytic embedding with closed image) along which I is the push-forward of J — the ideal of the closed submanifold τ(N) lies in I, and J = τ^*I (IdealSheaf.IsPushforwardAlong) — and compacts K' ⊆ N, K ⊆ M with τ(U_{K'}) ⊆ U_K, the succession of P(M, I) over U_K is the push-forward along τ of the succession of P(N, J) over U_{K'}, up to blow-ups whose centres lie outside the part over τ(U_{K'}) (FiniteSuccession.IsPushforwardUpToEmptyAlong; [Kol07, 34.3]).

Włodarczyk's (4), that the factorization over a larger compact restricts to the factorization over a smaller one, is the compatibility of the family: the succession over K ⊆ K', restricted to U_K, is an extension of the succession over K, the same blow-ups with isomorphisms interspersed (ExtensionCompatibleFamily.isExtensionOf_restrict; [Wlo09, Definition 3.2.6]). Centres of codimension one are admitted, as in [Wlo09, Remark (1) after Theorem 2.0.3]: the blow-up of such a centre is an isomorphism, and the centre becomes a component of the exceptional divisor.

Relation to the source.

• Translation. P is Włodarczyk's principalization as a rule on all pairs $(M, I)$, the morphism $\mathrm{prin}$ of his last sentence: for the pair T = (M, I), P T is the compatible family of $\mathrm{prin}_I \colon \tilde M \to M$, and T.I.IsLocallyFinitelyPrincipalizedBy (P T) is his "there exists a locally finite principalization of $I$", with clauses (1)–(3).
• Correction. The hypothesis that $I$ has nonzero stalks (the field isNonzeroEverywhere of the pair) is tacit in the source: otherwise the total transform $\sigma^{r*}(I)$ could not be the ideal of a divisor. Kollár states it explicitly, for an ideal sheaf "not zero on any irreducible component" [Kol07, Theorem 35]. The ideal sheaves with a zero stalk are not inputs, so nothing is asserted of them.
• Interpretation. In Włodarczyk's clause (3), the total transform $\sigma^{r*}(I)$ "is the ideal of a simple normal crossing divisor $\tilde E_U$ which is a locally finite combination of the irreducible components of the divisor $E_{U_r}$": the exponents of $\tilde E_U$ are read at each point, $\tilde E_U$ near a point being a combination of the components of $E_{U_r}$ through it.
• Interpretation. Włodarczyk's sheaf of ideals $\tilde I$ on $\tilde M$, which none of his clauses mentions, is read as the total transform $\mathrm{prin}_I^*(I)$; it is asserted to be a normal-crossings divisor (IdealSheaf.IsNormalCrossingsDivisor), the form of clause (3) that is local on $\tilde M$.
• Translation. "Embeddings of ambient varieties" in the last sentence is read as Kollár's commutation with closed embeddings [Kol07, Theorem 35 (5)], in the form of [Kol07, 34.3] for an empty boundary: $B(X, I_X) = j_* B(Y, I_Y)$ for a closed embedding $j$ of smooth varieties with $\mathcal{O}_X / I_X = j_*(\mathcal{O}_Y / I_Y)$, here I.IsPushforwardAlong J τ with the closed embedding τ (an analytic embedding with closed image), whose image is a closed submanifold: the ideal of the image (vanishingStalk) lies in I, and J = τ^*I. This is Włodarczyk's $I = \tau_*(J) \cdot \mathcal{O}_M$ [Wlo09, Remark (3) after Theorem 2.0.3], whose canonical resolution has the centres $\tau(C_i)$ of that of $J$ [Wlo09, Theorem 3.5.1 (3)]. The proof follows Kollár's derivation from his Claim 71.2 [Kol07, 72], the commutation of the marked order reduction with closed embeddings, through [Kol07, Theorem 107 (3)] and [Kol07, Theorem 103 (3)] at the mark 1, the value of P.
• Restatement. The commutation with closed embeddings is stated over every pair of compact sets, as the push-forward of a succession up to blow-ups whose centres lie outside the part over $\tau(U_{K'})$ (FiniteSuccession.IsPushforwardUpToEmptyAlong): the succession of P(M, I) over $U_K$ also blows up centres over $U_K \setminus \tau(U_{K'})$, which the succession over $U_{K'}$ does not see. The strict transforms of $\tau(N)$ are not formed: the relation is stated through embeddings of the stages, over $\tau$, with closed images containing every centre point over $\tau(U_{K'})$ and along which the centres pull back.
• Restatement. The commutation with local analytic isomorphisms is stated in 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 \colon N \to M$ to a local analytic isomorphism $\tilde g \colon \tilde N \to \tilde M$ over $g$ identifying $\tilde N$ with the fibre product $N \times_M \tilde M$, the "natural lifting" of [Wlo09, Theorem 2.0.1 (3)]; the fibre product is stated pointwise, as the bijection of $\tilde g$ between the fibres over corresponding points.
• Interpretation. The exact equality for a surjective local analytic isomorphism [Wlo09, Theorem 3.5.1 (1)] has no counterpart per pair of compact sets: for $g$ the identity and compacts $K' \subsetneq K$ with a centre of the succession over $U_K$ lying over $U_K \setminus U_{K'}$, the succession induced over $U_{K'}$ has an empty centre which the succession over $U_{K'}$ omits. Its global content is read as: for surjective $g$ the lift $\tilde g$ is a surjective local analytic isomorphism identifying $\tilde N$ with $N \times_M \tilde M$.
• Interpretation. Włodarczyk's analytic manifold is read as pure-dimensional: the local analytic isomorphisms relate manifolds modelled on one space, and a closed embedding relates manifolds modelled on two, so the pairs carry their model space and P is one assignment over all finite-dimensional model spaces over $\mathbb{K}$.
• Strengthening. Every neighbourhood $U_K$ has compact closure, which the source does not ask. It makes the commutations apply, for a local analytic isomorphism or a closed embedding $g \colon N \to M$, to every compact set $K'$ of $N$: the closure $K$ of $g(U_{K'})$ is compact, and $g(U_{K'}) \subseteq K \subseteq U_K$.
• Strengthening. The clause that $\mathrm{prin}_I$ is an isomorphism over the complement of the support of $I$ is not in [Wlo09, Theorem 2.0.3]; it is [Wlo09, Lemma 4.0.3] and, for an empty boundary, [Kol07, Theorem 35 (3)].
• Strengthening. Each centre has a single codimension, and empty centres are admitted (their blow-ups are isomorphisms).
• Gap. Compared with Kollár's functorial principalization [Kol07, Theorem 35] (AlgebraicGeometry.exists_functorial_principalization): the inputs are pairs $(M, I)$, Kollár's triples with an empty boundary; the values are compatible families over the compact sets rather than single blow-up sequences, as Kollár's passage to analytic spaces provides them [Kol07, 44]; the commutation with smooth morphisms [Kol07, 34.1] is asserted, in Włodarczyk's form, for local analytic isomorphisms only, the smooth morphisms of relative dimension zero; and the commutation with change of fields [Kol07, 34.2] has no counterpart.

Source statement: [Wlo09, Theorem 2.0.3, p. 35]

Source statement: [Kol07, Theorem 35] (analytic manifolds, empty boundary; item 44)