The logarithmic derivative rule and Kollár's Theorem 88 for one blowing-up

For a blowing-up π : M' → M with centre Y ⊆ S, S a smooth hypersurface with strict transform S', and a marked ideal sheaf (J, m) of order ≥ m along Y:

• birationalTransform_logDerivIter_le, the logarithmic version of the derivative rule [Kol07, 87, (87.3)] ("a logarithmic version of (76), proved the same way using (75.4)"): π_*^{-1}(D^j(−log S)(J), m − j) ⊆ D^j(−log S')(π_*^{-1}(J, m)) for j ≤ m;
• iteratedDeriv_birationalTransform_eq_sum, [Kol07, Theorem 88] for one blowing-up: D^s(π_*^{-1}(J, m)) = ∑_{j ≤ s} D^{s−j}(−log S')(π_*^{-1}(D^j J, m − j)) for s ≤ m.

Both are proved stalk by stalk at a point a' of M', in three cases:

• a' ∉ S': D(−log S') is the full derivative there (I_{S',a'} = (1)), and the statements reduce to the derivative rule of Hironaka.Manifold.BlowUp.Transform.DerivTransform; for (88.1) the j = 0 summand alone is D^s(π_*^{-1}(J, m))_{a'};
• a' ∈ S' over the centre: Kollár's good chart (exists_kollarChartData_of_mem_strictTransform) reads both sides through the chart-ring map χ, where the chart-level statements for schemes hold (transform_Dlogpow_le_chartDlogpow for (87.3), iterate_chartD_transformIdeal_le for the ⊆ of (88.1)), and the rule (75.1) carries D', D'(−log y_{h₀}) into D, D(−log S') (map_chartDlogpow_le_logDerivativeIter, derivativeIter_map_le_map_iterate_chartD_of_span);
• a' ∈ S' off the centre: π is a local isomorphism, both birational transforms are total transforms and D(−log S), D commute with local isomorphisms (stalkIdeal_logDerivIter_pullback_of_bijective, stalkIdeal_iteratedDeriv_pullback_of_bijective); for (88.1) the j = s summand.

The ⊇ of (88.1) is the derivative rule with D^{s−j}(−log S') ⊆ D^{s−j} and D^{s−j} D^j = D^s. The counterparts for schemes are in Hironaka.Scheme.BlowUpSequence.Theorem88Basic; this is the one-step form from which the theorem along a sequence of blowings-up is assembled.

theorem Manifold.birationalTransform_logDerivIter_le {𝕜 : 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] [FiniteDimensional 𝕜 E] {S Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) (hS : IsClosedSubmanifold ψ S 1) (hYS : Y ⊆ S) (hS' : IsClosedSubmanifold ψ (strictTransformSet π Y S) 1) (J : IdealSheaf (structureSheaf 𝕜 E M)) {m j : ℕ} (hm : ∀ a ∈ Y, ↑m ≤ hY.idealSheaf.ordAlongIdeal J a) (hj : j ≤ m) : (MarkedIdealSheaf.birationalTransform hY h { I := IdealSheaf.logDerivIter E ψ hS j J, m := m - j }).I ≤ IdealSheaf.logDerivIter E ψ hS' j (MarkedIdealSheaf.birationalTransform hY h { I := J, m := m }).I

The logarithmic derivative rule [Kol07, 87, (87.3)] for one blowing-up: for a blowing-up π with centre Y ⊆ S, m ≤ ord_Y J at every point of Y and j ≤ m, π_*^{-1}(D^j(−log S)(J), m − j) ⊆ D^j(−log S')(π_*^{-1}(J, m)), S' the strict transform of S.

theorem Manifold.iteratedDeriv_birationalTransform_eq_sum {𝕜 : 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] [FiniteDimensional 𝕜 E] {S Y : Set M} {c : ℕ} {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) (hS : IsClosedSubmanifold ψ S 1) (hYS : Y ⊆ S) (hS' : IsClosedSubmanifold ψ (strictTransformSet π Y S) 1) (J : IdealSheaf (structureSheaf 𝕜 E M)) {m s : ℕ} (hm : ∀ a ∈ Y, ↑m ≤ hY.idealSheaf.ordAlongIdeal J a) (hs : s ≤ m) : (MarkedIdealSheaf.birationalTransform hY h { I := J, m := m }).I.iteratedDeriv s = ∑ j ∈ Finset.range (s + 1), IdealSheaf.logDerivIter E ψ hS' (s - j) (MarkedIdealSheaf.birationalTransform hY h { I := J.iteratedDeriv j, m := m - j }).I

Kollár's Theorem 88 for one blowing-up [Kol07, Theorem 88]: for a blowing-up π with centre Y ⊆ S, m ≤ ord_Y J at every point of Y and s ≤ m, D^s(π_*^{-1}(J, m)) = ∑_{j=0}^{s} D^{s−j}(−log S')(π_*^{-1}(D^j J, m − j)): the order of restricting to x₁ = 0 and transforming "does not matter" (the proof of [Kol07, Lemma 62]); (87.2) applied to π_*^{-1}(J, m) in the good charts, where ∂/∂y₁ commutes with the transform by (75.1); the ⊇ is the derivative rule (markedTransform_iteratedDeriv_le) with the filtration.