Properties of the logarithmic derivative ideal sheaves

Properties of logarithmic derivations from [Kol07, 87]: the inclusions I ⊂ D(−log S)(I) ⊂ D(I) and the second of Kollár's three properties, (87.2) — the filtration D^s(−log S)(I) ⊂ D^{s−1}(−log S)(D(I)) ⊂ ⋯ ⊂ D^s(I) and, in local coordinates, the decomposition D^s(I) = D^s(−log S)(I) + D^{s−1}(−log S)(∂I/∂x₁) + ⋯ + (∂^s I/∂x₁^s) whose first j + 1 summands span D^{s−j}(−log S)(D^j(I)). (The first property, (87.1), the restriction to S, is Hironaka/Manifold/IdealSheaf/LogDerivRestrict.lean; the third, the transform under blow-ups, is in Hironaka/Manifold/BlowUp/Transform/.) Everything is stalkwise through stalkIdeal_logDeriv and the Hironaka library's lemmas on Ideal.logDerivative; the composition rule D^a(−log S)(D^b(−log S)(J)) = D^{a+b}(−log S)(J) is the iterate law; off S the logarithmic derivative is the plain derivative (Ideal.logDerivative_top); at a point of S with regular coordinates of the stalk whose distinguished coordinate x_h generates (I_S)_a, the stalk of D^r(−log S)(J) is the Hironaka library's Dlogpow h r J_a (logDerivative_eq_Dlog), and the decomposition (87.2) is Dlogpow_Dpow_eq_iSup read through stalkIdeal_iteratedDeriv_eq_Dpow. These are the properties used to transform the derivative ideals under a blow-up with centre inside S (Hironaka/Manifold/BlowUp/Transform/LogDerivBlowUp.lean).

