The logarithmic derivative ideal sheaf D(−log S)(𝓘) along a hypersurface

Kollár's logarithmic derivatives along a smooth hypersurface S [Kol07, 87]: the sheaf Der_X(−log S) of derivations preserving the ideal of S, which in local coordinates with S = (x₁ = 0) is "Der_X(−log S) = ⟨x₁ ∂/∂x₁, ∂/∂x₂, …, ∂/∂xₙ⟩", and the logarithmic derivative D(−log S)(I) of an ideal sheaf, generated by I and the images of I under these derivations, with its iterates D^{r+1}(−log S)(I) := D(−log S)(D^r(−log S)(I)).

The definition is stalkwise and chart-free: the stalk of D(−log S)(J) at a is the Hironaka library's Ideal.logDerivative 𝕜 (I_{S,a}) J_a = J_a ⊔ ∑_δ ⟨δ J_a⟩ over the 𝕜-derivations δ of 𝒪_{M,a} preserving the stalk I_{S,a} of the reduced ideal sheaf of the hypersurface (IsClosedSubmanifold.idealSheaf, itself chart-independent). The family of stalks has local generators (so IdealSheaf.ofStalks applies, as for deriv): in a chart adapted to S with S = (x_h = 0), the derivations x_h ∂_h and ∂_j (j ≠ h) generate the preserving derivations at every point of the chart — at a point of S because a derivation is ∑_i δ(x_i − x_i(a)) ∂_i and δ(x_h) ∈ (x_h), at a point off S because x_h is a unit there and all derivations preserve the unit ideal — so on the chart the germs of the generators f_j of J, of x_h ∂_h f_j and of ∂_i f_j (i ≠ h) generate the stalks (Kollár's "D(f_1, …, f_s) = (f_i, ∂f_i/∂x_j)" with ∂_h weighted by x_h). The iterates D^r(−log S)(J) are logDerivIter. Their properties are in Hironaka/Manifold/IdealSheaf/LogDerivLemmas.lean and their restriction to S in Hironaka/Manifold/IdealSheaf/LogDerivRestrict.lean.

The algebraic span lemma for D(−log J)

theorem Ideal.logDerivative_span_eq_of_span {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] {ι : Type u_3} (der : ι → Derivation k A A) {J : Ideal A} (hder : ∀ (i : ι), (der i).PreservesIdeal J) (h : ∀ (δ : Derivation k A A), δ.PreservesIdeal J → δ ∈ Submodule.span A (Set.range der)) (S : Set A) : logDerivative k J (span S) = span (S ∪ ⋃ (i : ι), ⇑(der i) '' S)

Ideal.derivative_span_eq_of_span for the logarithmic derivative (Kollár's description of D(−log S) in coordinates, [Kol07, 87]): if the derivations der i preserve J and span (over A) the derivations preserving J, then D(−log J)(⟨S⟩) = ⟨S ∪ ⋃_i der i '' S⟩.

The coordinate logarithmic derivations x_h ∂_h, ∂_j (j ≠ h) at a point of a chart

noncomputable def Manifold.logCoordDerivStalk {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) (h i : Fin n) : Derivation 𝕜 ↑((structureSheaf 𝕜 E M).presheaf.stalk a) ↑((structureSheaf 𝕜 E M).presheaf.stalk a)

Kollár's generators of Der_X(−log S) in coordinates with S = (x_h = 0) [Kol07, 87]: the family i ↦ x_h ∂_h for i = h, ∂_i otherwise, on the stalk at a.

Equations

• Manifold.logCoordDerivStalk E ψ φ hφ ha h i = if i = h then Manifold.coord E ψ φ hφ ha h • Manifold.coordDerivStalk E ψ φ hφ ha h else Manifold.coordDerivStalk E ψ φ hφ ha i

theorem Manifold.logCoordDerivStalk_self {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) (h : Fin n) : logCoordDerivStalk E ψ φ hφ ha h h = coord E ψ φ hφ ha h • coordDerivStalk E ψ φ hφ ha h

theorem Manifold.logCoordDerivStalk_of_ne {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) {h i : Fin n} (hi : i ≠ h) : logCoordDerivStalk E ψ φ hφ ha h i = coordDerivStalk E ψ φ hφ ha i

theorem Manifold.logCoordDerivStalk_preservesIdeal {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) (h i : Fin n) : (logCoordDerivStalk E ψ φ hφ ha h i).PreservesIdeal (Ideal.span {coord E ψ φ hφ ha h})

Each x_h ∂_h, ∂_j (j ≠ h) preserves the ideal (x_h) [Kol07, 87].

theorem Manifold.mem_span_logCoordDerivStalk_of_preservesIdeal {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) (h : Fin n) (δ : Derivation 𝕜 ↑((structureSheaf 𝕜 E M).presheaf.stalk a) ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) (hδ : δ.PreservesIdeal (Ideal.span {coord E ψ φ hφ ha h})) : δ ∈ Submodule.span (↑((structureSheaf 𝕜 E M).presheaf.stalk a)) (Set.range (logCoordDerivStalk E ψ φ hφ ha h))

A derivation preserving (x_h) is an 𝒪_{M,a}-combination of x_h ∂_h and the ∂_j, j ≠ h ([Kol07, 87], from δ = ∑_i δ(x_i − x_i(a)) ∂_i).

theorem Manifold.logDerivative_span_coord_eq {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) (h : Fin n) (T : Set ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) : Ideal.logDerivative 𝕜 (Ideal.span {coord E ψ φ hφ ha h}) (Ideal.span T) = Ideal.span (T ∪ ⋃ (i : Fin n), ⇑(logCoordDerivStalk E ψ φ hφ ha h i) '' T)

On the stalk at a point where x_h = 0: D(−log (x_h))(⟨T⟩) = ⟨T ∪ x_h ∂_h T ∪ ⋃_{j ≠ h} ∂_j T⟩ ([Kol07, 87], in coordinates).

theorem Manifold.derivative_span_eq_span_logCoordDerivStalk {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) (h : Fin n) (hu : IsUnit (coord E ψ φ hφ ha h)) (T : Set ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) : Ideal.derivative 𝕜 (Ideal.span T) = Ideal.span (T ∪ ⋃ (i : Fin n), ⇑(logCoordDerivStalk E ψ φ hφ ha h i) '' T)

At a point where x_h is a unit (off the hypersurface), the same family generates the plain derivative: D(⟨T⟩) = ⟨T ∪ x_h ∂_h T ∪ ⋃_{j ≠ h} ∂_j T⟩.

The section-level family and the local generators

noncomputable def Manifold.logCoordDerivSection {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (V : TopologicalSpace.Opens M) (hV : ↑V ⊆ φ.source) (h i : Fin n) (f : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))) : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))

