Empty rounds: the rounds over a region of low order erase to nothing

Kollár's remark after [Kol07, Theorem 68], that the order reduction BO_m does nothing when max-ord I < m, for the rounds of the resolution family (Hironaka/Resolution/Analytic/Wlo09/Rounds.lean). The round BO_{n,d+1} on a triple of its class produces a sequence of order ≥ d + 1 (the field isOfOrderGe, [Kol07, Definition 66 (4′)]); over a reading map into a region where the order of the ideal is ≤ d, no centre can be met: stage by stage the marked transform keeps order ≤ d, the centre (which lies where that order is ≥ d + 1) has empty preimage, the blowing-up is an isomorphism there and the marked transform is the total transform (birationalTransform_I_of_eq_empty). So the round's list pulled back along the reading map erases to the empty list (eraseEmpty_pullback_roundList_eq_nil), and where the ideal is the unit ideal every round does, whatever their number (eraseEmpty_resolveFrom_eq_nil_of_ord_eq_zero, the case of an admissible chain with no round in Hironaka/Resolution/Analytic/Wlo09/Canonicity.lean).

• FiniteSuccession.isEmptyAt_of_ord_le_of_lt: the order bound read pointwise; a centre lying where the marked transform has order ≥ m is empty when that order is ≤ b < m.
• ord_markedTransformSeq_pullback_le_of_lt: the bound ≤ b propagates along the pulled-back sequence (the recursion; isOfOrderGe_pullback).
• BlowUpSequence.eraseEmpty_eq_nil_of_forall_isEmptyAt: a list of empty centres erases to nil (the empty blow-up convention [Kol07, 32], via the count length_eraseEmpty_add_emptyCount).
• IdealSheaf.ord_comap_of_isLocalDiffeomorphAt: the order of an inverse image ideal sheaf at a point where the map is a local isomorphism, in the comap form.

theorem AnalyticManifold.FiniteSuccession.isEmptyAt_of_ord_le_of_lt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : AnalyticManifold 𝕜 E} (S : M.FiniteSuccession) {I E₀ : M.IdealSheaf} {m b : ℕ} (hge : S.IsOfOrderGe I m E₀) (hb : b < m) (i : Fin S.length) (hlt : ∀ (x : (S.stage i.castSucc).carrier), Manifold.IdealSheaf.ord (S.markedTransformSeq I m i.castSucc) x ≤ ↑b) : S.IsEmptyAt i

The order bound of [Kol07, Definition 66 (4′)] read pointwise: a centre of a sequence of order ≥ m for (I, m) lies where the marked transform has order ≥ m (ordAlong_le_ord); if that order is ≤ b < m at every point of the stage, the centre is empty.

theorem AnalyticManifold.IdealSheaf.ord_comap_of_isLocalDiffeomorphAt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M N : AnalyticManifold 𝕜 E} (J : M.IdealSheaf) (f : AnalyticMap N M) {b : N.carrier} (hf : IsLocalDiffeomorphAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ (⇑f) b) : (Manifold.IdealSheaf.pullback ⇑f ⋯ J).ord b = Manifold.IdealSheaf.ord J (f b)

ord_pullback_of_isLocalDiffeomorphAt in the comap form: the order of the inverse image ideal sheaf at a point where the map is a local isomorphism is the order of the ideal sheaf at the image point.

theorem Hironaka.Manifold.ord_markedTransformSeq_pullback_le_of_lt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M N : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (L : AnalyticManifold.BlowUpSequence ψ₀ M) {m : ℕ} (hge : L.toSuccession.IsOfOrderGe T.I m T.F.idealSheaf) (h : AnalyticMap N M) (hh : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ ⇑h) {b : ℕ} (hb : b < m) (hlow : ∀ (y : N.carrier), Manifold.IdealSheaf.ord T.I (h y) ≤ ↑b) (i : Fin ((L.pullback h hh).length + 1)) (x : ((L.pullback h hh).stage i).carrier) : Manifold.IdealSheaf.ord ((L.pullback h hh).toSuccession.markedTransformSeq (Manifold.IdealSheaf.pullback ⇑h ⋯ T.I) m i) x ≤ ↑b

