The derivative ideal sheaf: 𝓘 ⊆ D(𝓘), the chart description, the iterates

Properties of IdealSheaf.deriv and iteratedDeriv (Hironaka/Manifold/IdealSheaf/Deriv.lean), Kollár's derivative ideal sheaves [Kol07, Definition 73]:

• le_deriv: J ⊆ D(J) (Kollár's "Note that I ⊂ D(I)", built into Ideal.derivative);
• stalkIdeal_deriv_eq_sup_iSup_coordDerivStalk: in a chart at a, D(J)_a = J_a + ∑_i ∂_i(J_a) with the coordinate derivations (Kollár's "local generators of Der_X"); coordDeriv_mem_carrier_deriv: the partial derivative of a section of J is a section of D(J); stalkIdeal_deriv_eq_span: on a generating open set, D(J)_b = (f_j, ∂_i f_j);
• stalkIdeal_deriv_eq_D: through the Hironaka library's regular coordinates of the stalk (IsLocalRing.RegularCoords, with the conditions IsLinearOver 𝕜 and SpansDerivations 𝕜 that the analytic stalk satisfies), D(J)_a is the coordinate derivative c.D J_a (Ideal.derivative_eq_D), so the local theory of derivative ideals of the Hironaka library applies to the stalks;
• the iterates: iteratedDeriv_zero, iteratedDeriv_succ ((73.2)), le_iteratedDeriv (the chain J ⊆ D(J) ⊆ D²(J) ⊆ ⋯), iteratedDeriv_add ([Kol07, Lemma 74 (1)]), and their stalks stalkIdeal_iteratedDeriv (= Ideal.derivativeIter) and stalkIdeal_iteratedDeriv_eq_Dpow (= c.Dpow r J_a).

These are the lemmas through which the derivative ideal sheaves are computed at the stalks in the maximal-contact and order-reduction arguments.

theorem Manifold.IdealSheaf.le_deriv {𝕜 : 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)) : J ≤ J.deriv

Kollár's "I ⊂ D(I)" [Kol07, Definition 73].

theorem Manifold.IdealSheaf.stalkIdeal_deriv_eq_sup_iSup_coordDerivStalk {𝕜 : 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)) {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {a : M} (ha : a ∈ φ.source) : J.deriv.stalkIdeal a = J.stalkIdeal a ⊔ ⨆ (i : Fin n), Ideal.span (⇑(coordDerivStalk E ψ φ hφ ha i) '' ↑(J.stalkIdeal a))

In a chart (φ, ψ) at a, the stalk of D(J) is generated by J_a and the coordinate partial derivatives ∂_i f, f ∈ J_a ([Kol07, Definition 73]; [BM97, (0.3)]).

theorem Manifold.IdealSheaf.coordDeriv_mem_carrier_deriv {𝕜 : 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)) {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (V : TopologicalSpace.Opens M) (hV : ↑V ⊆ φ.source) {f : ↑((structureSheaf 𝕜 E M).presheaf.obj (Opposite.op V))} (hf : f ∈ J.carrier V) (i : Fin n) : (coordDeriv E ψ φ hφ V hV i) f ∈ J.deriv.carrier V

The coordinate partial derivative of a section of J over an open V of the chart is a section of D(J).

theorem Manifold.IdealSheaf.stalkIdeal_deriv_eq_span {𝕜 : 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)) {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 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) : J.deriv.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 stalk of D(J) at b ∈ V is generated by the germs of the generators f_j and of their coordinate partial derivatives ∂_i f_j.

theorem Manifold.IdealSheaf.stalkIdeal_deriv_eq_D {𝕜 : 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)) {n : ℕ} {a : M} [IsRegularLocalRing ↑((structureSheaf 𝕜 E M).presheaf.stalk a)] (c : IsLocalRing.RegularCoords (↑((structureSheaf 𝕜 E M).presheaf.stalk a)) n) (hk : c.IsLinearOver 𝕜) (hs : c.SpansDerivations 𝕜) : J.deriv.stalkIdeal a = c.D (J.stalkIdeal a)

For regular coordinates c of the stalk (IsLocalRing.RegularCoords) with 𝕜-linear, spanning derivations, the stalk of D(J) is the coordinate derivative c.D J_a of the Hironaka library (Ideal.derivative_eq_D).

The iterates Dʳ(J)

@[simp]

theorem Manifold.IdealSheaf.iteratedDeriv_zero {𝕜 : 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)) : J.iteratedDeriv 0 = J

@[simp]

theorem Manifold.IdealSheaf.iteratedDeriv_succ {𝕜 : 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)) (r : ℕ) : J.iteratedDeriv (r + 1) = (J.iteratedDeriv r).deriv

D^{r+1}(J) = D(D^r(J)) [Kol07, Definition 73, (73.2)].

theorem Manifold.IdealSheaf.iteratedDeriv_succ' {𝕜 : 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)) (r : ℕ) : J.iteratedDeriv (r + 1) = J.deriv.iteratedDeriv r

theorem Manifold.IdealSheaf.le_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)) (r : ℕ) : J ≤ J.iteratedDeriv r

The chain J ⊆ D(J) ⊆ D²(J) ⊆ ⋯.

theorem Manifold.IdealSheaf.iteratedDeriv_le_succ {𝕜 : 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)) (r : ℕ) : J.iteratedDeriv r ≤ J.iteratedDeriv (r + 1)

theorem Manifold.IdealSheaf.iteratedDeriv_add {𝕜 : 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)) (r s : ℕ) : J.iteratedDeriv (r + s) = (J.iteratedDeriv s).iteratedDeriv r

D^r(D^s(J)) = D^{r+s}(J) [Kol07, Lemma 74 (1)].

theorem Manifold.IdealSheaf.stalkIdeal_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)) (r : ℕ) (a : M) : (J.iteratedDeriv r).stalkIdeal a = Ideal.derivativeIter 𝕜 r (J.stalkIdeal a)

The stalk of D^r(J) is Kollár's r-th derivative D^r(J_a) of the stalk ideal (Ideal.derivativeIter).

theorem Manifold.IdealSheaf.stalkIdeal_iteratedDeriv_eq_Dpow {𝕜 : 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)) {n : ℕ} {a : M} [IsRegularLocalRing ↑((structureSheaf 𝕜 E M).presheaf.stalk a)] (c : IsLocalRing.RegularCoords (↑((structureSheaf 𝕜 E M).presheaf.stalk a)) n) (hk : c.IsLinearOver 𝕜) (hs : c.SpansDerivations 𝕜) (r : ℕ) : (J.iteratedDeriv r).stalkIdeal a = c.Dpow r (J.stalkIdeal a)

Through regular coordinates c of the stalk, the stalk of D^r(J) is the Hironaka library's c.Dpow r J_a (Ideal.derivativeIter_eq_Dpow).