The section-level family f ↦ x_h · ∂_h f (i = h), f ↦ ∂_i f (i ≠ h) over V.

Equations

• Manifold.logCoordDerivSection E ψ φ hφ V hV h i f = if i = h then Manifold.coordSection E ψ φ hφ V hV h * (Manifold.coordDeriv E ψ φ hφ V hV h) f else (Manifold.coordDeriv E ψ φ hφ V hV i) f

theorem Manifold.germ_logCoordDerivSection {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (V : TopologicalSpace.Opens M) (hV : ↑V ⊆ φ.source) {b : M} (hb : b ∈ V) (h i : Fin n) (f : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))) : (CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ V b hb)) (logCoordDerivSection E ψ φ hφ V hV h i f) = (logCoordDerivStalk E ψ φ hφ ⋯ h i) ((CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ V b hb)) f)

The germ of logCoordDerivSection is logCoordDerivStalk of the germ.

theorem Manifold.logDerivative_stalkIdeal_eq_span {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (V : TopologicalSpace.Opens M) (hV : ↑V ⊆ φ.source) {S : Set M} (hS : IsClosedSubmanifold ψ S 1) {σ : Fin 1 ↪ Fin n} (hφS : IsAdaptedChart ψ S φ σ) (J : IdealSheaf (structureSheaf 𝕜 E M)) {U : TopologicalSpace.Opens M} {k : ℕ} (f : Fin k → ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op U))) (hf : ∀ (b : M) (hb : b ∈ U), J.stalkIdeal b = Ideal.span (Set.range fun (j : Fin k) => (CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ U b hb)) (f j))) (hVU : V ≤ U) {b : M} (hb : b ∈ V) : Ideal.logDerivative 𝕜 (hS.idealSheaf.stalkIdeal b) (J.stalkIdeal b) = Ideal.span ((Set.range fun (j : Fin k) => (CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ V b hb)) ((CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.map (CategoryTheory.homOfLE hVU).op)) (f j))) ∪ ⋃ (i : Fin n), Set.range fun (j : Fin k) => (CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.germ V b hb)) (logCoordDerivSection E ψ φ hφ V hV (σ 0) i ((CategoryTheory.ConcreteCategory.hom ((structureSheaf 𝕜 E M).presheaf.map (CategoryTheory.homOfLE hVU).op)) (f j))))

Kollár's "D(f_1, …, f_s) = (f_i, ∂f_i/∂x_j)" for the logarithmic derivative along the hypersurface S = (x_h = 0) of an adapted chart, uniformly on an open V of the chart contained in a generating open set U of J: at every b ∈ V the stalk D(−log S)(J)_b is generated by the germs of the f_j, of x_h ∂_h f_j and of the ∂_i f_j, i ≠ h — at b ∈ S by the description of the preserving derivations, at b ∉ S because x_h(b) ≠ 0.

theorem Manifold.hasLocalGenerators_logDerivative_stalkIdeal {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {S : Set M} [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] (hS : IsClosedSubmanifold ψ S 1) (J : IdealSheaf (structureSheaf 𝕜 E M)) : IdealSheaf.HasLocalGenerators fun (a : ↑↧M) => Ideal.logDerivative 𝕜 (hS.idealSheaf.stalkIdeal a) (J.stalkIdeal a)

The logarithmic derivatives of the stalk ideals along a hypersurface have local generators: on an adapted chart at a point of S (the generators f_j, x_h ∂_h f_j, ∂_i f_j), and off S the plain derivatives.

The logarithmic derivative ideal sheaf and its iterates

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

The logarithmic derivative ideal sheaf D(−log S)(J) along a closed hypersurface S [Kol07, 87]: the locally finitely generated ideal sheaf whose stalk at a is Ideal.logDerivative 𝕜 (I_{S,a}) J_a — generated by J_a and all δ f, f ∈ J_a, δ a 𝕜-derivation of 𝒪_{M,a} preserving the ideal of S; in an adapted chart S = (x_h = 0), by J_a, x_h ∂_h f and ∂_j f (j ≠ h).

Equations

• Manifold.IdealSheaf.logDeriv E ψ hS J = Manifold.IdealSheaf.ofStalks (Manifold.structureSheaf 𝕜 E M) (fun (a : ↑↧M) => Ideal.logDerivative 𝕜 (hS.idealSheaf.stalkIdeal a) (J.stalkIdeal a)) ⋯

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

The stalk of D(−log S)(J) at a is D(−log I_{S,a})(J_a) (Ideal.logDerivative).

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

The iterates D^r(−log S)(J) [Kol07, 87].

Equations

• Manifold.IdealSheaf.logDerivIter E ψ hS r J = (Manifold.IdealSheaf.logDeriv E ψ hS)^[r] J

@[simp]

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

@[simp]

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

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