Tools for the logarithmic derivative rule and Theorem 88 under a blowing-up

Bridges between the analytic stalks and the chart-level layer of the version for schemes, and one transport:

• stalkIdeal_logDerivIter: the stalk of D^r(−log S)(J) is the intrinsic iterate Ideal.logDerivativeIter 𝕜 (I_{S,a}) r J_a.
• logDerivativeIter_map_ringEquiv: the iterate of Ideal.logDerivative_map_ringEquiv (the logarithmic derivative is transported by a ring isomorphism respecting the 𝕜-structures, the preserving derivations conjugated along the isomorphism), hence the locality of D(−log S) at a point where the germ map is bijective (stalkIdeal_logDeriv_pullback_of_bijective), in particular off the centre of a blowing-up where the strict transform's ideal is the pull-back of I_S (stalkIdeal_idealSheaf_strictTransform_of_notMem, from I_{S'} = π_*^{-1}(I_S, 1)).
• exists_kollarChartData_of_mem_strictTransform: at a point a' of the strict transform S' over the centre, Kollár's good chart (the flag chart of Hironaka.Manifold.BlowUp.Transform.StrictFlag, a blow-up chart whose index is not the index of S, Kollár's permutation of the coordinates, regular coordinates and the chart-ring map χ) packaged with I_{S,π a'} = (x_{h₀}), I_{S',a'} = (χ y_{h₀}), h₀ < r, the rule (75.1) χ ∂'_j = ∂_{u_{τ j}} χ, the preservation of (χ y_{h₀}) by ∂_{u_{τ j}}, j ≠ h₀, the spanning of the 𝕜-derivations by the ∂_{u_{τ j}}, and the transform formula π_*^{-1}(I, m)_{a'} = χ(transformIdeal I_a m).

Sources: [Kol07, 87, (87.3)], [Kol07, 75], [Kol07, Lemma 74, (4)]; the good chart is the one in the proof of [Kol07, Theorem 88]. These tools are used in Hironaka.Manifold.BlowUp.Transform.LogDerivBlowUp.

The iterated logarithmic derivative under a ring isomorphism

theorem Ideal.logDerivativeIter_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) (J : Ideal A) (r : ℕ) (I : Ideal A) : map e.toRingHom (logDerivativeIter k J r I) = logDerivativeIter k (map e.toRingHom J) r (map e.toRingHom I)

The iterated form of Ideal.logDerivative_map_ringEquiv (Hironaka.Scheme.BlowUpSequence.TransformLogDerivative).

The intrinsic iterate on stalks

theorem Manifold.IdealSheaf.stalkIdeal_logDerivIter {𝕜 : 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) (r : ℕ) (J : IdealSheaf (structureSheaf 𝕜 E M)) (a : M) : (logDerivIter E ψ hS r J).stalkIdeal a = Ideal.logDerivativeIter 𝕜 (hS.idealSheaf.stalkIdeal a) r (J.stalkIdeal a)

The stalk of D^r(−log S)(J) is the intrinsic iterate D^r(−log I_{S,a})(J_a).

Locality of D(−log S) at a point where the germ map is bijective

theorem Manifold.stalkIdeal_logDeriv_pullback_of_bijective {𝕜 : 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} {N : Type u} [TopologicalSpace N] [ChartedSpace E N] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N] {S' : Set N} (φ : N → M) (hφ : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ φ) (hS : IsClosedSubmanifold ψ S 1) (hS' : IsClosedSubmanifold ψ S' 1) (J : IdealSheaf (structureSheaf 𝕜 E M)) {b : N} (hb : Function.Bijective ⇑(germMap φ hφ b)) (hI : hS'.idealSheaf.stalkIdeal b = Ideal.map (germMap φ hφ b) (hS.idealSheaf.stalkIdeal (φ b))) : (IdealSheaf.logDeriv E ψ hS' (IdealSheaf.pullback φ hφ J)).stalkIdeal b = (IdealSheaf.pullback φ hφ (IdealSheaf.logDeriv E ψ hS J)).stalkIdeal b

Locality of D(−log S) ([Kol07, Lemma 74, (4)] for the logarithmic derivative): at a point b where the germ map of φ is bijective and the ideal of S' is the pull-back of the ideal of S, the stalk of D(−log S')(φ^* J) is the stalk of φ^*(D(−log S)(J)).

theorem Manifold.stalkIdeal_logDerivIter_pullback_of_bijective {𝕜 : 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} {N : Type u} [TopologicalSpace N] [ChartedSpace E N] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N] {S' : Set N} (φ : N → M) (hφ : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ φ) (hS : IsClosedSubmanifold ψ S 1) (hS' : IsClosedSubmanifold ψ S' 1) (J : IdealSheaf (structureSheaf 𝕜 E M)) {b : N} (hb : Function.Bijective ⇑(germMap φ hφ b)) (hI : hS'.idealSheaf.stalkIdeal b = Ideal.map (germMap φ hφ b) (hS.idealSheaf.stalkIdeal (φ b))) (r : ℕ) : (IdealSheaf.logDerivIter E ψ hS' r (IdealSheaf.pullback φ hφ J)).stalkIdeal b = (IdealSheaf.pullback φ hφ (IdealSheaf.logDerivIter E ψ hS r J)).stalkIdeal b

The iterated form of stalkIdeal_logDeriv_pullback_of_bijective.

theorem Manifold.stalkIdeal_iteratedDeriv_pullback_of_bijective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {N : Type u} [TopologicalSpace N] [ChartedSpace E N] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ N] (φ : N → M) (hφ : ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E) ⊤ φ) [FiniteDimensional 𝕜 E] (J : IdealSheaf (structureSheaf 𝕜 E M)) {b : N} (hb : Function.Bijective ⇑(germMap φ hφ b)) (r : ℕ) : ((IdealSheaf.pullback φ hφ J).iteratedDeriv r).stalkIdeal b = (IdealSheaf.pullback φ hφ (J.iteratedDeriv r)).stalkIdeal b

