Basic properties of the derivative ideal sheaf

[Kol07, Lemma 74 (1), (2), (5)], "higher derivatives have the usual properties", stated there without proof, and the remark after [Kol07, Definition 73]: if max-ord I ≤ m then Dᵐ(I) = 𝒪_X, so the Dʳ(I) form an ascending chain I ⊂ D(I) ⊂ ⋯ ⊂ Dᵐ(I) = 𝒪_X. The converse is [Wlo05, Definition 2.7.1]: a marked ideal (I, μ) is of maximal order if max{ord_x I} ≤ μ, "or equivalently D^μ(I) = 𝒪_X".

• Order properties, with no hypothesis on f: I ≤ D(I), Dʳ(Dˢ(I)) = D^{r+s}(I) ([Kol07, Lemma 74 (1)]), monotonicity in I and in r, and once Dᵐ(I) = 𝒪_X so is every later Dʳ(I); these are order facts about ofIdeals and iterates.
• On a scheme locally of finite type over k, sectionwise: D(I + J) = D(I) + D(J) (derivative_sup, from Ideal.derivative_sup of Hironaka/Algebra/Derivative/Basic.lean, a k-derivation being additive; this is immediate from the definition and is not one of the items of Lemma 74) and the product rule Dʳ(I·J) ≤ ⨆_{i ≤ r} Dⁱ(I) D^{r−i}(J) ([Kol07, Lemma 74 (2)], derivativeIter_mul_le, from Leibniz for every k-derivation).
• On a smooth k-scheme in characteristic zero: D^μ(I) = 𝒪_X ⟺ max-ord I ≤ μ (derivativeIter_eq_top_iff_maxOrd_le): D^μ(I) is the unit ideal sheaf iff its support {ord ≥ μ + 1} (Hironaka/Scheme/IdealSheaf/Derivative/Cosupport.lean) is empty iff every ord_x I ≤ μ (maxOrd_le_iff, Hironaka/Scheme/IdealSheaf/Order/Constructible.lean).
• [Kol07, Lemma 74 (5)], D(Î) = \widehat{D(I)}, in coordinates: for coordinates whose k-linear ∂ᵢ span the k-derivations, c.adicCompletion.D (J R̂) = (D_k J) R̂ (D_adicCompletion_derivative, from D_adicCompletion of Hironaka/Algebra/Local/DerivativeCompletion.lean), and at a point with residue field algebraic over k such coordinates exist on the stalk (Hironaka/Scheme/IdealSheaf/Derivative/StalkCoords.lean), giving c.adicCompletion.D (I_x Ô_{X,x}) = D(I)_x Ô_{X,x} (exists_regularCoords_D_adicCompletion, which nothing else in the library uses).

Used for Theorem 88 (Hironaka/Scheme/BlowUpSequence/Theorem88Basic.lean, Hironaka/Resolution/Algebraic/Kol07/Theorem88BlowUp.lean, Hironaka/Resolution/Algebraic/Kol07/Theorem88Sequence.lean), for the transforms of derivatives (Hironaka/Scheme/BlowUpSequence/TransformDerivative.lean), for the logarithmic derivative sheaf (Hironaka/Scheme/IdealSheaf/Derivative/LogarithmicSheaf.lean), for tuning (Hironaka/Resolution/Algebraic/Tuning/Sheaf.lean) and for functoriality (Hironaka/Resolution/Algebraic/OrderReduction/Functorial.lean).

The completion, in coordinates ([Kol07, Lemma 74 (5)])

theorem IsLocalRing.RegularCoords.D_adicCompletion_derivative {k : Type u_1} [CommRing k] {R : Type u_2} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] [Algebra k R] {n : ℕ} (c : RegularCoords R n) (hk : c.IsLinearOver k) (hs : c.SpansDerivations k) (J : Ideal R) : c.adicCompletion.D (Ideal.map (algebraMap R (AdicCompletion (maximalIdeal R) R)) J) = Ideal.map (algebraMap R (AdicCompletion (maximalIdeal R) R)) (Ideal.derivative k J)

[Kol07, Lemma 74 (5)], D(Ĵ) = \widehat{D(J)}: for coordinates whose k-linear ∂ᵢ span the k-derivations, the coordinate derivative of J R̂ on the completion is the extension of Kollár's image ideal D_k(J).

Order properties, with no hypothesis on f

