The weak transform of a purely nonmonomial ideal is purely nonmonomial

Step 1 of the proof of [Kol07, Theorem 107] (item 111) rests on the remark that the transform of the nonmonomial part N(𝓘) and the marked transform of (𝓘, m) differ by a product of powers of the exceptional divisors, hence only in their monomial part. Its content for one blow-up is that the marked transform of N(𝓘), taken at its exact order along the centre, is again purely nonmonomial for the transformed boundary family. This file proves that statement: for an ideal sheaf K whose exponents along all components of the boundary family F vanish, with ord_Y K = d along the centre Y and ord K ≤ d at every point of Y, the weak transform W = π_*^{-1}(K, d) has vanishing exponents along every component of F' = F.totalTransform π Y (componentExponent_weakTransformOf_eq_zero), so that M_{F'}(W) = ⊤ and N_{F'}(W) = W. The components of F' are of two kinds.

• Components of the strict transforms of the members. The exponent of W along such a component C' is read at a point of C' off the exceptional divisor, which exists because C' is relatively open in the strict transform of the member and π⁻¹(E^j \ Y) is dense there. At such a point W is the total transform of K, the blow-up is a local analytic isomorphism, and the exponent is an exponent of K along a component of F, hence zero.
• Components of the exceptional divisor. The exponent of W along such a component α is read at a point of α where W is the unit ideal. Such a point exists by Kollár's computation of the transform in coordinates [Kol07, Definition 60, (60.3)], as in the proof of [Kol07, Lemma 61]: an element f of K of order d at the base point has transform f / x_r^d = Q(y), a polynomial in the ratio coordinates y with a unit coefficient; the polynomial of values is nonzero, so some ratio vector t has Q(t) ≠ 0, and the slice of the blow-up chart with the scaling and off-block coordinates of the base point is connected, so the point with ratios t lies in α.

The weak transform, the total transform divided by the exact power of the ideal of the exceptional divisor, is Hironaka's [Hir64, §5, p. 142]; the marked transform at the exact order coincides with it (birationalTransform_eq_weakTransformOf_of_ordAlong_eq).

A component contains the connected component of any of its points

theorem Hironaka.Manifold.BMO.mem_componentSet_of_mem_connectedComponentIn {X : Type u} [TopologicalSpace X] (G : Manifold.HypersurfaceFamily X) (i : ComponentIndex G) {x y : X} (hx : x ∈ componentSet G i) (hy : y ∈ connectedComponentIn (G.hyp i.fst) x) : y ∈ componentSet G i

A point of the connected component of x in the member E^j, for x on the component i = ⟨j, C⟩, lies on componentSet G i: the connected component of x is the class of x.

Off the exceptional divisor

theorem Hironaka.Manifold.BMO.weakTransformOf_stalkIdeal_of_notMem {𝕜 : 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] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) [T2Space M] [SecondCountableTopology M] (K : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) {a' : M'} (ha' : π a' ∉ Y) : (Manifold.IdealSheaf.weakTransformOf hY h K).stalkIdeal a' = (Manifold.IdealSheaf.pullback π ⋯ K).stalkIdeal a'

Off the centre the weak transform has the stalk of the total transform: the exponent of the exceptional ideal that is divided out is the (generic) order of K along the empty trace of the centre, that is toNat ⊤ = 0, so the colon is by the unit ideal.

