The derivative of a birational transform under one blowing-up

For one blowing-up π : M' → M with centre Y and a marked ideal sheaf (I, m) with ord_Y I ≥ m, π_*^{-1}(D^j(I), m − j) ⊆ D^j(π_*^{-1}(I, m)) for j ≤ m (markedTransform_iteratedDeriv_le): the case of one blow-up of [Kol07, Theorem 76] (for j = 1 and one blow-up the statement is the content of the formulas (75.1)–(75.3), and "the rest follows by induction on j"), also [Wlo05, Lemma 2.6.3]. The proof is stalkwise:

• over the centre, the stalk of the birational transform is the image under the chart-ring map χ of the algebraic transform transformIdeal (birationalTransform_stalkIdeal_eq_map_transformIdeal), the stalk of D(I) is the coordinate derivative κ.D I_a in regular coordinates of the stalk (stalkIdeal_deriv_eq_D, taken in Kollár's order τ), the version for schemes gives π_*^{-1}(D(I), m) ⊆ D'(π_*^{-1}(I, m + 1)) in the chart ring (transform_D_le_chartD), and the formulas (75.1)–(75.3) carry D' into D (chartRingHom_chartDerivRing_eq_coordDerivStalk, map_chartD_le_derivative);
• off the centre both birational transforms are total transforms along the local isomorphism π, and D commutes with local isomorphisms (stalkIdeal_deriv_pullback_of_isLocalDiffeomorphAt).

The order bookkeeping ord_Y D^j(I) ≥ m − j (the step "(74.3)" in the proof of [Kol07, Corollary 77]) is le_ordAlongIdeal_iteratedDeriv, the stalk form of the algebraic Dpow_le_chartCenter_pow.

The strict transform of a smooth hypersurface H ⊇ Y has ideal sheaf π_*^{-1}(I_H, 1) (idealSheaf_strictTransform_eq_markedTransform_one): isIdealSheafOf_strictTransform of Hironaka.Manifold.BlowUp.Transform.StrictIdeal read through the uniqueness of the ideal sheaf of a closed submanifold; [Wlo05, Lemma 2.7.4], and the proof of [Kol07, Theorem 80].

These results feed the derivative rules along a sequence of blowings-up (Hironaka.Manifold.FiniteSuccession.DerivTransform).

theorem Ideal.derivative_bot {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] : derivative k ⊥ = ⊥

The derivative ideal of the zero ideal is zero.

theorem Ideal.derivativeIter_bot {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (r : ℕ) : derivativeIter k r ⊥ = ⊥

The iterated derivative ideals of the zero ideal are zero.

theorem Manifold.IdealSheaf.deriv_mono {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [FiniteDimensional 𝕜 E] {J K : IdealSheaf (structureSheaf 𝕜 E M)} (h : J ≤ K) : J.deriv ≤ K.deriv

The derivative ideal sheaf is monotone.

theorem Manifold.IdealSheaf.iteratedDeriv_mono {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [FiniteDimensional 𝕜 E] {J K : IdealSheaf (structureSheaf 𝕜 E M)} (h : J ≤ K) (j : ℕ) : J.iteratedDeriv j ≤ K.iteratedDeriv j

The iterated derivative ideal sheaves are monotone.

theorem Manifold.exists_regularCoords_reindex {𝕜 : 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] (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) (τ : Fin n ≃ Fin n) : ∃ (κ : IsLocalRing.RegularCoords (↑((structureSheaf 𝕜 E M).presheaf.stalk a)) n), (∀ (j : Fin n), κ.x j = coord E ψ φ hφ ha (τ j) - (const 𝕜 E M a) ((eval 𝕜 E M a) (coord E ψ φ hφ ha (τ j)))) ∧ (∀ (j : Fin n), κ.pderiv j = Derivation.restrictScalars ℚ (coordDerivStalk E ψ φ hφ ha (τ j))) ∧ κ.IsLinearOver 𝕜 ∧ κ.SpansDerivations 𝕜

Regular coordinates of the stalk (exists_regularCoords_stalk) taken in a prescribed order τ of the chart coordinates (Kollár's order at a point of the centre): x_j = coord (τ j) − coord (τ j)(a), ∂_j = ∂_{τ j}, 𝕜-linear and spanning.

theorem Manifold.le_ordAlongIdeal_iteratedDeriv {𝕜 : 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] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) (I : IdealSheaf (structureSheaf 𝕜 E M)) {a : M} (ha : a ∈ Y) {m j : ℕ} (hj : j ≤ m) (hm : ↑m ≤ hY.idealSheaf.ordAlongIdeal I a) : ↑(m - j) ≤ hY.idealSheaf.ordAlongIdeal (I.iteratedDeriv j) a

At a point a of the closed submanifold Y, if I has order ≥ m along Y at a, then D^j(I) has order ≥ m − j along Y at a for j ≤ m ([Kol07, Lemma 74, (3)]; the step "(74.3)" in the proof of [Kol07, Corollary 77]).

theorem Manifold.le_ordAlongIdeal_deriv {𝕜 : 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] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) (I : IdealSheaf (structureSheaf 𝕜 E M)) {m : ℕ} (hm : ∀ a ∈ Y, ↑(m + 1) ≤ hY.idealSheaf.ordAlongIdeal I a) (a : M) : a ∈ Y → ↑m ≤ hY.idealSheaf.ordAlongIdeal I.deriv a

The order bookkeeping for one derivative: ord_Y I ≥ m + 1 gives ord_Y D(I) ≥ m.

theorem Manifold.birationalTransform_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] {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 π) {J : IdealSheaf (structureSheaf 𝕜 E M)} {k : ℕ} (hk : ∀ a ∈ Y, ↑k ≤ hY.idealSheaf.ordAlongIdeal J a) {a' : M'} (ha' : π a' ∉ Y) : (MarkedIdealSheaf.birationalTransform hY h { I := J, m := k }).I.stalkIdeal a' = (IdealSheaf.pullback π ⋯ J).stalkIdeal a'

Off the centre the marked transform is the total transform: the exceptional ideal sheaf is the unit ideal there and the colon by the unit ideal is the identity.

theorem Manifold.markedTransform_deriv_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] {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 π) (I : IdealSheaf (structureSheaf 𝕜 E M)) {m : ℕ} (hm : ∀ a ∈ Y, ↑(m + 1) ≤ hY.idealSheaf.ordAlongIdeal I a) : (MarkedIdealSheaf.birationalTransform hY h { I := I.deriv, m := m }).I ≤ (MarkedIdealSheaf.birationalTransform hY h { I := I, m := m + 1 }).I.deriv

For a blowing-up π with centre Y and ord_Y I ≥ m + 1 at every point of Y, π_*^{-1}(D(I), m) ⊆ D(π_*^{-1}(I, m + 1)) [Kol07, Theorem 76].

theorem Manifold.markedTransform_iteratedDeriv_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] {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 π) (I : IdealSheaf (structureSheaf 𝕜 E M)) {m : ℕ} (hm : ∀ a ∈ Y, ↑m ≤ hY.idealSheaf.ordAlongIdeal I a) {j : ℕ} (hj : j ≤ m) : (MarkedIdealSheaf.birationalTransform hY h { I := I.iteratedDeriv j, m := m - j }).I ≤ (MarkedIdealSheaf.birationalTransform hY h { I := I, m := m }).I.iteratedDeriv j

One blowing-up in [Kol07, Theorem 76] ("the rest follows by induction on j"), also [Wlo05, Lemma 2.6.3]; the form along a sequence of blowings-up is markedTransform_derivativeIter_le. For a blowing-up π with centre Y, ord_Y I ≥ m at every point of Y and j ≤ m, π_*^{-1}(D^j(I), m − j) ⊆ D^j(π_*^{-1}(I, m)).

theorem Manifold.idealSheaf_strictTransform_eq_markedTransform_one {𝕜 : 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 : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) {H : Set M} (hH : IsClosedSubmanifold ψ H 1) (hYH : Y ⊆ H) : ⋯.idealSheaf = (MarkedIdealSheaf.birationalTransform hY h { I := hH.idealSheaf, m := 1 }).I

For a blowing-up π with centre Y ⊆ H, H a smooth hypersurface, the strict transform H' is a smooth hypersurface of M' whose ideal sheaf is the marked transform of (I_H, 1) ([Wlo05, Lemma 2.7.4]; the proof of [Kol07, Theorem 80]).