Logarithmic derivatives along a blow-up sequence: Kollár's (87.3), Theorem 88 and Corollary 89

For a smooth hypersurface S and a sequence Π of blowings-up of order ≥ m for (I, m) whose centres lie in the strict transforms S_i of S, the logarithmic derivatives D(−log S_i) (the derivations preserving the ideal of S_i, [Kol07, 87]) interact with the marked transforms as follows:

• markedTransformSeq_logDerivIter_le: the inclusion (87.3) of [Kol07, 87] along the sequence, Π_*^{-1}(D^j(−log S)(I), m − j) ⊆ D^j(−log S_i)(Π_*^{-1}(I, m)), by induction on the stage with the one-blowing-up inclusion (birationalTransform_logDerivIter_le) and the monotonicity of the marked transform, as Kollár's Theorem 76 is iterated in Hironaka/Manifold/FiniteSuccession/DerivTransform.lean;
• iteratedDeriv_markedTransformSeq_eq_sum: Theorem 88 [Kol07, Theorem 88] along the sequence, D^s(Π_*^{-1}(I, m)) = ∑_{j=0}^{s} D^{s−j}(−log S_r)(Π_*^{-1}(D^j I, m − j)), by Kollár's induction on the number of blowings-up: at the stage i + 1 the one-blowing-up formula for π_i expresses D^s(Π_{i+1}) by the D^{s−j}(−log S_{i+1})(π_{i*}^{-1}(D^j Π_i, m − j)); the induction hypothesis writes D^j Π_i as a sum, the marked transform of a sum is the sum of the marked transforms, each π_{i*}^{-1}(D^{j−l}(−log S_i)(·), m − j) lies in D^{j−l}(−log S_{i+1})(π_{i*}^{-1}(·, m − l)) by (87.3), and D^{s−j}(−log S_{i+1}) D^{j−l}(−log S_{i+1}) = D^{s−l}(−log S_{i+1}) collapses the double sum; the reverse inclusion is Theorem 76 with the containment D^t(−log S) ⊆ D^t. A prefix-bounded form (iteratedDeriv_markedTransformSeq_eq_sum_of_forall_lt) assumes the order clause only at the stages before the one considered;
• cosupp_markedTransformSeq_inter_eq_iInter: Corollary 89 [Kol07, Corollary 89], S_r ∩ cosupp(Π_*^{-1}(I, m), m) = ⋂_{j<m} cosupp((Π|_{S_r})_*^{-1}((D^j I)|_S, m − j), m − j): Theorem 88 at s = m − 1 restricted to S_r through (87.1) (restriction carries D(−log S) to D) and the restriction of the marked transforms to the strict transforms (markedTransformSeq_pullback_restrictIncl, Kollár's Lemma 62 along the sequence), read through cosupp(I, m) = cosupp(D^{m−1}(I), 1) [Kol07, Lemma 74 (3)] on both sides, with the cosupport of a restriction the preimage of the cosupport and the cosupport of a finite sum the intersection of the cosupports (the stalks being local rings).

Corollary 89 is the identity by which the going-up theorem [Kol07, Theorem 84] recognizes the points of order ≥ m on a hypersurface of maximal contact.

Finite sums of ideals and of ideal sheaves

theorem Ideal.finset_sup_eq_top_iff_of_isLocalRing {R : Type u_1} [CommRing R] [IsLocalRing R] {ι : Type u_2} (F : Finset ι) (f : ι → Ideal R) : F.sup f = ⊤ ↔ ∃ j ∈ F, f j = ⊤

In a local ring a finite sup of ideals is the unit ideal iff one of them is (the stalk form of "the cosupport of a sum is the intersection of the cosupports", property (4) of the cosupport in [Kol07, Definition 59]).

theorem Manifold.IdealSheaf.finset_sum_le {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} {ι : Type u_1} {F : Finset ι} {G : ι → IdealSheaf 𝒪} {K : IdealSheaf 𝒪} (h : ∀ j ∈ F, G j ≤ K) : ∑ i ∈ F, G i ≤ K

A finite sum of ideal sheaves lies in K when every summand does (the sum of ideal sheaves is the stalkwise sup; the summands lie in the sum by Mathlib's Finset.single_le_sum).

theorem Manifold.IdealSheaf.one_le_ord_iff_mem_support {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} [∀ (x : ↑X), IsLocalRing ↑(𝒪.presheaf.stalk x)] (J : IdealSheaf 𝒪) (x : ↑X) : 1 ≤ J.ord x ↔ x ∈ J.support

1 ≤ ord_x J iff x lies in the cosupport of J.

theorem Manifold.IdealSheaf.mem_support_finset_sum_iff {X : TopCat} {𝒪 : TopCat.Sheaf CommRingCat X} [∀ (x : ↑X), IsLocalRing ↑(𝒪.presheaf.stalk x)] {ι : Type u_1} (F : Finset ι) (G : ι → IdealSheaf 𝒪) (x : ↑X) : x ∈ (∑ i ∈ F, G i).support ↔ ∀ j ∈ F, x ∈ (G j).support

The cosupport of a finite sum is the intersection of the cosupports (property (4) of the cosupport in [Kol07, Definition 59]), read at a point: the stalks are local rings.

The logarithmic derivative of a finite sum; pull-backs of finite sums

theorem Manifold.IdealSheaf.logDerivIter_finset_sum_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] {S : Set M} (hS : IsClosedSubmanifold ψ S 1) {ι : Type u_2} (F : Finset ι) (G : ι → IdealSheaf (structureSheaf 𝕜 E M)) (t : ℕ) : logDerivIter E ψ hS t (∑ i ∈ F, G i) ≤ ∑ i ∈ F, logDerivIter E ψ hS t (G i)

D^t(−log S) of a finite sum lies in the sum of the D^t(−log S)s (Ideal.logDerivativeIter_iSup_le, stalkwise).

theorem Manifold.IdealSheaf.le_ord_iff_one_le_ord_iteratedDeriv {𝕜 : 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 : IdealSheaf (structureSheaf 𝕜 E M)) {m : ℕ} (hm : 1 ≤ m) (a : M) : ↑m ≤ J.ord a ↔ 1 ≤ (J.iteratedDeriv (m - 1)).ord a

cosupp(I, m) = cosupp(D^{m−1}(I), 1) [Kol07, Lemma 74 (3)] at the level of orders: ord_a J ≥ m iff ord_a D^{m−1} J ≥ 1, for 1 ≤ m.

theorem Manifold.IdealSheaf.pullback_finset_sum {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {E' : Type u_2} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {N : Type u} [TopologicalSpace N] [ChartedSpace E' N] (φ : N → M) (hφ : ContMDiff (modelWithCornersSelf 𝕜 E') (modelWithCornersSelf 𝕜 E) ⊤ φ) {ι : Type u_3} (F : Finset ι) (G : ι → IdealSheaf (structureSheaf 𝕜 E M)) : pullback φ hφ (∑ i ∈ F, G i) = ∑ i ∈ F, pullback φ hφ (G i)

Pull-back commutes with finite sums.

Along a succession

theorem AnalyticManifold.FiniteSuccession.le_ordAlong_congr_chart_of_le_ordAlong {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) {I : M.IdealSheaf} {m : ℕ} (i : Fin B.length) (h4 : ∀ a ∈ Manifold.IdealSheaf.support (B.center i), ↑m ≤ Manifold.IdealSheaf.ordAlongIdeal (B.center i) (B.markedTransformSeq I m i.castSucc) a) (a : ↑↧(M.finStages B.later i.castSucc).carrier) : a ∈ Manifold.IdealSheaf.support (B.center i) → ↑m ≤ ⋯.idealSheaf.ordAlongIdeal (B.markedTransformSeq I m i.castSucc) a

The order clause (4′) of [Kol07, Definition 66] at a stage, for the centre read in the chart ψ.

theorem AnalyticManifold.FiniteSuccession.IsOfOrderGe.le_ordAlong_congr_chart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) {I E₀ : M.IdealSheaf} {m : ℕ} (hge : B.IsOfOrderGe I m E₀) (i : Fin B.length) (a : ↑↧(M.finStages B.later i.castSucc).carrier) : a ∈ Manifold.IdealSheaf.support (B.center i) → ↑m ≤ ⋯.idealSheaf.ordAlongIdeal (B.markedTransformSeq I m i.castSucc) a

The order hypothesis of [Kol07, Definition 66] at a stage, for the centre read in the chart ψ (le_ordAlong_congr_chart_of_le_ordAlong with the order clause (4′) of hge).

theorem AnalyticManifold.FiniteSuccession.birationalTransform_step_congr_chart {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) (i : Fin B.length) (J : (B.stage i.castSucc).IdealSheaf) (k : ℕ) : (Manifold.MarkedIdealSheaf.birationalTransform ⋯ ⋯ { I := J, m := k }).I = (Manifold.MarkedIdealSheaf.birationalTransform ⋯ ⋯ { I := J, m := k }).I

The marked transform at a step, with the centre read in the chart ψ (MarkedIdealSheaf.birationalTransform_congr).

theorem AnalyticManifold.FiniteSuccession.markedTransformSeq_logDerivIter_le {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold ψ S 1) (hc : B.CentersIn S) {I E₀ : M.IdealSheaf} {m : ℕ} (hge : B.IsOfOrderGe I m E₀) {j : ℕ} (hj : j ≤ m) (i : Fin (B.length + 1)) : B.markedTransformSeq (Manifold.IdealSheaf.logDerivIter E ψ hS j I) (m - j) i ≤ Manifold.IdealSheaf.logDerivIter E ψ ⋯ j (B.markedTransformSeq I m i)

The inclusion (87.3) of [Kol07, 87] along a sequence: for Π of order ≥ m for (I, m) whose centres lie in the strict transforms S_i of the hypersurface S, and j ≤ m, Π_*^{-1}(D^j(−log S)(I), m − j) ⊆ D^j(−log S_i)(Π_*^{-1}(I, m)) at every stage i. The algebraic counterpart is markedTransformSeq_logDerivativeIter_le.

theorem AnalyticManifold.FiniteSuccession.iteratedDeriv_markedTransformSeq_eq_sum_of_forall_lt {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold ψ S 1) (hc : B.CentersIn S) {I : M.IdealSheaf} {m s : ℕ} (hs : s ≤ m) (i : Fin (B.length + 1)) (h4 : ∀ (i' : Fin B.length), ↑i' < ↑i → ∀ a ∈ Manifold.IdealSheaf.support (B.center i'), ↑m ≤ Manifold.IdealSheaf.ordAlongIdeal (B.center i') (B.markedTransformSeq I m i'.castSucc) a) : Manifold.IdealSheaf.iteratedDeriv (B.markedTransformSeq I m i) s = ∑ j ∈ Finset.range (s + 1), Manifold.IdealSheaf.logDerivIter E ψ ⋯ (s - j) (B.markedTransformSeq (Manifold.IdealSheaf.iteratedDeriv I j) (m - j) i)

Theorem 88 [Kol07, Theorem 88] along a sequence, in prefix-bounded form: for Π whose centres lie in the strict transforms S_i of the hypersurface S, a stage i such that the marked transforms of (I, m) have order ≥ m along the centres of the steps before i (the order clause (4′) on the prefix, with no normal-crossings clause), and s ≤ m, D^s(Π_*^{-1}(I, m)) = ∑_{j=0}^{s} D^{s−j}(−log S_i)(Π_*^{-1}(D^j I, m − j)) at the stage i. Kollár's induction on the number of blowings-up; the step from i to i + 1 uses (4′) at the step i only, through the prefix-bounded form of Corollary 77.

theorem AnalyticManifold.FiniteSuccession.iteratedDeriv_markedTransformSeq_eq_sum {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold ψ S 1) (hc : B.CentersIn S) {I E₀ : M.IdealSheaf} {m : ℕ} (hge : B.IsOfOrderGe I m E₀) {s : ℕ} (hs : s ≤ m) (i : Fin (B.length + 1)) : Manifold.IdealSheaf.iteratedDeriv (B.markedTransformSeq I m i) s = ∑ j ∈ Finset.range (s + 1), Manifold.IdealSheaf.logDerivIter E ψ ⋯ (s - j) (B.markedTransformSeq (Manifold.IdealSheaf.iteratedDeriv I j) (m - j) i)

Theorem 88 [Kol07, Theorem 88] along a sequence: for Π of order ≥ m for (I, m) whose centres lie in the strict transforms S_i of the hypersurface S, and s ≤ m, D^s(Π_*^{-1}(I, m)) = ∑_{j=0}^{s} D^{s−j}(−log S_i)(Π_*^{-1}(D^j I, m − j)) at every stage i (iteratedDeriv_markedTransformSeq_eq_sum_of_forall_lt with the order clause (4′) of hge). The algebraic counterpart is derivativeIter_markedTransformSeq_eq_iSup.

theorem AnalyticManifold.FiniteSuccession.logDerivIter_pullback_restrictIncl {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold ψ S 1) (hc : B.CentersIn S) (i : Fin (B.length + 1)) (r : ℕ) (J : (B.stage i).IdealSheaf) : Manifold.IdealSheaf.pullback ⇑(B.restrictIncl hS hc i) ⋯ (Manifold.IdealSheaf.logDerivIter E ψ ⋯ r J) = (Manifold.IdealSheaf.pullback ⇑(B.restrictIncl hS hc i) ⋯ J).iteratedDeriv r

The identity (87.1) of [Kol07, 87] along the inclusions S_i ↪ X_i of the restricted sequence: the restriction of D^r(−log S_i)(J) to S_i is the r-th derivative of the restriction.

theorem AnalyticManifold.FiniteSuccession.cosupp_markedTransformSeq_inter_eq_iInter {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} [FiniteDimensional 𝕜 E] {M : AnalyticManifold 𝕜 E} (B : M.FiniteSuccession) {S : Set M.carrier} (hS : Manifold.IsClosedSubmanifold ψ S 1) (hc : B.CentersIn S) {I E₀ : M.IdealSheaf} {m : ℕ} (hge : B.IsOfOrderGe I m E₀) (hm : 1 ≤ m) : ⇑(B.restrictIncl hS hc (Fin.last B.length)) ⁻¹' {x : (B.stage (Fin.last B.length)).carrier | ↑m ≤ Manifold.IdealSheaf.ord (B.markedTransformSeq I m (Fin.last B.length)) x} = ⋂ (j : ℕ), ⋂ (_ : j < m), {y : ↑↧((B.restrictSubmanifold hS hc).stage (Fin.last B.length)).carrier | ↑(m - j) ≤ Manifold.IdealSheaf.ord ((B.restrictSubmanifold hS hc).markedTransformSeq (Manifold.IdealSheaf.pullback ⇑hS.inclusionMap ⋯ (Manifold.IdealSheaf.iteratedDeriv I j)) (m - j) (Fin.last B.length)) y}

Corollary 89 [Kol07, Corollary 89]: with the assumptions of Theorem 88 and 1 ≤ m, on the last strict transform S_r (read as the preimage under its embedding into the last stage), S_r ∩ cosupp(Π_*^{-1}(I, m), m) = ⋂_{j<m} cosupp((Π|_{S_r})_*^{-1}((D^j I)|_S, m − j), m − j). The algebraic counterpart carries the same name.