Theorem 88 for one blow-up

[Kol07, Theorem 88] for a single smooth blow-up π : B_Z X → X with center Z ⊆ S, S a smooth hypersurface, ord_Z I ≥ m, s ≤ m: D^s π_*^{-1}(I, m) = ∑_{j ≤ s} D^{s−j}(−log S₁) π_*^{-1}(D^j I, m − j) (88.1). Kollár proves this case in a local chart; the induction along a sequence is in Hironaka/Resolution/Algebraic/Kol07/Theorem88Sequence.lean.

• ⊇ is the coordinate-free inclusion of Hironaka/Scheme/BlowUpSequence/Theorem88Basic.lean for one blow-up (Theorem 76 and D(−log S₁) ⊆ D).
• ⊆ is checked at the closed points q of B_Z X (le_of_forall_stalkIdeal_le_of_isClosed; B_Z X is Jacobson, being locally of finite type over k). Off the center the two sides are the transported D^s I_z (stalkIdeal_derivativeIter_markedTransform_of_notMem, the j = s summand). Over the center, at z = π(q): κ(z) is algebraic (isAlgebraic_residueField_π_of_isClosed), so dim 𝒪_{X,z} = n and the flag coordinates x_0, …, x_{n−1} (exists_flagCoords: a regular system of parameters whose first member is the equation of S and whose first r members generate Z) have n members; the chart description of the stalk with these coordinates (exists_stalk_equiv_localization_chart_of_chartCenter) puts q in the chart of some x_j, j ≤ r. If j = 0 (the chart of the equation of S) the strict transform misses q (Hironaka/Resolution/Algebraic/Kol07/Theorem88Chart.lean) and (88.1) at q is its j = 0 summand. Otherwise, with the coordinates reindexed so that the pivot is the last center coordinate and x_0 stays first: the stalks of the marked transforms are the images of the chart transforms transformIdeal (stalkIdeal_markedTransform_eq_map_transformIdeal); the derivative ideals of the stalk are computed by the chart derivations, which generate Der_k(𝒪_{B,q}) at the closed point q (derivativeIter_map_le_map_iterate_chartD, from forall_derivation_eq_sum_of_isClosed); iterate_chartD_transformIdeal_le gives the chart-level inclusion, Kollár's formula (88.2); the chart logarithmic derivations are logarithmic along the strict transform's chart ideal (x_r y_0)^{sat} (chartDlogpow_le_logDerivativeIter), whose image is (S₁)_q (stalkIdeal_strictTransform_eq_map_span_colon), and D(−log) is transported through the localization and the isomorphism e (map_logDerivativeIter_le); finally the coordinate derivatives c.Dpow j I_z lie in the full D^j I_z (Dpow_le_derivativeIter, k-linear coordinates).

theorem Derivation.mem_map_sup_span_image {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing k] [CommRing A] [CommRing B] [Algebra k B] (δ : Derivation k B B) (φ : A →+* B) (J : Ideal A) {z : B} (hz : z ∈ Ideal.map φ J) : δ z ∈ Ideal.map φ J ⊔ Ideal.span (⇑δ '' ⇑φ '' ↑J)

Leibniz on the generators of an image ideal: δ (J B) ⊆ J B + span (δ (φ J)).

theorem Ideal.derivativeIter_map_ringEquiv {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing k] [CommRing A] [CommRing B] [Algebra k A] [Algebra k B] (e : A ≃+* B) (hk : ∀ (a : k), e ((algebraMap k A) a) = (algebraMap k B) a) (s : ℕ) (J : Ideal A) : map e.toRingHom (derivativeIter k s J) = derivativeIter k s (map e.toRingHom J)

The iterated derivative ideal is transported by a ring isomorphism respecting the k-structures (derivative_map_ringEquiv, iterated).

theorem Ideal.colon_span_singleton_pow_mul_eq {A : Type u_4} [CommRing A] [IsDomain A] {a : A} (ha : a ≠ 0) (c : ℕ) (T : Ideal A) : Submodule.colon (span {a ^ c} * T) ↑(span {a} ^ c) = T

Cancelling a power of a nonzerodivisor, ((aᶜ) T : (a)ᶜ) = T in a domain: a corollary of Ideal.colon_span_pow_mul_self (Hironaka/Algebra/ColonPow.lean; the colon by the ideal (a)ᶜ is the colon by {aᶜ}).

theorem Ideal.map_logDerivativeIter_le {k : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing k] [CommRing A] [CommRing B] [Algebra k A] [Algebra k B] {C : Type u_4} [CommRing C] [Algebra k C] [Algebra A B] [IsScalarTower k A B] (M : Submonoid A) [IsLocalization M B] (e : B ≃+* C) (hk : ∀ (a : k), e ((algebraMap k B) a) = (algebraMap k C) a) (J : Ideal A) (t : ℕ) (K : Ideal A) : map (e.toRingHom.comp (algebraMap A B)) (logDerivativeIter k J t K) ≤ logDerivativeIter k (map (e.toRingHom.comp (algebraMap A B)) J) t (map (e.toRingHom.comp (algebraMap A B)) K)

