The total transform as the exceptional power times the marked transform

For a blow-up π : M' → M with centre Y and exceptional divisor F, the marked transform of a marked ideal (J, k) with k ≤ ord_Y J is defined by π_*^{-1}(J, k) := (𝒪(kF) · π^* J, k) [Kol07, Definition 60, (60.1)], that is, by dividing the k-th power of the ideal of F out of the total transform π^* J. This file states the definition as a product: at every point of M', π^*(J) = 𝓘_F^k · π_*^{-1}(J, k) as ideal sheaves (totalTransform_eq_exc_pow_mul_birationalTransform). Over the centre this is the exact division A = u^k · (A : u^k) in the stalk, read in a blow-up chart where the exceptional divisor is a coordinate hyperplane; off the centre both sides are the pull-back of J. As a special case, the total transform of the ideal sheaf of a smooth hypersurface D ⊇ Y is the exceptional ideal times the ideal of the strict transform of D.

Step 1 of the proof of [Kol07, Theorem 107] uses this to compare the marked transform of (𝓘, m) with the transform of the nonmonomial part N(𝓘): the two differ by a power of the exceptional ideal, which the nonmonomial part ignores (BMO/Step1PerBlowUp.lean).

theorem Hironaka.Manifold.BMO.stalkIdeal_totalTransform_eq_exc_pow_mul_birationalTransform {𝕜 : 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 π) {J : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)} {k : ℕ} (hk : ∀ x ∈ Y, ↑k ≤ hY.idealSheaf.ordAlongIdeal J x) {φ : OpenPartialHomeomorph M E} {σ : Fin c ↪ Fin n} {i : Fin c} {Φ : OpenPartialHomeomorph M' E} (hφ : Manifold.IsAdaptedChart ψ Y φ σ) (hΦ : Manifold.IsBlowUpChart ψ π φ σ i Φ) {p : M'} (hp : p ∈ Φ.source) (hpY : π p ∈ Y) : (Manifold.IdealSheaf.pullback π ⋯ J).stalkIdeal p = (Manifold.IdealSheaf.pullback π ⋯ hY.idealSheaf).stalkIdeal p ^ k * (Manifold.MarkedIdealSheaf.birationalTransform hY h { I := J, m := k }).I.stalkIdeal p

At a point p over the centre in a blow-up chart, the stalk of the total transform π^* J is the k-th power of the stalk of the exceptional ideal times the stalk of the marked transform of (J, k), for k ≤ ord_Y J: the exact division A = u^k · (A : u^k) of Kol07, Definition 60, (60.1), where u is the coordinate of the exceptional divisor in the chart.

theorem Hironaka.Manifold.BMO.totalTransform_eq_exc_pow_mul_birationalTransform {𝕜 : 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 π) {J : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)} {k : ℕ} (hk : ∀ x ∈ Y, ↑k ≤ hY.idealSheaf.ordAlongIdeal J x) : Manifold.IdealSheaf.pullback π ⋯ J = Manifold.IdealSheaf.pullback π ⋯ hY.idealSheaf ^ k * (Manifold.MarkedIdealSheaf.birationalTransform hY h { I := J, m := k }).I

The identity π^*(J) = 𝓘_F^k · π_*^{-1}(J, k) as ideal sheaves on the blow-up, for a mark k ≤ ord_Y J [Kol07, Definition 60, (60.1)]: stalkwise, over the centre by the chart computation stalkIdeal_totalTransform_eq_exc_pow_mul_birationalTransform, off the centre because the exceptional ideal is the unit ideal and the marked transform is the total transform there.

theorem Hironaka.Manifold.BMO.comap_idealSheaf_eq_exc_mul_strictTransform {𝕜 : 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 π) {D : Set M} (hD : Manifold.IsClosedSubmanifold ψ D 1) (hYD : Y ⊆ D) : Manifold.IdealSheaf.pullback π ⋯ hD.idealSheaf = Manifold.IdealSheaf.pullback π ⋯ hY.idealSheaf * ⋯.idealSheaf

For a smooth hypersurface D containing the centre Y, the total transform of its ideal sheaf is the exceptional ideal times the ideal sheaf of the strict transform of D: π^*(𝓘_D) = 𝓘_F · 𝓘_{D̃}. The case k = 1 of totalTransform_eq_exc_pow_mul_birationalTransform, 𝓘_D having order ≥ 1 along Y ⊆ D, together with the identification of the ideal of the strict transform with the marked transform of (𝓘_D, 1).