A nonzero ideal sheaf stays nonzero along a blow-up sequence

The disjoined triple of [Kol07, 72] carries the pull-back π^* I of the ideal sheaf along the composite of the disjoining blow-ups, and the domain of the order-reduction functor (AnalyticTriple) asks it to be nonzero at every point, as Hironaka's "coherent sheaf of non-zero ideals" [Hir64, Main Theorem II(N), p. 176]. Along one blowing-up the germ map is injective (IsBlowUp.germMap_injective), so the stalk of the pull-back — the image of the stalk under the germ map — is nonzero; along the succession, by induction on the stage through the functoriality of comap. Used for the disjoined input of the order reduction (DisjoinInput.lean).

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

The pull-back of a nonzero-everywhere ideal sheaf along a blowing-up is nonzero everywhere: its stalk is the image of a nonzero stalk under the injective germ map.

theorem Hironaka.Manifold.isNonzeroEverywhere_comap_stageMap {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} [FiniteDimensional 𝕜 E] {S : M.FiniteSuccession} {I : M.IdealSheaf} (hI : Manifold.IdealSheaf.IsNonzeroEverywhere I) (i : Fin (S.length + 1)) : (Manifold.IdealSheaf.pullback ⇑(S.stageMap i) ⋯ I).IsNonzeroEverywhere

Along a blow-up sequence the pull-back of a nonzero-everywhere ideal sheaf to every stage is nonzero everywhere (induction on the stage; comap is functorial).