D(−log) through a localization followed by a ring isomorphism respecting the k-structures, iterated: (D^t(−log J) K) C ⊆ D^t(−log J C)(K C).

theorem Hironaka.Sequence.isAlgebraic_residueField_π_of_isClosed {k : Type u} [Field k] [CharZero k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (Z : X.IdealSheafData) [AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp Z.subschemeι f)] (q : ↥Z.blowUp) (hq : IsClosed {q}) : Algebra.IsAlgebraic k (IsLocalRing.ResidueField ↑(X.presheaf.stalk (Z.blowUpπ q)))

The residue field of z = π(q) is algebraic over k when q is a closed point of B_Z X: κ(z) ↪ κ(q) over k, and κ(q) is algebraic (trdeg_residueField_stalk_eq_zero_of_isClosed).

theorem Hironaka.Sequence.ringKrullDim_stalk_π_eq_of_isClosed {k : Type u} [Field k] [CharZero k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (Z : X.IdealSheafData) [AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp Z.subschemeι f)] (q : ↥Z.blowUp) (hq : IsClosed {q}) : ringKrullDim ↑(X.presheaf.stalk (Z.blowUpπ q)) = ↑n

At z = π(q), q closed, dim 𝒪_{X,z} = n.

theorem Hironaka.Sequence.derivativeIter_map_le_map_iterate_chartD {k : Type u} [Field k] [CharZero k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (Z : X.IdealSheafData) [AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp Z.subschemeι f)] {R : Type u} [CommRing R] [IsRegularLocalRing R] [Algebra k R] [Algebra ℚ R] (q : ↥Z.blowUp) (hq : IsClosed {q}) (c : IsLocalRing.RegularCoords R n) (hk : c.IsLinearOver k) (ρ : Fin n) (𝔮 : Ideal ↥(IsLocalRing.chartRing c.x ρ)) [𝔮.IsPrime] (e : ↑(Z.blowUp.presheaf.stalk q) ≃+* Localization.AtPrime 𝔮) (hk' : ∀ (a : k), e.symm ((algebraMap k (Localization.AtPrime 𝔮)) a) = (algebraMap k ↑(Z.blowUp.presheaf.stalk q)) a) (T : Ideal ↥(IsLocalRing.chartRing c.x ρ)) (s : ℕ) : Ideal.derivativeIter k s (Ideal.map (e.symm.toRingHom.comp (algebraMap (↥(IsLocalRing.chartRing c.x ρ)) (Localization.AtPrime 𝔮))) T) ≤ Ideal.map (e.symm.toRingHom.comp (algebraMap (↥(IsLocalRing.chartRing c.x ρ)) (Localization.AtPrime 𝔮))) ((c.chartD ρ)^[s] T)

At a closed point q of B_Z X identified with a localization of the chart ring R' = R[c.x_i / c.x_ρ] of k-linear coordinates c (the chart isomorphism e, respecting the k-structures), the derivative ideal of the stalk is computed by the chart derivations: D^s(T 𝒪_{B,q}) ⊆ (D'^s T) 𝒪_{B,q}. The chart derivations, localized and transported along e, are dual to the transported chart coordinates, so they generate Der_k(𝒪_{B,q}) (forall_derivation_eq_sum_of_isClosed), and Leibniz on the generators finishes.

theorem Hironaka.Sequence.stalkIdeal_markedTransform_eq_map_transformIdeal {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (Z K : X.IdealSheafData) (c : ℕ) (q : ↥Z.blowUp) {n' : ℕ} (y : Fin n' → ↑(X.presheaf.stalk (Z.blowUpπ q))) (ρ : Fin n') (hn' : ↑n' = ringKrullDim ↑(X.presheaf.stalk (Z.blowUpπ q))) (hy : IsLocalRing.maximalIdeal ↑(X.presheaf.stalk (Z.blowUpπ q)) = Ideal.span (Set.range y)) (hZ' : Z.stalkIdeal (Z.blowUpπ q) = IsLocalRing.chartCenter y ρ) (𝔮 : Ideal ↥(IsLocalRing.chartRing y ρ)) [𝔮.IsPrime] (e : ↑(Z.blowUp.presheaf.stalk q) ≃+* Localization.AtPrime 𝔮) (he : ∀ (a : ↑(X.presheaf.stalk (Z.blowUpπ q))), e ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap Z.blowUpπ q)) a) = (algebraMap (↥(IsLocalRing.chartRing y ρ)) (Localization.AtPrime 𝔮)) ((algebraMap ↑(X.presheaf.stalk (Z.blowUpπ q)) ↥(IsLocalRing.chartRing y ρ)) a)) (hK : K.stalkIdeal (Z.blowUpπ q) ≤ IsLocalRing.chartCenter y ρ ^ c) : (K.markedTransform Z c).stalkIdeal q = Ideal.map (e.symm.toRingHom.comp (algebraMap (↥(IsLocalRing.chartRing y ρ)) (Localization.AtPrime 𝔮))) (IsLocalRing.transformIdeal y ρ (K.stalkIdeal (Z.blowUpπ q)) c)

