The composite of a blow-up sequence carries a closed subspace into its strict transform

For a closed subspace Y ⊆ M with ideal sheaf J and a finite blow-up sequence π_0, …, π_{r-1} with smooth centres, the ideal-theoretic strict transforms Y_i of FiniteSuccession.strictTransformSubspaceSeq (StrictSubspaceSeq.lean) contain the inverse images of J: σ^{i*}(J) · 𝒪_{U_i} ⊆ 𝓘_{Y_i} for the composite σ^i : U_i → M. At each step the strict transform contains the total transform (totalTransform_le_strictTransformSubspace): the strict transform is the saturation of the total transform by the exceptional divisor [BM97, §3, Proposition 3.13], the total transform being the subspace defined by the inverse image ideal [Hir64, Ch. 0, §5, pp. 141–142]; compare σ^*(I_Y) = I_Ỹ I_Ẽ in [Wlo09, Theorem 2.0.2(6)]. Inverse images compose along the composite (IdealSheaf.pullback_comp). Read on the analytic spaces Sp(U_i), Sp(M), this is exactly the compatibility QuotientSpace.Compat that KLocallyRingedSpace.quotientMap needs to induce the morphism of closed subspaces Y_r → Y_0 over σ^r: the local resolution map Ỹ_Z → Y_Z of Włodarczyk's canonical desingularization of a germ [Wlo09, §4, (3)⇒(4)] (which, as Kollár warns, need not itself be a composite of smooth blow-ups [Kol07, Warning 23]), and the fields map/map_comp of AmbientBlowUpFactorization.

• FiniteSuccession.comap_stageMap_le_strictTransformSubspaceSeq S J i: σ^{i*}J ≤ 𝓘_{Y_i}.
• FiniteSuccession.compat_composite_strictTransformSubspaceSeq S ψ J: the Compat of Sp(σ^r) between 𝓘_{Y_r} and J.

theorem AnalyticManifold.FiniteSuccession.comap_stageMap_le_strictTransformSubspaceSeq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (J : M.IdealSheaf) (i : Fin (S.length + 1)) : Manifold.IdealSheaf.pullback ⇑(S.stageMap i) ⋯ J ≤ S.strictTransformSubspaceSeq J i

Along the succession the inverse image of the closed subspace J under the composite σ^i : U_i → M lies in the strict transform Y_i: by induction on the stage, each step being totalTransform_le_strictTransformSubspace at the succession's witnesses (the strict transform is the saturation of the total transform, [BM97, §3, Proposition 3.13]; the total transform is [Hir64, Ch. 0, §5, pp. 141–142]).

theorem AnalyticManifold.FiniteSuccession.compat_composite_strictTransformSubspaceSeq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) (ψ : E ≃L[𝕜] Fin n → 𝕜) (J : M.IdealSheaf) : AnalyticSpace.QuotientSpace.Compat (↑(AnalyticSpace.toSpaceHom ψ S.composite)) (S.strictTransformSubspaceSeq J (Fin.last S.length)) J

The composite Sp(σ^r) : Sp(U_r) → Sp(M) is compatible (QuotientSpace.Compat) with the final strict transform 𝓘_{Y_r} and J: the hypothesis under which KLocallyRingedSpace.quotientMap induces the morphism of closed subspaces Sp(U_r)/𝓘_{Y_r} → Sp(M)/J over Sp(σ^r), the local resolution map Ỹ_Z → Y_Z of [Wlo09, §4, (3)⇒(4)] and the fields map/map_comp of AmbientBlowUpFactorization.