The derivative of an ideal

[Kol07, Definition 73]: on a smooth scheme over a field k, with Der_X the sheaf of derivations 𝒪_X → 𝒪_X, the first derivative of an ideal sheaf I is the ideal sheaf D(I) generated by all derivatives of elements of I, D(I) := im[Der_X × I → 𝒪_X] (73.1); in terms of generators, D(f₁, …, f_s) = (fᵢ, ∂fᵢ/∂xⱼ); the higher derivatives are D^{r+1}(I) := D(Dʳ(I)) (73.2).

This module is the affine-local layer: for a k-algebra A and an ideal J, Ideal.derivative k J := J ⊔ (δ f : δ ∈ Der_k(A, A), f ∈ J) (so J ⊆ D(J) by definition; Kollár derives it from f = ∂(xf)/∂x − x ∂f/∂x) and its iterates Ideal.derivativeIter k r J. Proved here: the universal property derivative_le_iff; a derivation lowers the N-adic order by at most one, J ⊆ N^{a+1} ⇒ D(J) ⊆ Nᵃ (derivative_le_pow, derivativeIter_le_pow); D commutes with sums (a derivation is additive) and Dʳ Dˢ = D^{r+s} ([Kol07, Lemma 74 (1)]); the product rule D(JK) ⊆ D(J) K + J D(K) and Dʳ(JK) ⊆ ∑ᵢ Dⁱ(J) D^{r−i}(K) ([Kol07, Lemma 74 (2)]); Kollár's description by generators when the derivations der i generate Der_k(A, A) (derivative_span_eq_of_span), which holds for the dual derivations of a basis of Ω_{A/k} (derivation_mem_span_range_dualBasis, through Mathlib's Der_k(A, A) ≅ Hom_A(Ω_{A/k}, A)); and, for a regular local ℚ-algebra with coordinates (RegularCoords) whose coordinate derivations are k-linear and span the k-derivations (Hironaka/Algebra/Local/CoordsOver.lean), the identification of Kollár's ideal with the coordinate derivative c.D of Hironaka/Algebra/Local/Derivative.lean (derivative_eq_D, derivativeIter_eq_Dpow; the inclusion c.D J ≤ D(J) needs only k-linearity, D_le_derivative).

The sheaf D(I) is Hironaka/Scheme/IdealSheaf/Derivative/Sheaf.lean and the logarithmic version Hironaka/Scheme/IdealSheaf/Derivative/Logarithmic.lean. Used throughout Hironaka/Derivative, Hironaka/Sequence, Hironaka/MaximalContact, Hironaka/Tuning and Hironaka/Balanced, for the blow-up chart (Hironaka/Algebra/Local/BlowUpLiftTransform.lean, Hironaka/Algebra/Local/TransformDerivMap.lean) and for the derivative ideal sheaves on manifolds (Hironaka/Manifold/IdealSheaf/Deriv.lean).