theorem Hironaka.Manifold.BMO.ordAlongIdeal_totalTransform_of_isLocalDiffeomorphAt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (h : Manifold.IsBlowUp ψ Y c π) (D J : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) {a' : M'} (hloc : IsLocalDiffeomorphAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ π a') : (Manifold.IdealSheaf.pullback π ⋯ D).ordAlongIdeal (Manifold.IdealSheaf.pullback π ⋯ J) a' = D.ordAlongIdeal J (π a')

At a point where the blow-up is a local analytic isomorphism, the order of the total transform of J along the total transform of D equals the order of J along D at the image point: the germ map is bijective there and carries the stalk ideals, their inclusions and their powers.

A point of a strict-transform component off the centre

theorem Hironaka.Manifold.BMO.exists_mem_componentSet_inl_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (F : Manifold.HypersurfaceFamily M) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hsnc : Manifold.HypersurfaceFamily.HasSncWith ψ F Y c) {j : F.ι} (C' : ConnectedComponents ↑((Manifold.HypersurfaceFamily.totalTransform π Y F).hyp (toLex (Sum.inl j)))) : ∃ a' ∈ componentSet (Manifold.HypersurfaceFamily.totalTransform π Y F) ⟨toLex (Sum.inl j), C'⟩, π a' ∉ Y

Every component C' of the strict transform of a member E^j contains a point off the exceptional divisor: C' is the trace on the strict transform closure (π⁻¹(E^j \ Y)) of an open set, which therefore meets π⁻¹(E^j \ Y).

The exponent along a strict-transform component is an exponent below

theorem Hironaka.Manifold.BMO.componentExponent_weakTransformOf_inl_eq {𝕜 : 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] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (F : Manifold.HypersurfaceFamily M) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hsnc : Manifold.HypersurfaceFamily.HasSncWith ψ F Y c) [T2Space M] [SecondCountableTopology M] (K : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) {j : F.ι} (C : ConnectedComponents ↑(F.hyp j)) (C' : ConnectedComponents ↑((Manifold.HypersurfaceFamily.totalTransform π Y F).hyp (toLex (Sum.inl j)))) {a' : M'} (ha' : a' ∈ componentSet (Manifold.HypersurfaceFamily.totalTransform π Y F) ⟨toLex (Sum.inl j), C'⟩) (hπ : π a' ∉ Y) (hC : π a' ∈ componentSet F ⟨j, C⟩) : componentExponent (Manifold.HypersurfaceFamily.totalTransform π Y F) ⋯ (Manifold.IdealSheaf.weakTransformOf hY h K) ⟨toLex (Sum.inl j), C'⟩ = componentExponent F hF K ⟨j, C⟩

The exponent of the weak transform along a component ⟨inl j, C'⟩ of the strict transform of E^j, read at a point a' of it off the centre lying over the component ⟨j, C⟩ of F, is the exponent of K along ⟨j, C⟩: both exponents are orders at the actual points; the weak transform has the stalk of the total transform there (weakTransformOf_stalkIdeal_of_notMem), the ideal of the component of F' is the total transform of the ideal of the component of F (stalkIdeal_totalTransform_componentIdeal_of_notMem), and the order transports along the local analytic isomorphism π (ordAlongIdeal_totalTransform_of_isLocalDiffeomorphAt).

theorem Hironaka.Manifold.BMO.componentExponent_weakTransformOf_inl {𝕜 : 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] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (F : Manifold.HypersurfaceFamily M) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hsnc : Manifold.HypersurfaceFamily.HasSncWith ψ F Y c) [T2Space M] [SecondCountableTopology M] (K : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) (hpure : ∀ (i : ComponentIndex F), componentExponent F hF K i = 0) {j : F.ι} (C' : ConnectedComponents ↑((Manifold.HypersurfaceFamily.totalTransform π Y F).hyp (toLex (Sum.inl j)))) : componentExponent (Manifold.HypersurfaceFamily.totalTransform π Y F) ⋯ (Manifold.IdealSheaf.weakTransformOf hY h K) ⟨toLex (Sum.inl j), C'⟩ = 0

If K is purely nonmonomial for F (every exponent along a component of F is 0, as for K = N(𝓘) by componentExponent_nonmonomialPart_eq_zero), then the exponent of its weak transform along every component ⟨inl j, C'⟩ of a strict transform is 0: read it at a point of C' off the centre (exists_mem_componentSet_inl_notMem) as an exponent of K (componentExponent_weakTransformOf_inl_eq). No hypothesis on the order of K along the centre is needed.

The fibre slice of a blow-up chart lies in one exceptional component

theorem Hironaka.Manifold.BMO.exists_mem_componentSet_inr_of_ratios {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] {π : M' → M} (F : Manifold.HypersurfaceFamily M) (α : ConnectedComponents ↑((Manifold.HypersurfaceFamily.totalTransform π Y F).hyp (toLex (Sum.inr PUnit.unit)))) {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (hφ : Manifold.IsAdaptedChart ψ Y φ σ) (hΦ : Manifold.IsBlowUpChart ψ π φ σ i Φ) {a' : M'} (ha' : a' ∈ Φ.source) (hα : a' ∈ componentSet (Manifold.HypersurfaceFamily.totalTransform π Y F) ⟨toLex (Sum.inr PUnit.unit), α⟩) (t : Fin n → 𝕜) : ∃ a'' ∈ componentSet (Manifold.HypersurfaceFamily.totalTransform π Y F) ⟨toLex (Sum.inr PUnit.unit), α⟩, a'' ∈ Φ.source ∧ π a'' = π a' ∧ ψ (↑Φ a'') = fun (j : Fin n) => if ∃ (k : Fin c), k ≠ i ∧ σ k = j then t j else ψ (↑Φ a') j

