The saturation defining the strict transform is of finite type

For a blowing-up π : M' → M with centre Y and exceptional ideal I_F, and an ideal sheaf of finite type I on M, the saturation ⋃_k (π⁻¹(I)_{a'} : I_{F,a'}^k) (saturationStalk) is the stalk family of an ideal sheaf of finite type, over ℝ as over ℂ (saturationStalk_hasLocalGenerators): this is Bierstone–Milman's "I_{X'} is an ideal of finite type since X is locally Noetherian" [BM97, Proposition 3.13], obtained here from the finite type of saturations on analytic spaces (AnalyticSpace.saturation_hasLocalGenerators of Hironaka.AnalyticSpace.Noether.Saturation) read on the analytic space of the blown-up manifold. It is the hypothesis under which the strict transform strictTransformSubspace has the saturation as its stalks, supplied at each step of a sequence of blowings-up.

theorem Manifold.saturationStalk_hasLocalGenerators {K : Type} [RCLike K] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace K E] {n : ℕ} {ψ : E ≃L[K] Fin n → K} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf K E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) (I : IdealSheaf (structureSheaf K E M)) : IdealSheaf.HasLocalGenerators (saturationStalk hY h I)

The saturation stalks saturationStalk hY h I of the total transform of I by the powers of the exceptional ideal of the blowing-up π have local generators, over every RCLike K: the ideal-theoretic strict transform is of finite type [BM97, Proposition 3.13]. This is AnalyticSpace.saturation_hasLocalGenerators at the analytic space of M'.