[Kol07, Definition 66] survives the deletion of empty blow-ups

For the boundary of the main theorems, the reduced ideal sheaf F.idealSheaf of a simple normal crossings family F, a list of order ≥ m for (I, m, F.idealSheaf) [Kol07, Definition 66] stays of order ≥ m after the deletion of its empty blow-ups ([Kol07, 34.1]; BlowUpSequence.isOfOrderGe_eraseEmpty): a kept step contributes the same two clauses on both sides, with the boundary transformed to the reduced ideal sheaf of the total transform of F (reducedTransform_eq_idealSheaf_totalTransform), so that the recursion runs over simple normal crossings families; a deleted step is an isomorphism Bl_∅ M ≃ M along which Kol07, Definition 66 pulls back (isOfOrderGe_map, from the descent isOfOrderGe_of_pullback), the marked transform being the pull-back (cons_markedTransformSeq_one_of_eq_empty) and the boundary the pull-back of F.idealSheaf (reducedTransform_blowUpπ_idealSheaf_of_eq_empty: the total transform of F along the empty blowing-up has the support of π⁻¹(F), and the reduced ideal sheaf depends only on the support).

The statement is for the boundary F.idealSheaf and not for an arbitrary ideal sheaf E₀: at a deleted step the boundary becomes red(π⁻¹E₀), not π⁻¹E₀, and identifying the normal-crossings clause for E₀ with that for its reduction would need a Nullstellensatz, which is not done here. The counterpart for schemes is in Hironaka.Resolution.Algebraic.Kol07.EraseEmptyInduced.

theorem Manifold.HypersurfaceFamily.idealSheaf_congr_support {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} {F G : HypersurfaceFamily M.carrier} (h : F.support = G.support) : F.idealSheaf = G.idealSheaf

The reduced ideal sheaf of a family depends only on its support.

theorem Hironaka.Manifold.reducedTransform_blowUpπ_idealSheaf_of_eq_empty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ₀ Y c) (hY₀ : Y = ∅) {F : Manifold.HypersurfaceFamily M.carrier} (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) : AnalyticManifold.IdealSheaf.reducedTransform (Manifold.blowUpπ ψ₀ hY) F.idealSheaf hY.idealSheaf = Manifold.IdealSheaf.pullback ⇑(Manifold.blowUpπ ψ₀ hY) ⋯ F.idealSheaf

Along the chosen blowing-up of an empty centre, the reduced transform of the reduced ideal sheaf of an snc family is the pull-back of that reduced ideal sheaf: by dictionary it is the reduced ideal sheaf of the total transform, whose support is π⁻¹(|F|).

theorem AnalyticManifold.BlowUpSequence.isOfOrderGe_map {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (φ : Diffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) M.carrier N.carrier ⊤) (Z : BlowUpSequence ψ₀ M) (I E₀ : N.IdealSheaf) (m : ℕ) (h : Z.toSuccession.IsOfOrderGe (Manifold.IdealSheaf.pullback ⇑φ.toAnalyticMap ⋯ I) m (Manifold.IdealSheaf.pullback ⇑φ.toAnalyticMap ⋯ E₀)) : (map φ Z).toSuccession.IsOfOrderGe I m E₀

[Kol07, Definition 66] pulls back along a diffeomorphism: the transport of a list of order ≥ m for the pull-backs of (I, E₀) is of order ≥ m for (I, E₀) (descent isOfOrderGe_of_pullback along φ, the transport being the pull-back along φ⁻¹).

theorem AnalyticManifold.BlowUpSequence.isOfOrderGe_eraseEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (I : M.IdealSheaf) (m : ℕ) {F : Manifold.HypersurfaceFamily M.carrier} : Manifold.HypersurfaceFamily.IsSnc ψ₀ F → L.toSuccession.IsOfOrderGe I m F.idealSheaf → L.eraseEmpty.toSuccession.IsOfOrderGe I m F.idealSheaf

[Kol07, 34.1] for [Kol07, Definition 66] with the boundary: a list of order ≥ m for (I, m, red F), F an snc family, stays of order ≥ m after the deletion of its empty blow-ups — so the erased list's induced triple lies in the class.