In a blow-up chart Φ of index i containing a point a' of the exceptional component ⟨inr (), α⟩, every vector t of ratio coordinates is realised by a point a'' of the same component over the same base point, with the scaling and off-block coordinates of a': the slice of the chart with scaling coordinate 0 and the off-block coordinates of a' is the continuous image of the ratio space, hence connected, lies in π⁻¹(Y) and contains a', so it lies in the connected component of a' in the exceptional divisor.

The unit point: Kollár's expansion in the chart ring

theorem Hironaka.Manifold.BMO.exists_mem_componentSet_inr_birationalTransform_stalkIdeal_eq_top {𝕜 : 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] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (F : Manifold.HypersurfaceFamily M) (K : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) {d : ℕ} (hord : ∀ a ∈ Y, hY.idealSheaf.ordAlongIdeal K a = ↑d) (hle : ∀ a ∈ Y, K.ord a ≤ ↑d) (α : ConnectedComponents ↑((Manifold.HypersurfaceFamily.totalTransform π Y F).hyp (toLex (Sum.inr PUnit.unit)))) : ∃ a'' ∈ componentSet (Manifold.HypersurfaceFamily.totalTransform π Y F) ⟨toLex (Sum.inr PUnit.unit), α⟩, (Manifold.MarkedIdealSheaf.birationalTransform hY h { I := K, m := d }).I.stalkIdeal a'' = ⊤

For K of order exactly d along the centre and of order ≤ d at its points, the marked transform π_*^{-1}(K, d) is the unit ideal at some point of every component of the exceptional divisor. This is Kollár's computation of the transform in coordinates Kol07, Definition 60, (60.3), as in the proof of [Kol07, Lemma 61]: at a point a of the centre an element f of K_a of order d has transform f / x_r^d = Q(y), a polynomial in the ratio coordinates with a unit coefficient (exists_transformElem_eq_chartPresentation); the polynomial of the coefficients' values is nonzero, so some ratio vector t has a nonzero value (MvPolynomial.funext, the field being infinite); at the point a'' of the component with ratios t (exists_mem_componentSet_inr_of_ratios) the chart-ring map carries Q(y) into the stalk of the marked transform with value Q(t) ≠ 0, a unit.

The exceptional components, and the corollaries

theorem Hironaka.Manifold.BMO.componentExponent_weakTransformOf_inr {𝕜 : 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] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (F : Manifold.HypersurfaceFamily M) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hsnc : Manifold.HypersurfaceFamily.HasSncWith ψ F Y c) [T2Space M] [SecondCountableTopology M] (K : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) {d : ℕ} (hord : ∀ a ∈ Y, hY.idealSheaf.ordAlongIdeal K a = ↑d) (hle : ∀ a ∈ Y, K.ord a ≤ ↑d) (α : ConnectedComponents ↑((Manifold.HypersurfaceFamily.totalTransform π Y F).hyp (toLex (Sum.inr PUnit.unit)))) : componentExponent (Manifold.HypersurfaceFamily.totalTransform π Y F) ⋯ (Manifold.IdealSheaf.weakTransformOf hY h K) ⟨toLex (Sum.inr PUnit.unit), α⟩ = 0

With ord K ≤ d on the centre, the exponent of the weak transform along every component of the exceptional divisor is 0: read it at the point where the marked transform is the unit ideal (exists_mem_componentSet_inr_birationalTransform_stalkIdeal_eq_top), the marked transform being the weak transform at the exact order.