theorem Manifold.IdealSheaf.le_logDeriv {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {S : Set M} (hS : IsClosedSubmanifold ψ S 1) (J : IdealSheaf (structureSheaf 𝕜 E M)) : J ≤ logDeriv E ψ hS J

I ⊂ D(−log S)(I) [Kol07, 87].

theorem Manifold.IdealSheaf.logDeriv_mono {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {S : Set M} (hS : IsClosedSubmanifold ψ S 1) {J K : IdealSheaf (structureSheaf 𝕜 E M)} (hJK : J ≤ K) : logDeriv E ψ hS J ≤ logDeriv E ψ hS K

D(−log S) is monotone.

theorem Manifold.IdealSheaf.logDerivIter_mono {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {S : Set M} (hS : IsClosedSubmanifold ψ S 1) (r : ℕ) {J K : IdealSheaf (structureSheaf 𝕜 E M)} (hJK : J ≤ K) : logDerivIter E ψ hS r J ≤ logDerivIter E ψ hS r K

The iterates are monotone.

theorem Manifold.IdealSheaf.logDerivIter_logDerivIter {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {S : Set M} (hS : IsClosedSubmanifold ψ S 1) (a b : ℕ) (J : IdealSheaf (structureSheaf 𝕜 E M)) : logDerivIter E ψ hS a (logDerivIter E ψ hS b J) = logDerivIter E ψ hS (a + b) J

The composition rule D^a(−log S)(D^b(−log S)(J)) = D^{a+b}(−log S)(J) (as used in the proof of [Kol07, Theorem 88]).

theorem Manifold.IdealSheaf.stalkIdeal_logDerivIter_of_notMem {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {S : Set M} (hS : IsClosedSubmanifold ψ S 1) [FiniteDimensional 𝕜 E] (r : ℕ) (J : IdealSheaf (structureSheaf 𝕜 E M)) {a : M} (ha : a ∉ S) : (logDerivIter E ψ hS r J).stalkIdeal a = (J.iteratedDeriv r).stalkIdeal a

Off S, D^r(−log S)(J) is D^r(J) stalk by stalk.

theorem Manifold.IdealSheaf.logDeriv_le_deriv {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {S : Set M} (hS : IsClosedSubmanifold ψ S 1) [FiniteDimensional 𝕜 E] (J : IdealSheaf (structureSheaf 𝕜 E M)) : logDeriv E ψ hS J ≤ J.deriv

D(−log S)(I) ⊂ D(I) [Kol07, 87].

theorem Manifold.IdealSheaf.logDerivIter_succ_le_logDerivIter_deriv {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {S : Set M} (hS : IsClosedSubmanifold ψ S 1) [FiniteDimensional 𝕜 E] (k : ℕ) (X : IdealSheaf (structureSheaf 𝕜 E M)) : logDerivIter E ψ hS (k + 1) X ≤ logDerivIter E ψ hS k X.deriv

One step of the filtration (87.2), in the form D^{k+1}(−log S)(X) ⊆ D^k(−log S)(D(X)).

theorem Manifold.IdealSheaf.logDerivIter_iteratedDeriv_le {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {S : Set M} (hS : IsClosedSubmanifold ψ S 1) [FiniteDimensional 𝕜 E] {s j : ℕ} (hj : j < s) (J : IdealSheaf (structureSheaf 𝕜 E M)) : logDerivIter E ψ hS (s - j) (J.iteratedDeriv j) ≤ logDerivIter E ψ hS (s - (j + 1)) (J.iteratedDeriv (j + 1))

One step of the filtration (87.2) [Kol07, 87]: for j < s, D^{s−j}(−log S)(D^j J) ⊆ D^{s−(j+1)}(−log S)(D^{j+1} J).

theorem Manifold.IdealSheaf.logDerivIter_le_iteratedDeriv {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {S : Set M} (hS : IsClosedSubmanifold ψ S 1) [FiniteDimensional 𝕜 E] (r : ℕ) (J : IdealSheaf (structureSheaf 𝕜 E M)) : logDerivIter E ψ hS r J ≤ J.iteratedDeriv r

The end of the filtration (87.2) [Kol07, 87]: D^r(−log S)(J) ⊆ D^r(J).

theorem Manifold.IdealSheaf.stalkIdeal_logDerivIter_eq_Dlogpow {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {S : Set M} (hS : IsClosedSubmanifold ψ S 1) [FiniteDimensional 𝕜 E] {a : M} (κ : IsLocalRing.RegularCoords (↑((structureSheaf 𝕜 E M).presheaf.stalk a)) n) (hk : κ.IsLinearOver 𝕜) (hs : κ.SpansDerivations 𝕜) (h : Fin n) (hSa : hS.idealSheaf.stalkIdeal a = Ideal.span {κ.x h}) (r : ℕ) (J : IdealSheaf (structureSheaf 𝕜 E M)) : (logDerivIter E ψ hS r J).stalkIdeal a = κ.Dlogpow h r (J.stalkIdeal a)

In coordinates: at a point a with regular coordinates κ of the stalk whose 𝕜-linear derivations span the 𝕜-derivations and with (I_S)_a = (κ.x h), (D^r(−log S)(J))_a = D^r(−log x_h)(J_a) (the Hironaka library's Dlogpow).

theorem Manifold.IdealSheaf.stalkIdeal_iteratedDeriv_eq_iSup_Dlogpow {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [FiniteDimensional 𝕜 E] {a : M} (κ : IsLocalRing.RegularCoords (↑((structureSheaf 𝕜 E M).presheaf.stalk a)) n) (hk : κ.IsLinearOver 𝕜) (hs : κ.SpansDerivations 𝕜) (h : Fin n) (s : ℕ) (J : IdealSheaf (structureSheaf 𝕜 E M)) : (J.iteratedDeriv s).stalkIdeal a = ⨆ (j : ℕ), ⨆ (_ : j ≤ s), κ.Dlogpow h (s - j) (κ.iterPderivIdeal h j (J.stalkIdeal a))

Kollár's decomposition (87.2) [Kol07, 87]: the decomposition of (D^s J)_a by the order of differentiation in the direction x_h — Dlogpow_Dpow_eq_iSup at j = s through stalkIdeal_iteratedDeriv_eq_Dpow.