The derivative ideal sheaf D(𝓘) and its iterates Dʳ(𝓘)

Kollár's derivative of an ideal sheaf [Kol07, Definition 73]: on a smooth variety the derivations ∂/∂x_1, …, ∂/∂x_n of a system of local coordinates generate the sheaf Der_X of derivations, and the first derivative of an ideal sheaf I is the ideal sheaf generated by I together with the derivatives of its elements, "D(I) := im[Der_X × I → 𝒪_X]" (73.1) — in terms of generators, "D(f_1, …, f_s) = (f_i, ∂f_i/∂x_j)" — and the higher derivatives are the iterates D^{r+1}(I) := D(D^r(I)) (73.2). This module defines D(J) and D^r(J) for a locally finitely generated ideal sheaf J on an analytic manifold.

The stalk of D(J) at a is Kollár's (73.1) for the stalk 𝒪_{M,a} with its 𝕜-derivations — the Hironaka library's Ideal.derivative 𝕜 (J.stalkIdeal a) = J_a ⊔ ⨆ δ, ⟨δ(J_a)⟩ (Hironaka/Algebra/Derivative/Basic.lean, with "I ⊂ D(I)" built in) — so it is chart-independent by construction. In a chart (φ, ψ) at a the coordinate derivations ∂_i = coordDerivStalk (Hironaka/Manifold/Germ/CoordDeriv.lean) generate the 𝕜-derivations as an 𝒪_{M,a}-module (coordDerivStalk_mem_span, from δ = ∑_i δ(x_i − x_i(a)) ∂_i), so Ideal.derivative_span_eq_of_span gives Kollár's "D(f_1, …, f_s) = (f_i, ∂f_i/∂x_j)": on an open V of the chart inside a generating open set of J, the germs of the generators f_j and of their partials ∂_i f_j (coordDeriv, whose germs are the ∂_i of the germs) generate D(J)_b at every b ∈ V (derivative_stalkIdeal_eq_span). Hence the family of stalks has local generators (hasLocalGenerators_derivative_stalkIdeal, in the chart at a of the maximal atlas with the coordinates modelCoord of the finite-dimensional model space), and IdealSheaf.deriv is ofStalks with these stalks; iteratedDeriv is its r-fold iterate (73.2). The partial derivatives are those of Bierstone–Milman's regular coordinate charts [BM97, (0.3)].

The derivative ideal sheaves give the maximal contact ideals MC(J) = D^{m−1}(J) and the coefficient ideals of the order-reduction algorithm (Hironaka/Manifold/IdealSheaf/Tuning.lean, Hironaka/Resolution/Analytic/OrderReduction/).

theorem Manifold.coordDerivStalk_mem_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) {a : M} (ha : a ∈ φ.source) (δ : Derivation 𝕜 ↑((structureSheaf 𝕜 E M).presheaf.stalk a) ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) : δ ∈ Submodule.span (↑((structureSheaf 𝕜 E M).presheaf.stalk a)) (Set.range (coordDerivStalk E ψ φ hφ ha))

Kollár's "the derivations ∂/∂x_1, …, ∂/∂x_n are local generators of Der_X" [Kol07, Definition 73]: every 𝕜-derivation of the stalk 𝒪_{M,a} lies in the 𝒪_{M,a}-span of the coordinate derivations ∂_i of the chart — δ = ∑_i δ(x_i − x_i(a)) ∂_i.

theorem Manifold.derivative_eq_sup_iSup_span_image_coordDerivStalk {𝕜 : 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) (I : Ideal ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) : Ideal.derivative 𝕜 I = I ⊔ ⨆ (i : Fin n), Ideal.span (⇑(coordDerivStalk E ψ φ hφ ha i) '' ↑I)

Kollár's (73.1) read in a chart ([Kol07, Definition 73]; [BM97, (0.3)]): the derivative D(I) = I + ∑_δ ⟨δ(I)⟩ of an ideal I of the stalk is generated by I and the coordinate partial derivatives ∂_i f, f ∈ I.

theorem Manifold.IdealSheaf.derivative_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) (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))) {V : TopologicalSpace.Opens M} (hVU : V ≤ U) (hV : ↑V ⊆ φ.source) {b : M} (hb : b ∈ V) : Ideal.derivative 𝕜 (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)) ((coordDeriv E ψ φ hφ V hV 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)" [Kol07, Definition 73]: on an open V of a chart inside a generating open set U of J, the derivative of the stalk ideal at b ∈ V is generated by the germs of the generators f_j and of their coordinate partial derivatives ∂_i f_j (the germ of ∂_i f_j is ∂_i of the germ of f_j).

theorem Manifold.IdealSheaf.hasLocalGenerators_derivative_stalkIdeal {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (J : IdealSheaf (structureSheaf 𝕜 E M)) [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [FiniteDimensional 𝕜 E] : HasLocalGenerators fun (a : ↑↧M) => Ideal.derivative 𝕜 (J.stalkIdeal a)

The derivatives of the stalk ideals have local generators: on U ∩ (chart at a), for U a generating open set of J, the generators f_j and their partials ∂_i f_j in the chart at a (modelCoord the coordinates of the finite-dimensional model space).

noncomputable def Manifold.IdealSheaf.deriv {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (J : IdealSheaf (structureSheaf 𝕜 E M)) [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [FiniteDimensional 𝕜 E] : IdealSheaf (structureSheaf 𝕜 E M)

The derivative ideal sheaf D(J) ([Kol07, Definition 73, (73.1)]; [BM97, (0.3)]): the locally finitely generated ideal sheaf whose stalk at a is Kollár's derivative Ideal.derivative 𝕜 J_a of the stalk ideal — generated by J_a and all δ f, f ∈ J_a, δ a 𝕜-derivation of 𝒪_{M,a}; in a chart, by J_a and the coordinate partials ∂_i f.

Equations

• J.deriv = Manifold.IdealSheaf.ofStalks (Manifold.structureSheaf 𝕜 E M) (fun (a : ↑↧M) => Ideal.derivative 𝕜 (J.stalkIdeal a)) ⋯

@[simp]

theorem Manifold.IdealSheaf.stalkIdeal_deriv {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (J : IdealSheaf (structureSheaf 𝕜 E M)) [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [FiniteDimensional 𝕜 E] (a : M) : J.deriv.stalkIdeal a = Ideal.derivative 𝕜 (J.stalkIdeal a)

The stalk of D(J) is Kollár's derivative D(J_a) = J_a ⊔ ∑_δ ⟨δ(J_a)⟩ of the stalk ideal (Ideal.derivative).

noncomputable def Manifold.IdealSheaf.iteratedDeriv {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] (J : IdealSheaf (structureSheaf 𝕜 E M)) [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [FiniteDimensional 𝕜 E] (r : ℕ) : IdealSheaf (structureSheaf 𝕜 E M)

The higher derivative ideal sheaves D^0(J) = J, D^{r+1}(J) = D(D^r(J)) [Kol07, Definition 73, (73.2)].

Equations

• J.iteratedDeriv r = (fun (I : Manifold.IdealSheaf (Manifold.structureSheaf 𝕜 E M)) => I.deriv)^[r] J