Along a pulled-back sequence: if L is of order ≥ m for the triple T and T.I has order ≤ b < m on the image of the local analytic isomorphism h, every marked transform of (h^* T.I, m) along h^* L has order ≤ b. Stage by stage: the centre lies where the marked transform has order ≥ m, so it is empty (isEmptyAt_of_ord_le_of_lt), the blowing-up is then an isomorphism and the marked transform is the total transform (birationalTransform_I_of_eq_empty), whose order at a point is the order below it.

theorem AnalyticManifold.BlowUpSequence.eraseEmpty_eq_nil_of_forall_isEmptyAt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (h : ∀ (i : Fin L.toSuccession.length), L.toSuccession.IsEmptyAt i) : L.eraseEmpty = nil M

A list all of whose centres are empty erases to the empty list ([Kol07, 32]: the count of empty centres is the length, length_eraseEmpty_add_emptyCount).

theorem Hironaka.Manifold.eraseEmpty_pullback_roundList_eq_nil {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bo : (d : ℕ) → BOanFam 𝕜 n d) {d : ℕ} {X : AnalyticManifold 𝕜 (Fin n → 𝕜)} (cur : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) X) (hcls : Manifold.AnalyticTriple.BOClass (d + 1) cur) (O : TopologicalSpace.Opens X.carrier) (hO : IsCompact (closure ↑O)) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (ι' : AnalyticMap N (X.restrict O)) (hι' : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑ι') (hlow : ∀ (y : N.carrier), Manifold.IdealSheaf.ord (cur.pullback (X.inclusion O) ⋯).I (ι' y) ≤ ↑d) : ((roundList bo cur hcls O hO).pullback ι' hι').eraseEmpty = AnalyticManifold.BlowUpSequence.nil N

The empty round over the reading image (the remark after [Kol07, Theorem 68]). The list of the round BO_{n,d+1} at O, pulled back along a reading map ι' into O on whose image the order is ≤ d, erases to the empty list: every centre lies in {ord ≥ d + 1} of the current marked transform (the field isOfOrderGe, [Kol07, Definition 66 (4′)]), which the image never meets, along the list, stage by stage.

theorem Hironaka.Manifold.eraseEmpty_resolveFrom_eq_nil_of_ord_eq_zero {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (bo : (d : ℕ) → BOanFam 𝕜 n d) (d : ℕ) {X : AnalyticManifold 𝕜 (Fin n → 𝕜)} (cur : Manifold.AnalyticTriple (ContinuousLinearEquiv.refl 𝕜 (Fin n → 𝕜)) X) (hord : ∀ (x : ↑↧X.carrier), Manifold.IdealSheaf.ord cur.I x ≤ ↑d) (hfin : Finite { j : cur.F.ι // cur.F.hyp j ≠ ∅ }) (Ω : ℕ → TopologicalSpace.Opens X.carrier) (hΩ : ∀ k < d, IsCompact (closure ↑(Ω k))) (hΩsub : ∀ (k : ℕ), k + 1 < d → closure ↑(Ω k) ⊆ ↑(Ω (k + 1))) {N : AnalyticManifold 𝕜 (Fin n → 𝕜)} (ι : AnalyticMap N X) (hι : IsLocalDiffeomorph (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) (modelWithCornersSelf 𝕜 (Fin n → 𝕜)) ⊤ ⇑ι) (hrange : Set.range ⇑ι ⊆ ↑(Ω 0)) (hzero : ∀ (y : N.carrier), Manifold.IdealSheaf.ord cur.I (ι y) ≤ ↑0) : (resolveFrom bo d cur hord hfin Ω hΩ hΩsub ι hι hrange).eraseEmpty = AnalyticManifold.BlowUpSequence.nil N

No rounds over a region where the ideal is the unit ideal. If the order is 0 on the reading image, the rounds read through ι erase to the empty list, whatever their number: every round's centres miss the image (eraseEmpty_pullback_roundList_eq_nil), and the marked transforms over it stay the unit ideal. The case of an admissible chain with no round in Hironaka/Resolution/Analytic/Wlo09/Canonicity.lean.