The iterated form of stalkIdeal_deriv_pullback_of_bijective at one point (iteratedDeriv_pullback_of_isLocalDiffeomorph, pointwise).

The strict transform of the hypersurface S ⊇ Y under a blowing-up

theorem Manifold.IsClosedSubmanifold.one_le_ordAlongIdeal_idealSheaf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {S Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) (hS : IsClosedSubmanifold ψ S 1) (hYS : Y ⊆ S) (a : M) : a ∈ Y → ↑1 ≤ hY.idealSheaf.ordAlongIdeal hS.idealSheaf a

Definedness of the mark 1 on I_S along a centre Y ⊆ S: ord_Y I_S ≥ 1 at every point of Y.

theorem Manifold.stalkIdeal_idealSheaf_strictTransform_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] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {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) {a' : M'} (ha' : π a' ∉ Y) : hS'.idealSheaf.stalkIdeal a' = Ideal.map (germMap π ⋯ a') (hS.idealSheaf.stalkIdeal (π a'))

Off the centre the ideal sheaf of the strict transform S' is the pull-back of I_S (I_{S'} = π_*^{-1}(I_S, 1) and birationalTransform_stalkIdeal_of_notMem).

theorem Manifold.exists_kollarChartData_of_mem_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] {S : Set 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 π) (hS : IsClosedSubmanifold ψ S 1) (hYS : Y ⊆ S) (hS' : IsClosedSubmanifold ψ (strictTransformSet π Y S) 1) {a' : M'} (haS' : a' ∈ strictTransformSet π Y S) (haY : π a' ∈ Y) : ∃ (κ : IsLocalRing.RegularCoords (↑((structureSheaf 𝕜 E M).presheaf.stalk (π a'))) n) (r : Fin n) (h₀ : Fin n) (χ : ↥(IsLocalRing.chartRing κ.x r) →+* ↑((structureSheaf 𝕜 E M').presheaf.stalk a')) (δ : Fin n → Derivation 𝕜 ↑((structureSheaf 𝕜 E M').presheaf.stalk a') ↑((structureSheaf 𝕜 E M').presheaf.stalk a')), κ.IsLinearOver 𝕜 ∧ κ.SpansDerivations 𝕜 ∧ h₀ < r ∧ IsLocalRing.chartCenter κ.x r = hY.idealSheaf.stalkIdeal (π a') ∧ hS.idealSheaf.stalkIdeal (π a') = Ideal.span {κ.x h₀} ∧ hS'.idealSheaf.stalkIdeal a' = Ideal.span {χ (IsLocalRing.chartYR κ.x r h₀)} ∧ (∀ (j : Fin n) (g : ↥(IsLocalRing.chartRing κ.x r)), χ ((κ.chartDerivRing r j) g) = (δ j) (χ g)) ∧ (∀ (j : Fin n), j ≠ h₀ → (δ j).PreservesIdeal (Ideal.span {χ (IsLocalRing.chartYR κ.x r h₀)})) ∧ (∀ (D : Derivation 𝕜 ↑((structureSheaf 𝕜 E M').presheaf.stalk a') ↑((structureSheaf 𝕜 E M').presheaf.stalk a')) (f : ↑((structureSheaf 𝕜 E M').presheaf.stalk a')), ∃ (a : Fin n → ↑((structureSheaf 𝕜 E M').presheaf.stalk a')), D f = ∑ j : Fin n, a j * (δ j) f) ∧ ∀ (I : IdealSheaf (structureSheaf 𝕜 E M)) {m : ℕ}, (∀ a ∈ Y, ↑m ≤ hY.idealSheaf.ordAlongIdeal I a) → (MarkedIdealSheaf.birationalTransform hY h { I := I, m := m }).I.stalkIdeal a' = Ideal.map χ (IsLocalRing.transformIdeal κ.x r (I.stalkIdeal (π a')) m)

Kollár's good chart at a point a' of the strict transform S' over the centre (the proof of [Kol07, Theorem 88]: coordinates with S = (x₁ = 0), and the chart where the strict transform of S is (y₁ = 0)): regular coordinates κ of the stalk at π a' reindexed by Kollár's permutation (exists_kollarPerm) with pivot r, the index h₀ < r of the hypersurface coordinate (I_{S,π a'} = (κ.x h₀)), the chart-ring map χ with I_{S',a'} = (χ y_{h₀}), the coordinate derivations δ j = ∂_{u_{τ j}} of the stalk at a' with the (75.1) rule χ ∂'_j = δ j ∘ χ, preserving (χ y_{h₀}) for j ≠ h₀ and spanning the 𝕜-derivations, and the transform formula π_*^{-1}(I, m)_{a'} = χ(π_*^{-1}(I_a, m)) for every marked ideal sheaf of order ≥ m along Y.