Derivative ideals

On a smooth scheme the first derivative D(I) of an ideal sheaf I is the ideal generated by all derivatives of elements of I, and Dʳ⁺¹(I) := D(Dʳ(I)); in local coordinates D(f₁, …, fₛ) = (fᵢ, ∂fᵢ/∂xⱼ) [Kol07, Definition 73]. Here, for a regular local ring R ⊇ ℚ with a coordinate structure c (Hironaka/Algebra/Local/Coords.lean), the derivative ideal is defined with the fixed derivations c.pderiv i; the spanning condition c.SpansDerivations (the ∂ᵢ span all derivations) identifies it with Kollár's coordinate-free definition (Dimg_eq_D).

Main declarations

• RegularCoords.D, RegularCoords.Dpow, and RegularCoords.markedD, the marked derivative Dʳ(I, m) = (Dʳ I, m - r) of [Kol07, Definition 73, (73.3)].
• le_D, D_le_iff, pderiv_mem_D, D_mono, Dpow_mono, Dpow_mono_left, le_Dpow; D_span, Dpow_span (generators and iterated partials); D_sup, D_iSup; D_changeCoords (independence of the coordinates); D_mul_le (the product rule of [Kol07, Lemma 74(2)] for r = 1); D_maximalIdeal_pow, Dpow_maximalIdeal_pow; Dimg_eq_D.
• Dpow_eq_top_of_ord_le: ord I ≤ m → Dᵐ(I) = R, Kollár's remark that the Dʳ(I) form an ascending chain ending in 𝒪_X [Kol07, Definition 73].
• The local forms of [Kol07, Lemma 74]: Dpow_Dpow (iteration, (1)), Dpow_mul_le (the product rule, (2)), le_ord_iff_le_ord_Dpow (the order under derivatives, (3), characteristic zero only), D_map (compatibility with a ring map compatible with the coordinates, the local content of (4)); and the Euler identity euler_sub_nsmul_mem behind (3).