Over the center, in the chart data at q: the stalk of π_*^{-1}(K, c) is the image under ψ' = e⁻¹ ∘ (R' → R'_𝔮) of the chart transform transformIdeal (for K_z ⊆ P^c): the colon formula stalkIdeal_markedTransform_of_chart and x_r^c · π_*^{-1}(K_z, c) = K_z R', the power of the nonzerodivisor π^♯ y_ρ cancelled.

theorem Hironaka.Sequence.stalkIdeal_strictTransform_eq_map_span_colon {X : AlgebraicGeometry.Scheme} (Z : X.IdealSheafData) (q : ↥Z.blowUp) {n' : ℕ} (y : Fin n' → ↑(X.presheaf.stalk (Z.blowUpπ q))) (ρ : Fin n') (hZ' : Z.stalkIdeal (Z.blowUpπ q) = IsLocalRing.chartCenter y ρ) (𝔮 : Ideal ↥(IsLocalRing.chartRing y ρ)) [𝔮.IsPrime] (e : ↑(Z.blowUp.presheaf.stalk q) ≃+* Localization.AtPrime 𝔮) (he : ∀ (a : ↑(X.presheaf.stalk (Z.blowUpπ q))), e ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap Z.blowUpπ q)) a) = (algebraMap (↥(IsLocalRing.chartRing y ρ)) (Localization.AtPrime 𝔮)) ((algebraMap ↑(X.presheaf.stalk (Z.blowUpπ q)) ↥(IsLocalRing.chartRing y ρ)) a)) (S : X.IdealSheafData) {g : ↑(X.presheaf.stalk (Z.blowUpπ q))} (hSz : S.stalkIdeal (Z.blowUpπ q) = Ideal.span {g}) : (S.strictTransform Z).stalkIdeal q = Ideal.map (e.symm.toRingHom.comp (algebraMap (↥(IsLocalRing.chartRing y ρ)) (Localization.AtPrime 𝔮))) (⨆ (i : ℕ), Submodule.colon (Ideal.span {(algebraMap ↑(X.presheaf.stalk (Z.blowUpπ q)) ↥(IsLocalRing.chartRing y ρ)) g}) ↑(Ideal.span {(algebraMap ↑(X.presheaf.stalk (Z.blowUpπ q)) ↥(IsLocalRing.chartRing y ρ)) (y ρ)} ^ i))

The stalk of the strict transform in the chart data: for S_z = (g), (S₁)_q is the image under ψ' of the y_ρ-saturation ⋃ᵢ ((φ g) : y_ρⁱ) of the total transform (φ g) R'.

Off the center

theorem Hironaka.Sequence.stalkIdeal_derivativeIter_markedTransform_of_notMem {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (Z I : X.IdealSheafData) (m s : ℕ) (q : ↥Z.blowUp) (hq : Z.blowUpπ q ∉ Z.support) : Ideal.derivativeIter k s ((I.markedTransform Z m).stalkIdeal q) = ((AlgebraicGeometry.Scheme.IdealSheafData.derivativeIter f s I).markedTransform Z (m - s)).stalkIdeal q

Off the center the marked transforms are total transforms along the isomorphism π^♯, and D^s π_*^{-1}(I, m) = π_*^{-1}(D^s I, m − s) there: (88.1)'s left side is its j = s summand.

Theorem 88 for one blow-up

theorem Hironaka.Sequence.derivativeIter_markedTransform_eq_iSup {k : Type u} [Field k] [CharZero k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (Z : X.IdealSheafData) [AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp Z.subschemeι f)] (S I : X.IdealSheafData) (hS : AlgebraicGeometry.IsSmoothDivisor S) {m : ℕ} (hZS : S ≤ Z) (hm : I.LeOrdAlong Z.support ↑m) {s : ℕ} (hs : s ≤ m) : AlgebraicGeometry.Scheme.IdealSheafData.derivativeIter (CategoryTheory.CategoryStruct.comp Z.blowUpπ f) s (I.markedTransform Z m) = ⨆ (j : ℕ), ⨆ (_ : j ≤ s), AlgebraicGeometry.Scheme.IdealSheafData.logDerivativeIter (CategoryTheory.CategoryStruct.comp Z.blowUpπ f) (S.strictTransform Z) (s - j) ((AlgebraicGeometry.Scheme.IdealSheafData.derivativeIter f j I).markedTransform Z (m - j))

[Kol07, Theorem 88] for one blow-up: for a smooth blow-up with center Z ⊆ S, S a smooth hypersurface, ord_Z I ≥ m and s ≤ m, D^s π_*^{-1}(I, m) = ∑_{j ≤ s} D^{s−j}(−log S₁) π_*^{-1}(D^j I, m − j).