Lemma 102: the weak transform under the first blow-up, and the empty member

Auxiliary facts about the construction of BDan (BD.lean), the analytic functor BD_{n,m,j} of [Kol07, Lemma 102]: the proof of the lemma blows up the union Z_{-1} of the components of E^j contained in cosupp(I, m) — a trivial blow-up, "the blow-up is an isomorphism", but the order of I along E^{jk} drops by m — and continues with the weak transform I_0.

• BlowUpSequence.eq_nil_of_noEmptyCenters_of_isEmpty — a list of centres on an empty manifold with no empty centre is the empty list ([Kol07, 32] on the empty manifold).
• BDan.stalkIdeal_weakTransformI_of_notMem — off Z_{-1} the weak transform I_0 is the pull-back of 𝓘 along the isomorphism π_{-1}: the exponent of the exceptional ideal in the colon description of the weak transform is the generic order of 𝓘 along the component of Z_{-1} through the point, which is 0 off Z_{-1}, so the stalk of I_0 is the image of the stalk of 𝓘 under the isomorphism of germ algebras induced by π_{-1}.
• BDan.isDBalanced_weakTransformI — the weak transform of a D-balanced ideal sheaf under the first blow-up is D-balanced (not in the sources; needed because the input functor is applied to the restriction of I_0, and [Kol07, Corollary 85] asks for a D-balanced ideal). D-balancedness is a stalkwise condition; over Z_{-1} the weak transform has order 0, so its stalk is the unit ideal and the condition is trivial; off Z_{-1} the stalk is the image of a D-balanced stalk under a ring isomorphism, and iterated derivatives and powers commute with isomorphisms.
• BDan.ord_weakTransformI_le — ord I_0 ≤ s everywhere (the proof of [Kol07, Lemma 102]: the order of I_0 along E^{jk} is that of I diminished by m, hence ≤ 0).
• BDan_eq_nil_of_hyp_eq_empty — at an empty member the value of BD_{n,m,·} is the empty list: Z_{-1} ⊆ E^j = ∅, the restricted triple lives on the empty manifold, where the value of the input has no nonempty centre, and the empty first blow-up is deleted.

theorem AnalyticManifold.BlowUpSequence.eq_nil_of_noEmptyCenters_of_isEmpty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (L : BlowUpSequence ψ₀ M) (hL : L.NoEmptyCenters) (hM : ∀ (x : M.carrier), False) : L = nil M

[Kol07, 32] on the empty manifold: a list of centres with no empty centre on a manifold without points is the empty list.

theorem Hironaka.Manifold.BDan.stalkIdeal_weakTransformI_of_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) {x' : (Manifold.blowUp ψ₀ ⋯).carrier} (hx : (piMinusOne T s j) x' ∉ BD.Zminus1 T.I s (T.F.hyp j)) : Manifold.IdealSheaf.stalkIdeal (weakTransformI T s j) x' = Ideal.map (germAlgEquiv (piMinusOne T s j) ⋯) (Manifold.IdealSheaf.stalkIdeal T.I ((piMinusOne T s j) x'))

Off Z_{-1} the weak transform I_0 is the pull-back of 𝓘 along the isomorphism π_{-1}: the stalk at x' is the image of the stalk of 𝓘 at π_{-1} x' under the isomorphism of germ algebras. In the colon description of the weak transform the exceptional ideal appears with the exponent given by the generic order of 𝓘 along the component of Z_{-1} through the point, which is 0 off Z_{-1}, so the weak transform there is the total transform, whose stalk is stalkIdeal_comap_eq_map_germAlgEquiv.

theorem Hironaka.Manifold.BDan.isDBalanced_weakTransformI {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) (hT : BDClass s T) : Manifold.IdealSheaf.IsDBalanced (weakTransformI T s j) s

The weak transform of a D-balanced ideal sheaf under the first blow-up of Lemma 102 is D-balanced at the same mark (not in the sources; the proof of [Kol07, Lemma 102] applies the going-up theorem to the D-balanced I_0). Stalkwise: over Z_{-1} the weak transform has order 0 (BD.ord_weakTransformOf_eq_zero_of_mem_Zminus1), so its stalk is the unit ideal and the inclusion (D^i J)^s ≤ J^{s-i} is trivial; off Z_{-1} the stalk is the image of the stalk of 𝓘 under a ring isomorphism (stalkIdeal_weakTransformI_of_notMem), and the image of a D-balanced ideal under a ring isomorphism is D-balanced, iterated derivatives and powers commuting with the isomorphism.

theorem Hironaka.Manifold.BDan.ord_weakTransformI_le {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (T : Manifold.AnalyticTriple ψ₀ M) (s : ℕ) (j : T.F.ι) (hT : BDClass s T) (x' : (Manifold.blowUp ψ₀ ⋯).carrier) : Manifold.IdealSheaf.ord (weakTransformI T s j) x' ≤ ↑s

The proof of [Kol07, Lemma 102], "since max-ord_{E^{jk}} I ≤ m to start with": the weak transform I_0 has order at most s everywhere — order 0 over Z_{-1}, the order of 𝓘 at the image point off it.

theorem Hironaka.Manifold.BDan_eq_nil_of_hyp_eq_empty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} {m : ℕ} (inp : BMOanData 𝕜 (n - 1) (IsLocalRing.tuningParam m)) (T : Manifold.AnalyticTriple ψ₀ M) (hT : Manifold.AnalyticTriple.BOClass m T) (j : T.F.ι) (hj : T.F.hyp j = ∅) : BDan m inp T hT j = AnalyticManifold.BlowUpSequence.nil M

At an empty member the value of BD_{n,m,·} is the empty list ([Kol07, 32]): Z_{-1} ⊆ E^j = ∅, the restricted triple lives on the empty manifold, where the value of the input functor has no nonempty centre, and the empty first blow-up is deleted.