That the top-order partials alone generate Dʳ(I) in characteristic zero (Kollár's parenthetical remark in Definition 73) is proved in Hironaka/Algebra/Local/TopPartials.lean.

def IsLocalRing.RegularCoords.D {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (I : Ideal R) : Ideal R

The first derivative ideal [Kol07, Definition 73, (73.1)]: the ideal generated by I and all ∂ᵢ f, f ∈ I.

Equations

• c.D I = I ⊔ ⨆ (i : Fin n), Ideal.span (⇑(c.pderiv i) '' ↑I)

theorem IsLocalRing.RegularCoords.le_D {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (I : Ideal R) : I ≤ c.D I

I ≤ D(I) (built into the definition).

theorem IsLocalRing.RegularCoords.pderiv_mem_D {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {I : Ideal R} {f : R} (hf : f ∈ I) (i : Fin n) : (c.pderiv i) f ∈ c.D I

theorem IsLocalRing.RegularCoords.D_le_iff {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {I J : Ideal R} : c.D I ≤ J ↔ I ≤ J ∧ ∀ (i : Fin n), ∀ g ∈ I, (c.pderiv i) g ∈ J

theorem IsLocalRing.RegularCoords.D_mono {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {I J : Ideal R} (h : I ≤ J) : c.D I ≤ c.D J

D is monotone.

theorem IsLocalRing.RegularCoords.D_top {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) : c.D ⊤ = ⊤

def IsLocalRing.RegularCoords.Dpow {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : ℕ) (I : Ideal R) : Ideal R

Higher derivative ideals [Kol07, Definition 73, (73.2)]: D⁰(I) = I, Dʳ⁺¹(I) = D(Dʳ(I)).

Equations

• c.Dpow r I = c.D^[r] I

@[simp]

theorem IsLocalRing.RegularCoords.Dpow_zero {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (I : Ideal R) : c.Dpow 0 I = I

@[simp]

theorem IsLocalRing.RegularCoords.Dpow_succ {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : ℕ) (I : Ideal R) : c.Dpow (r + 1) I = c.D (c.Dpow r I)

theorem IsLocalRing.RegularCoords.Dpow_succ' {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : ℕ) (I : Ideal R) : c.Dpow (r + 1) I = c.Dpow r (c.D I)

theorem IsLocalRing.RegularCoords.Dpow_one {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (I : Ideal R) : c.Dpow 1 I = c.D I

theorem IsLocalRing.RegularCoords.Dpow_mono {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : ℕ) {I J : Ideal R} (h : I ≤ J) : c.Dpow r I ≤ c.Dpow r J

Dʳ is monotone in the ideal.

theorem IsLocalRing.RegularCoords.le_Dpow {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : ℕ) (I : Ideal R) : I ≤ c.Dpow r I

theorem IsLocalRing.RegularCoords.Dpow_mono_left {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {r r' : ℕ} (h : r ≤ r') (I : Ideal R) : c.Dpow r I ≤ c.Dpow r' I

The ascending chain I ⊆ D(I) ⊆ D²(I) ⊆ ⋯ of [Kol07, Definition 73]: Dʳ(I) ≤ Dʳ'(I) for r ≤ r'.

theorem IsLocalRing.RegularCoords.D_span {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (S : Set R) : c.D (Ideal.span S) = Ideal.span (S ∪ ⋃ (i : Fin n), ⇑(c.pderiv i) '' S)

D(⟨S⟩) is generated by S and the ∂ⱼ s, s ∈ S (Leibniz: ∂ⱼ(a s) = a ∂ⱼ s + s ∂ⱼ a): Kollár's D(f₁, …, fₛ) = (fᵢ, ∂fᵢ/∂xⱼ) [Kol07, Definition 73].

def IsLocalRing.RegularCoords.iterPderiv {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (l : List (Fin n)) (f : R) : R

The iterated partial derivative along a list of indices, ∂_{i₁} ⋯ ∂_{iₖ} f.

Equations

• c.iterPderiv l f = List.foldr (fun (i : Fin n) (g : R) => (c.pderiv i) g) f l

@[simp]

theorem IsLocalRing.RegularCoords.iterPderiv_nil {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (f : R) : c.iterPderiv [] f = f

@[simp]

theorem IsLocalRing.RegularCoords.iterPderiv_cons {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (i : Fin n) (l : List (Fin n)) (f : R) : c.iterPderiv (i :: l) f = (c.pderiv i) (c.iterPderiv l f)

def IsLocalRing.RegularCoords.iterPderivSet {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (S : Set R) (r : ℕ) : Set R

The iterated partials of order at most r of the elements of S.

Equations

• c.iterPderivSet S r = ⋃ (l : List (Fin n)), ⋃ (_ : l.length ≤ r), c.iterPderiv l '' S

theorem IsLocalRing.RegularCoords.mem_iterPderivSet {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {S : Set R} {r : ℕ} {f : R} : f ∈ c.iterPderivSet S r ↔ ∃ (l : List (Fin n)), l.length ≤ r ∧ ∃ s ∈ S, c.iterPderiv l s = f

theorem IsLocalRing.RegularCoords.iterPderivSet_zero {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (S : Set R) : c.iterPderivSet S 0 = S

theorem IsLocalRing.RegularCoords.iterPderivSet_succ {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (S : Set R) (r : ℕ) : c.iterPderivSet S (r + 1) = c.iterPderivSet S r ∪ ⋃ (i : Fin n), ⇑(c.pderiv i) '' c.iterPderivSet S r

theorem IsLocalRing.RegularCoords.Dpow_span {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (S : Set R) (r : ℕ) : c.Dpow r (Ideal.span S) = Ideal.span (c.iterPderivSet S r)

Dʳ(⟨S⟩) is generated by the iterated partials of order at most r of the elements of S [Wlo05, Definition 2.6.1]; compare the parenthetical remark in [Kol07, Definition 73].

theorem IsLocalRing.RegularCoords.D_sup {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (I J : Ideal R) : c.D (I ⊔ J) = c.D I ⊔ c.D J

D commutes with finite sums of ideals.

theorem IsLocalRing.RegularCoords.D_iSup {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {ι : Sort u_2} (I : ι → Ideal R) : c.D (⨆ (k : ι), I k) = ⨆ (k : ι), c.D (I k)

D commutes with arbitrary sums of ideals.

theorem IsLocalRing.RegularCoords.D_changeCoords {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (x' : Fin n → R) (hx' : maximalIdeal R = Ideal.span (Set.range x')) (hcomm : ∀ (i j : Fin n) (f : R), (c.transportPderiv x' i) ((c.transportPderiv x' j) f) = (c.transportPderiv x' j) ((c.transportPderiv x' i) f)) (I : Ideal R) : (c.changeCoords x' hx' hcomm).D I = c.D I

The derivative ideal does not depend on the coordinate structure (Kollár's definition [Kol07, Definition 73] is coordinate-free).

theorem IsLocalRing.RegularCoords.D_mul_le {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (I J : Ideal R) : c.D (I * J) ≤ c.D I * J ⊔ I * c.D J

The product rule for derivative ideals, D(IJ) ≤ D(I) J + I D(J): [Kol07, Lemma 74(2)] for r = 1, [BM08, Lemma 3.2(2)].

theorem IsLocalRing.RegularCoords.D_maximalIdeal_pow_succ {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (a : ℕ) : c.D (maximalIdeal R ^ (a + 1)) ≤ maximalIdeal R ^ a

D(𝔪^(a+1)) ≤ 𝔪^a, by the product rule.

theorem IsLocalRing.RegularCoords.D_maximalIdeal_pow {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {a : ℕ} (ha : 1 ≤ a) : c.D (maximalIdeal R ^ a) ≤ maximalIdeal R ^ (a - 1)

D(𝔪^a) ≤ 𝔪^(a-1) for a ≥ 1 (and D(𝔪^0) = R, D_maximalIdeal_pow_zero).

theorem IsLocalRing.RegularCoords.D_maximalIdeal_pow_zero {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) : c.D (maximalIdeal R ^ 0) = ⊤

theorem IsLocalRing.RegularCoords.Dpow_maximalIdeal_pow {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {r a : ℕ} (h : r ≤ a) : c.Dpow r (maximalIdeal R ^ a) ≤ maximalIdeal R ^ (a - r)

Dʳ(𝔪^a) ≤ 𝔪^(a-r) for r ≤ a.

theorem IsLocalRing.RegularCoords.Dpow_eq_top_of_ord_le_of_forall {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (h74 : ∀ (I : Ideal R) {r m : ℕ}, r < m → (↑m ≤ ord I ↔ ↑(m - r) ≤ ord (c.Dpow r I))) {I : Ideal R} {m : ℕ} (hord : ord I ≤ ↑m) : c.Dpow m I = ⊤

"If max-ord I ≤ m, then Dᵐ(I) = 𝒪_X" [Kol07, Definition 73], in the local form ord I ≤ m → Dᵐ(I) = R, conditional on the order statement (3) of [Kol07, Lemma 74], which is proved below (le_ord_iff_le_ord_Dpow); Dpow_eq_top_of_ord_le is the unconditional form.

def IsLocalRing.RegularCoords.markedD {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (J : MarkedIdeal R) (r : ℕ) : r ≤ J.m → MarkedIdeal R

The marked derivative [Kol07, Definition 73, (73.3)]: Dʳ(I, m) := (Dʳ(I), m - r) for r ≤ m.

Equations

• c.markedD J r x✝ = { I := c.Dpow r J.I, m := J.m - r }

@[simp]

theorem IsLocalRing.RegularCoords.markedD_I {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (J : MarkedIdeal R) (r : ℕ) (h : r ≤ J.m) : (c.markedD J r h).I = c.Dpow r J.I

@[simp]

theorem IsLocalRing.RegularCoords.markedD_m {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (J : MarkedIdeal R) (r : ℕ) (h : r ≤ J.m) : (c.markedD J r h).m = J.m - r

Kollár's image definition

Kollár defines D(I) as the image of Der_X × I → 𝒪_X over all derivations [Kol07, Definition 73, (73.1)], and notes I ⊂ D(I) through f = ∂(x f) - x ∂f. With the fixed ∂ᵢ the inclusion is built in; the two definitions agree once the ∂ᵢ span the derivations (SpansDerivations) and a coordinate exists.

def IsLocalRing.Dimg {R : Type u_1} [CommRing R] [Algebra ℚ R] (I : Ideal R) : Ideal R

Kollár's definition of the derivative ideal: the ideal generated by δ f for all ℚ-derivations δ and all f ∈ I [Kol07, Definition 73, (73.1)]; it does not refer to coordinates.

Equations

• IsLocalRing.Dimg I = ⨆ (δ : Derivation ℚ R R), Ideal.span (⇑δ '' ↑I)

theorem IsLocalRing.RegularCoords.Dimg_eq_D {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (hs : c.SpansDerivations ℚ) (hn : n ≠ 0) (I : Ideal R) : Dimg I = c.D I

When the ∂ᵢ span the derivations and there is at least one coordinate, Kollár's image definition agrees with D; the inclusion I ≤ Dimg I is Kollár's f = ∂₁(x₁ f) - x₁ ∂₁ f [Kol07, Definition 73].

Kollár's Lemma 74

Kollár: "Higher derivatives have the usual properties" [Kol07, Lemma 74], stated without proof (likewise [Wlo05, Lemma 2.6.2] and [BM08, Lemma 3.2]). Item (1) is iteration; (2) is Leibniz; (3) rests on the Euler identity ∑ᵢ xᵢ ∂ᵢ f ≡ a f (mod 𝔪^(a+1)) for f ∈ 𝔪^a, and on a being a unit in characteristic zero; (4) in local form is a computation on generators.

theorem IsLocalRing.RegularCoords.Dpow_Dpow {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r s : ℕ) (I : Ideal R) : c.Dpow r (c.Dpow s I) = c.Dpow (r + s) I

Dʳ (Dˢ I) = Dʳ⁺ˢ I [Kol07, Lemma 74(1)].

theorem IsLocalRing.RegularCoords.Dpow_mul_le {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (r : ℕ) (I J : Ideal R) : c.Dpow r (I * J) ≤ ⨆ i ∈ Finset.range (r + 1), c.Dpow i I * c.Dpow (r - i) J

The product rule Dʳ (I J) ≤ ∑_{i ≤ r} Dⁱ I · Dʳ⁻ⁱ J [Kol07, Lemma 74(2)].

theorem IsLocalRing.RegularCoords.D_pow_le {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (J : Ideal R) {k : ℕ} (hk : 1 ≤ k) : c.D (J ^ k) ≤ c.D J * J ^ (k - 1)

D (J^k) ≤ D J · J^(k-1) for k ≥ 1 (the product rule as used in the proof of [Kol07, Proposition 99]).

theorem IsLocalRing.RegularCoords.D_finset_prod_le {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {ι : Type u_2} [DecidableEq ι] {s : Finset ι} (hs : s.Nonempty) (J : ι → Ideal R) : c.D (∏ k ∈ s, J k) ≤ ⨆ k ∈ s, c.D (J k) * ∏ l ∈ s.erase k, J l

The product rule for a nonempty finite product of ideals.

theorem IsLocalRing.RegularCoords.D_finset_prod_pow_le {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {ι : Type u_2} [DecidableEq ι] (s : Finset ι) (hs : s.Nonempty) (J : ι → Ideal R) (e : ι → ℕ) (he : ∀ k ∈ s, 1 ≤ e k) : c.D (∏ k ∈ s, J k ^ e k) ≤ ⨆ k ∈ s, c.D (J k) * J k ^ (e k - 1) * ∏ l ∈ s.erase k, J l ^ e l

The product rule for a nonempty finite product of powers with positive exponents. (A sum over the k with cₖ ≥ 1 would be false when every exponent vanishes, since D R = R; the restriction to the support of the exponent vector is left to the caller.)

theorem IsLocalRing.RegularCoords.le_ord_Dpow {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {I : Ideal R} {m r : ℕ} (hm : ↑m ≤ ord I) (hr : r ≤ m) : ↑(m - r) ≤ ord (c.Dpow r I)

The easy inclusion of [Kol07, Lemma 74(3)]: m ≤ ord I implies m - r ≤ ord (Dʳ I) for r ≤ m, from Dʳ(𝔪^m) ≤ 𝔪^(m-r).

The Euler identity

noncomputable def IsLocalRing.RegularCoords.euler {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) : Derivation ℚ R R

The Euler operator ∑ᵢ xᵢ ∂ᵢ.

Equations

• c.euler = ∑ i : Fin n, c.x i • c.pderiv i

theorem IsLocalRing.RegularCoords.euler_apply {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (f : R) : c.euler f = ∑ i : Fin n, c.x i * (c.pderiv i) f

theorem IsLocalRing.RegularCoords.euler_x {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (i : Fin n) : c.euler (c.x i) = c.x i

theorem IsLocalRing.RegularCoords.euler_mem_maximalIdeal {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (f : R) : c.euler f ∈ maximalIdeal R

theorem IsLocalRing.RegularCoords.euler_sub_self_mem_sq {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {h : R} (hh : h ∈ maximalIdeal R) : c.euler h - h ∈ maximalIdeal R ^ 2

E h ≡ h (mod 𝔪²) for h ∈ 𝔪 (Euler's identity in degree one).

theorem IsLocalRing.RegularCoords.euler_sub_nsmul_mem {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {a : ℕ} (ha : 1 ≤ a) {f : R} (hf : f ∈ maximalIdeal R ^ a) : c.euler f - ↑a * f ∈ maximalIdeal R ^ (a + 1)

The Euler identity: E f ≡ a f (mod 𝔪^(a+1)) for f ∈ 𝔪^a, a ≥ 1.

theorem IsLocalRing.RegularCoords.exists_pderiv_notMem_of_notMem_pow_succ {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {a : ℕ} (ha : 1 ≤ a) {f : R} (hf : f ∈ maximalIdeal R ^ a) (hf' : f ∉ maximalIdeal R ^ (a + 1)) : ∃ (i : Fin n), (c.pderiv i) f ∉ maximalIdeal R ^ a

An element of 𝔪^a ∖ 𝔪^(a+1), a ≥ 1, has a partial derivative outside 𝔪^a (the characteristic-zero fact behind [Kol07, Lemma 74(3)], "char. 0 only!", and [Wlo05, Lemma 2.6.2]). If all ∂ᵢ f ∈ 𝔪^a then E f ∈ 𝔪^(a+1), so a f ∈ 𝔪^(a+1) by the Euler identity, and a is a unit.

theorem IsLocalRing.RegularCoords.D_bot {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) : c.D ⊥ = ⊥

D 0 = 0.

theorem IsLocalRing.RegularCoords.D_eq_top_of_ord_eq_zero {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {I : Ideal R} (hI : ord I = 0) : c.D I = ⊤

If ord I = 0 then D I = R.

theorem IsLocalRing.RegularCoords.ord_D_of_ord_eq {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {a : ℕ} (ha : 1 ≤ a) {I : Ideal R} (hI : ord I = ↑a) : ord (c.D I) = ↑(a - 1)

If ord I = a ≥ 1 then ord (D I) = a - 1.

theorem IsLocalRing.RegularCoords.ord_Dpow_of_ord_eq {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {a : ℕ} {I : Ideal R} (hI : ord I = ↑a) {r : ℕ} (hr : r ≤ a) : ord (c.Dpow r I) = ↑(a - r)

ord (Dʳ I) = a - r for ord I = a and r ≤ a.

theorem IsLocalRing.RegularCoords.le_ord_iff_le_ord_Dpow {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (I : Ideal R) {r m : ℕ} (h : r < m) : ↑m ≤ ord I ↔ ↑(m - r) ≤ ord (c.Dpow r I)

For r < m, m ≤ ord I ↔ m - r ≤ ord (Dʳ I): the local form of cosupp(I, m) = cosupp(Dʳ(I), m − r) [Kol07, Lemma 74(3)], [Wlo05, Lemma 2.6.2], [BM08, Lemma 3.2(3)].

theorem IsLocalRing.RegularCoords.Dpow_eq_top_of_ord_le {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {I : Ideal R} {m : ℕ} (hord : ord I ≤ ↑m) : c.Dpow m I = ⊤

If ord I ≤ m then Dᵐ I = R [Kol07, Definition 73] (from le_ord_iff_le_ord_Dpow).

theorem IsLocalRing.RegularCoords.D_span_singleton_x_pow {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (i : Fin n) {m : ℕ} (hm : 1 ≤ m) : c.D (Ideal.span {c.x i ^ m}) = Ideal.span {c.x i ^ (m - 1)}

The derivative of a power of a coordinate: D ⟨xᵢ^m⟩ = ⟨xᵢ^(m-1)⟩ for m ≥ 1 (m is a unit in characteristic zero).

theorem IsLocalRing.RegularCoords.Dpow_span_singleton_x_pow {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (i : Fin n) {r m : ℕ} (hr : r ≤ m) : c.Dpow r (Ideal.span {c.x i ^ m}) = Ideal.span {c.x i ^ (m - r)}

Dʳ ⟨xᵢ^m⟩ = ⟨xᵢ^(m-r)⟩ for r ≤ m.

theorem IsLocalRing.RegularCoords.D_span_singleton_x_mul_x {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {i j : Fin n} (hij : i ≠ j) : c.D (Ideal.span {c.x i * c.x j}) = Ideal.span {c.x i, c.x j}

D ⟨xᵢ xⱼ⟩ = ⟨xᵢ, xⱼ⟩ for i ≠ j.

theorem IsLocalRing.RegularCoords.D_map {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {R' : Type u_2} [CommRing R'] [IsRegularLocalRing R'] [Algebra ℚ R'] {n' : ℕ} (c' : RegularCoords R' n') (φ : R →+* R') (e : Fin n → Fin n') (hφ : ∀ (i : Fin n) (f : R), (c'.pderiv (e i)) (φ f) = φ ((c.pderiv i) f)) (hφ' : ∀ j ∉ Set.range e, ∀ (f : R), (c'.pderiv j) (φ f) = 0) (I : Ideal R) : c'.D (Ideal.map φ I) = Ideal.map φ (c.D I)

The local content of "D(f^* I) = f^*(D(I)) for smooth f" [Kol07, Lemma 74(4)], [Wlo05, Lemma 2.6.5], [BM08, Lemma 3.2(4)]: for φ : R → R' compatible with the derivations (∂'_{e i} ∘ φ = φ ∘ ∂ᵢ, and ∂'ⱼ ∘ φ = 0 off the image of e), D' (φ(I) R') = φ(D I) R'.

theorem IsLocalRing.RegularCoords.D_map_le {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {R' : Type u_2} [CommRing R'] [IsRegularLocalRing R'] [Algebra ℚ R'] {n' : ℕ} (c' : RegularCoords R' n') (φ : R →+* R') (e : Fin n' → Fin n) (hφ : ∀ (j : Fin n') (f : R), (c'.pderiv j) (φ f) = φ ((c.pderiv (e j)) f)) (I : Ideal R) : c'.D (Ideal.map φ I) ≤ Ideal.map φ (c.D I)

If every coordinate derivation of R' is induced along φ by one of R (∂'ⱼ ∘ φ = φ ∘ ∂_{e j}), then D' (φ I) ≤ φ (D I): the local content of Kollár's (DI)|_S ⊃ D(I|_S) for the restriction to a smooth subvariety (the discussion preceding [Kol07, Definition 83]). For the restriction to R̄ = R/⟨x₁⟩ with coordinates x₂, …, xₙ the extra generators ∂₁ f only enlarge the right side.

theorem IsLocalRing.RegularCoords.Dpow_map_le {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {R' : Type u_2} [CommRing R'] [IsRegularLocalRing R'] [Algebra ℚ R'] {n' : ℕ} (c' : RegularCoords R' n') (φ : R →+* R') (e : Fin n' → Fin n) (hφ : ∀ (j : Fin n') (f : R), (c'.pderiv j) (φ f) = φ ((c.pderiv (e j)) f)) (r : ℕ) (I : Ideal R) : c'.Dpow r (Ideal.map φ I) ≤ Ideal.map φ (c.Dpow r I)

D'ʳ (φ I) ≤ φ (Dʳ I) under the hypothesis of D_map_le.