theorem AlgebraicGeometry.Scheme.IdealSheafData.le_derivative {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (I : X.IdealSheafData) : I ≤ derivative f I

I ⊆ D(I) ([Kol07, (73.2)]).

theorem AlgebraicGeometry.Scheme.IdealSheafData.derivative_mono {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) {I J : X.IdealSheafData} (h : I ≤ J) : derivative f I ≤ derivative f J

D is monotone.

theorem AlgebraicGeometry.Scheme.IdealSheafData.derivativeIter_derivativeIter {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (r s : ℕ) (I : X.IdealSheafData) : derivativeIter f r (derivativeIter f s I) = derivativeIter f (r + s) I

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

theorem AlgebraicGeometry.Scheme.IdealSheafData.le_derivativeIter {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (r : ℕ) (I : X.IdealSheafData) : I ≤ derivativeIter f r I

I ⊆ Dʳ(I).

theorem AlgebraicGeometry.Scheme.IdealSheafData.derivativeIter_mono {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (r : ℕ) {I J : X.IdealSheafData} (h : I ≤ J) : derivativeIter f r I ≤ derivativeIter f r J

Dʳ is monotone.

theorem AlgebraicGeometry.Scheme.IdealSheafData.derivativeIter_mono_left {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) {r s : ℕ} (h : r ≤ s) (I : X.IdealSheafData) : derivativeIter f r I ≤ derivativeIter f s I

The Dʳ(I) ascend in r (the chain after [Kol07, Definition 73]).

theorem AlgebraicGeometry.Scheme.IdealSheafData.derivativeIter_eq_top_of_le {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) (I : X.IdealSheafData) {m r : ℕ} (h : m ≤ r) (hm : derivativeIter f m I = ⊤) : derivativeIter f r I = ⊤

Once Dᵐ(I) = 𝒪_X, so is every later Dʳ(I).

Sums and products on a scheme locally of finite type, sectionwise

theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_derivativeIter {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [LocallyOfFiniteType f] (r : ℕ) (I : X.IdealSheafData) (U : ↑X.affineOpens) : (derivativeIter f r I).ideal U = Ideal.derivativeIter k r (I.ideal U)

Dʳ(I)(U) = Dʳ(I(U)) on every affine open (ideal_derivative of Hironaka/Scheme/IdealSheaf/Derivative/Sheaf.lean, iterated).

theorem AlgebraicGeometry.Scheme.IdealSheafData.derivative_sup {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [LocallyOfFiniteType f] (I J : X.IdealSheafData) : derivative f (I ⊔ J) = derivative f I ⊔ derivative f J

D(I ⊔ J) = D(I) ⊔ D(J), immediate from the definition of D.

theorem AlgebraicGeometry.Scheme.IdealSheafData.derivative_add {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [LocallyOfFiniteType f] (I J : X.IdealSheafData) : derivative f (I + J) = derivative f I + derivative f J

D(I + J) = D(I) + D(J) (the sum of ideal sheaves is their supremum).

theorem AlgebraicGeometry.Scheme.IdealSheafData.derivative_mul_le {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [LocallyOfFiniteType f] (I J : X.IdealSheafData) : derivative f (I * J) ≤ derivative f I * J + I * derivative f J

[Kol07, Lemma 74 (2)] for r = 1: D(IJ) ⊆ D(I) J + I D(J).

theorem AlgebraicGeometry.Scheme.IdealSheafData.derivativeIter_mul_le {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [LocallyOfFiniteType f] (r : ℕ) (I J : X.IdealSheafData) : derivativeIter f r (I * J) ≤ ⨆ i ∈ Finset.range (r + 1), derivativeIter f i I * derivativeIter f (r - i) J

[Kol07, Lemma 74 (2)], the product rule Dʳ(I·J) ⊆ ∑_{i=0}^r Dⁱ(I) D^{r−i}(J), the sum of ideal sheaves being their supremum.

Maximal order and the completion on a smooth k-scheme in characteristic zero

theorem AlgebraicGeometry.Scheme.IdealSheafData.derivativeIter_eq_top_iff_maxOrd_le {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] (I : X.IdealSheafData) (μ : ℕ) : derivativeIter f μ I = ⊤ ↔ I.maxOrd ≤ ↑μ

[Wlo05, Definition 2.7.1]: (I, μ) is of maximal order, D^μ(I) = 𝒪_X, iff max-ord I ≤ μ. The support of D^μ(I) is {ord ≥ μ + 1}, empty iff every ord_x I ≤ μ.

theorem AlgebraicGeometry.Scheme.IdealSheafData.derivativeIter_eq_top_of_maxOrd_le {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] (I : X.IdealSheafData) {m : ℕ} (h : I.maxOrd ≤ ↑m) : derivativeIter f m I = ⊤

The remark after [Kol07, Definition 73]: if max-ord I ≤ m then Dᵐ(I) = 𝒪_X.

theorem AlgebraicGeometry.Scheme.IdealSheafData.exists_regularCoords_D_adicCompletion {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] (I : X.IdealSheafData) (x : ↥X) (halg : Algebra.IsAlgebraic k (IsLocalRing.ResidueField ↑(X.presheaf.stalk x))) : ∃ (m : ℕ) (c : IsLocalRing.RegularCoords (↑(X.presheaf.stalk x)) m), c.IsLinearOver k ∧ c.SpansDerivations k ∧ c.adicCompletion.D (Ideal.map (algebraMap (↑(X.presheaf.stalk x)) (AdicCompletion (IsLocalRing.maximalIdeal ↑(X.presheaf.stalk x)) ↑(X.presheaf.stalk x))) (I.stalkIdeal x)) = Ideal.map (algebraMap (↑(X.presheaf.stalk x)) (AdicCompletion (IsLocalRing.maximalIdeal ↑(X.presheaf.stalk x)) ↑(X.presheaf.stalk x))) ((derivative f I).stalkIdeal x)

[Kol07, Lemma 74 (5)] at a stalk: at a point with residue field algebraic over k, the stalk carries coordinates spanning the k-derivations, and for them D(Î_x) = \widehat{D(I)_x} in Ô_{X,x}: the coordinate derivative of I_x Ô_{X,x} is the extension of the stalk D(I)_x = D_k(I_x).