def Ideal.derivative (k : Type u_1) {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (J : Ideal A) : Ideal A

The derivative of an ideal ([Kol07, (73.1)]): the ideal generated by J and all derivatives δ f of its elements under the k-derivations of A.

Equations

• Ideal.derivative k J = J ⊔ ⨆ (δ : Derivation k A A), Ideal.span (⇑δ '' ↑J)

def Ideal.derivativeIter (k : Type u_1) {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (r : ℕ) (J : Ideal A) : Ideal A

Higher derivatives ([Kol07, (73.2)]): D⁰(J) = J, D^{r+1}(J) = D(Dʳ(J)).

Equations

• Ideal.derivativeIter k r J = (Ideal.derivative k)^[r] J

theorem Ideal.le_derivative {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (J : Ideal A) : J ≤ derivative k J

J ⊆ D(J): by definition here; Kollár's f = ∂(xf)/∂x − x ∂f/∂x in [Kol07, Definition 73].

theorem Ideal.derivation_apply_mem_derivative {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (δ : Derivation k A A) {J : Ideal A} {f : A} (hf : f ∈ J) : δ f ∈ derivative k J

δ f ∈ D(J) for f ∈ J.

theorem Ideal.derivative_le_iff {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] {J K : Ideal A} : derivative k J ≤ K ↔ J ≤ K ∧ ∀ (δ : Derivation k A A), ∀ f ∈ J, δ f ∈ K

The universal property of D(J): it lies in K iff J and all derivatives of elements of J do.

theorem Ideal.derivative_mono {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] {J K : Ideal A} (h : J ≤ K) : derivative k J ≤ derivative k K

@[simp]

theorem Ideal.derivativeIter_zero {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (J : Ideal A) : derivativeIter k 0 J = J

@[simp]

theorem Ideal.derivativeIter_succ {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (r : ℕ) (J : Ideal A) : derivativeIter k (r + 1) J = derivative k (derivativeIter k r J)

theorem Ideal.derivativeIter_succ' {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (r : ℕ) (J : Ideal A) : derivativeIter k (r + 1) J = derivativeIter k r (derivative k J)

theorem Ideal.le_derivativeIter {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (r : ℕ) (J : Ideal A) : J ≤ derivativeIter k r J

theorem Ideal.derivativeIter_mono {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (r : ℕ) {J K : Ideal A} (h : J ≤ K) : derivativeIter k r J ≤ derivativeIter k r K

theorem Ideal.derivative_le_pow {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] {J N : Ideal A} {a : ℕ} (h : J ≤ N ^ (a + 1)) : derivative k J ≤ N ^ a

Leibniz for the derivative ideal: J ⊆ N^(a+1) gives D(J) ⊆ N^a — every derivation lowers the N-adic order by at most one (IsLocalRing.derivation_mem_pow).

theorem Ideal.derivativeIter_le_pow {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] {J N : Ideal A} {a r : ℕ} (h : J ≤ N ^ (a + r)) : derivativeIter k r J ≤ N ^ a

J ⊆ N^(a+r) gives Dʳ(J) ⊆ N^a (the easy half of [Kol07, Lemma 74 (3)], for all derivations).

Sums and products

theorem Ideal.derivative_iSup {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] {ι : Sort u_3} (J : ι → Ideal A) : derivative k (⨆ (i : ι), J i) = ⨆ (i : ι), derivative k (J i)

D commutes with arbitrary sums of ideals, a k-derivation being additive.

theorem Ideal.derivative_sup {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (J K : Ideal A) : derivative k (J ⊔ K) = derivative k J ⊔ derivative k K

D(J + K) = D(J) + D(K).

theorem Ideal.derivativeIter_derivativeIter {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (r s : ℕ) (J : Ideal A) : derivativeIter k r (derivativeIter k s J) = derivativeIter k (r + s) J

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

theorem Ideal.derivative_mul_le {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (J K : Ideal A) : derivative k (J * K) ≤ derivative k J * K ⊔ J * derivative k K

[Kol07, Lemma 74 (2)] for r = 1, for all k-derivations: Leibniz, D(JK) ⊆ D(J) K + J D(K).

theorem Ideal.derivativeIter_mul_le {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (r : ℕ) (J K : Ideal A) : derivativeIter k r (J * K) ≤ ⨆ i ∈ Finset.range (r + 1), derivativeIter k i J * derivativeIter k (r - i) K

[Kol07, Lemma 74 (2)], for all k-derivations: the product rule Dʳ(JK) ⊆ ∑_{i ≤ r} Dⁱ(J) D^{r−i}(K), by induction on r from the case r = 1.

Generators

theorem Ideal.derivative_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) (h : ∀ (δ : Derivation k A A), δ ∈ Submodule.span A (Set.range der)) (S : Set A) : derivative k (span S) = span (S ∪ ⋃ (i : ι), ⇑(der i) '' S)

Kollár's description by generators, D(f₁, …, f_s) = (fᵢ, ∂fᵢ/∂xⱼ) ([Kol07, Definition 73]): when the derivations der i generate Der_k(A, A) as an A-module, D(⟨S⟩) = ⟨S, der i s⟩; by Leibniz, the derivative of an A-combination of the generators lies in the ideal they generate.

theorem Ideal.derivation_mem_span_range_dualBasis {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] {ι : Type u_3} [Finite ι] (b : Module.Basis ι A Ω[A⁄k]) (δ : Derivation k A A) : δ ∈ Submodule.span A (Set.range fun (i : ι) => (KaehlerDifferential.linearMapEquivDerivation k A) (b.coord i))

Kollár's "the derivations ∂/∂x₁, …, ∂/∂xₙ are local generators of Der_X" ([Kol07, Definition 73]): for a basis b of Ω_{A/k}, the dual derivations b.coord i ∘ d generate Der_k(A, A); Mathlib's linearMapEquivDerivation identifies Der_k(A, A) with Hom_A(Ω_{A/k}, A), on which the b.coord i form the dual basis.

Kollár's ideal is the coordinate derivative

theorem Ideal.derivative_eq_D {k : Type u_1} [CommRing k] {R : Type u_3} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] [Algebra k R] {n : ℕ} (c : IsLocalRing.RegularCoords R n) (hk : c.IsLinearOver k) (hs : c.SpansDerivations k) (J : Ideal R) : derivative k J = c.D J

When the coordinate derivations of c are k-linear and span the k-derivations (IsLinearOver, SpansDerivations), Kollár's ideal D(J) is the coordinate derivative c.D J of Hironaka/Algebra/Local/Derivative.lean (Kollár's "the derivations ∂/∂x₁, …, ∂/∂xₙ are local generators of Der_X", [Kol07, Definition 73]).

theorem Ideal.D_le_derivative {k : Type u_1} [CommRing k] {R : Type u_3} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] [Algebra k R] {n : ℕ} (c : IsLocalRing.RegularCoords R n) (hk : c.IsLinearOver k) (J : Ideal R) : c.D J ≤ derivative k J

The coordinate derivative c.D J lies in Kollár's ideal as soon as the ∂ᵢ are k-linear (they are then k-derivations); spanning is not needed.

theorem Ideal.Dpow_le_derivativeIter {k : Type u_1} [CommRing k] {R : Type u_3} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] [Algebra k R] {n : ℕ} (c : IsLocalRing.RegularCoords R n) (hk : c.IsLinearOver k) (r : ℕ) (J : Ideal R) : c.Dpow r J ≤ derivativeIter k r J

c.Dʳ J ≤ Dʳ(J) for k-linear coordinate derivations.

theorem Ideal.derivativeIter_eq_Dpow {k : Type u_1} [CommRing k] {R : Type u_3} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] [Algebra k R] {n : ℕ} (c : IsLocalRing.RegularCoords R n) (hk : c.IsLinearOver k) (hs : c.SpansDerivations k) (r : ℕ) (J : Ideal R) : derivativeIter k r J = c.Dpow r J

The iterates: Dʳ(J) = c.Dʳ(J) under the same hypotheses.