theorem Hironaka.Manifold.BMO.componentExponent_weakTransformOf_eq_zero {𝕜 : 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] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (F : Manifold.HypersurfaceFamily M) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hsnc : Manifold.HypersurfaceFamily.HasSncWith ψ F Y c) [T2Space M] [SecondCountableTopology M] (K : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) {d : ℕ} (hord : ∀ a ∈ Y, hY.idealSheaf.ordAlongIdeal K a = ↑d) (hle : ∀ a ∈ Y, K.ord a ≤ ↑d) (hpure : ∀ (i : ComponentIndex F), componentExponent F hF K i = 0) (i' : ComponentIndex (Manifold.HypersurfaceFamily.totalTransform π Y F)) : componentExponent (Manifold.HypersurfaceFamily.totalTransform π Y F) ⋯ (Manifold.IdealSheaf.weakTransformOf hY h K) i' = 0

All exponents of the weak transform along the components of the transformed boundary family vanish: along the strict transforms by componentExponent_weakTransformOf_inl, along the exceptional components by componentExponent_weakTransformOf_inr.

theorem Hironaka.Manifold.BMO.monomialPart_weakTransformOf_eq_top {𝕜 : 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] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (F : Manifold.HypersurfaceFamily M) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hsnc : Manifold.HypersurfaceFamily.HasSncWith ψ F Y c) [T2Space M] [SecondCountableTopology M] (K : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) {d : ℕ} (hord : ∀ a ∈ Y, hY.idealSheaf.ordAlongIdeal K a = ↑d) (hle : ∀ a ∈ Y, K.ord a ≤ ↑d) (hpure : ∀ (i : ComponentIndex F), componentExponent F hF K i = 0) : monomialPart (Manifold.HypersurfaceFamily.totalTransform π Y F) ⋯ (Manifold.IdealSheaf.weakTransformOf hY h K) = ⊤

The monomial part of the weak transform with respect to the transformed boundary family is the unit ideal: every component exponent vanishes.

theorem Hironaka.Manifold.BMO.nonmonomialPart_weakTransformOf_eq_self {𝕜 : 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] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (F : Manifold.HypersurfaceFamily M) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hsnc : Manifold.HypersurfaceFamily.HasSncWith ψ F Y c) [T2Space M] [SecondCountableTopology M] (K : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) {d : ℕ} (hord : ∀ a ∈ Y, hY.idealSheaf.ordAlongIdeal K a = ↑d) (hle : ∀ a ∈ Y, K.ord a ≤ ↑d) (hpure : ∀ (i : ComponentIndex F), componentExponent F hF K i = 0) : nonmonomialPart (Manifold.HypersurfaceFamily.totalTransform π Y F) ⋯ (Manifold.IdealSheaf.weakTransformOf hY h K) = Manifold.IdealSheaf.weakTransformOf hY h K

Purity of the weak transform: N_{F'}(W) = W, from M_{F'}(W) · N_{F'}(W) = W with M_{F'}(W) the unit ideal.

theorem Hironaka.Manifold.BMO.nonmonomialPart_birationalTransform_eq_self {𝕜 : 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] {Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (F : Manifold.HypersurfaceFamily M) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hsnc : Manifold.HypersurfaceFamily.HasSncWith ψ F Y c) [T2Space M] [SecondCountableTopology M] (K : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) {d : ℕ} (hord : ∀ a ∈ Y, hY.idealSheaf.ordAlongIdeal K a = ↑d) (hle : ∀ a ∈ Y, K.ord a ≤ ↑d) (hpure : ∀ (i : ComponentIndex F), componentExponent F hF K i = 0) : nonmonomialPart (Manifold.HypersurfaceFamily.totalTransform π Y F) ⋯ (Manifold.MarkedIdealSheaf.birationalTransform hY h { I := K, m := d }).I = (Manifold.MarkedIdealSheaf.birationalTransform hY h { I := K, m := d }).I

Purity of the marked transform at the exact order: for K purely nonmonomial for F (as K = N(𝓘)), d the exact order of K along the centre and ord K ≤ d on the centre, the marked transform π_*^{-1}(K, d) is its own nonmonomial part with respect to the transformed boundary family. This is the one-blow-up form of the remark of [Kol07, 111, Step 1].