The top-order partials generate Dʳ(I) in characteristic zero

Kollár remarks, in [Kol07, Definition 73], that Dʳ(I) contains all r-th partial derivatives of elements of I but is bigger over general rings ("try second derivatives over ℤ[x]"), while over fields of characteristic zero the two agree, by formulas such as ∂f/∂y = ∂²(xf)/∂y∂x − x ∂²f/∂y∂x and 2 ∂f/∂x = ∂²(xf)/∂x² − x ∂²f/∂x².

Dʳ(I) is generated by the iterated partials of order ≤ r of the elements of I (Dpow_span, Hironaka/Algebra/Local/Derivative.lean); this file shows that in characteristic zero (Algebra ℚ R, the standing hypothesis of RegularCoords) the partials of order exactly r suffice, as long as there is a coordinate to differentiate along (0 < n). The general form of Kollár's two identities is ∂^{i₀ ∷ l}(x_{i₀} f) = x_{i₀} ∂^{i₀ ∷ l} f + (k + 1) ∂^l f, k the number of occurrences of i₀ in l (iterPderiv_x_mul), and k + 1 is a unit. The result is a remark on the definition; nothing else in the library depends on it.

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

The partials of order exactly r of the elements of S (compare iterPderivSet, order ≤ r).

Equations

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

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

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

theorem IsLocalRing.RegularCoords.iterPderiv_perm {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {l l' : List (Fin n)} (h : l.Perm l') (f : R) : c.iterPderiv l f = c.iterPderiv l' f

Iterated partials do not depend on the order of differentiation.

theorem IsLocalRing.RegularCoords.iterPderiv_mem_Dpow {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {I : Ideal R} {f : R} (hf : f ∈ I) (l : List (Fin n)) : c.iterPderiv l f ∈ c.Dpow l.length I

Every r-th partial of an element of I lies in Dʳ(I) [Kol07, Definition 73].

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

The r-th partials of elements of I lie in Dʳ(I).

theorem IsLocalRing.RegularCoords.pderiv_eq_of_ne {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) {i j : Fin n} (h : j ≠ i) (f : R) : (c.pderiv j) f = (c.pderiv j) ((c.pderiv i) (c.x i * f)) - c.x i * (c.pderiv j) ((c.pderiv i) f)

Kollár's first identity [Kol07, Definition 73]: for j ≠ i, ∂ⱼ f = ∂ⱼ∂ᵢ(xᵢ f) − xᵢ ∂ⱼ∂ᵢ f.

theorem IsLocalRing.RegularCoords.two_nsmul_pderiv {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (i : Fin n) (f : R) : 2 • (c.pderiv i) f = (c.pderiv i) ((c.pderiv i) (c.x i * f)) - c.x i * (c.pderiv i) ((c.pderiv i) f)

Kollár's second identity [Kol07, Definition 73]: 2 ∂ᵢ f = ∂ᵢ²(xᵢ f) − xᵢ ∂ᵢ² f.

theorem IsLocalRing.RegularCoords.iterPderiv_x_mul {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (l : List (Fin n)) (i : Fin n) (f : R) : c.iterPderiv l (c.x i * f) = c.x i * c.iterPderiv l f + List.count i l • c.iterPderiv (l.erase i) f

The general form of Kollár's identities: ∂^l(xᵢ f) = xᵢ ∂^l f + k ∂^{l ∖ i} f, where k is the number of occurrences of i in l and l ∖ i erases one of them.

theorem IsLocalRing.RegularCoords.iterPderiv_mem_span_topPderivSet_succ {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (hn : 0 < n) {I : Ideal R} {f : R} (hf : f ∈ I) (l : List (Fin n)) : c.iterPderiv l f ∈ Ideal.span (c.topPderivSet (↑I) (l.length + 1))

In characteristic zero, every r-th partial of an element of I is a combination of (r+1)-th partials of elements of I, provided there is a coordinate (0 < n): (k + 1) ∂^l f = ∂^{i₀ ∷ l}(x_{i₀} f) − x_{i₀} ∂^{i₀ ∷ l} f with k + 1 a unit.

theorem IsLocalRing.RegularCoords.span_topPderivSet_le_succ {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (hn : 0 < n) (I : Ideal R) (r : ℕ) : Ideal.span (c.topPderivSet (↑I) r) ≤ Ideal.span (c.topPderivSet (↑I) (r + 1))

In characteristic zero the r-th partials of elements of I lie in the span of the (r+1)-th partials (0 < n).

theorem IsLocalRing.RegularCoords.span_topPderivSet_mono {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (hn : 0 < n) (I : Ideal R) {r s : ℕ} (hrs : r ≤ s) : Ideal.span (c.topPderivSet (↑I) r) ≤ Ideal.span (c.topPderivSet (↑I) s)

theorem IsLocalRing.RegularCoords.Dpow_eq_span_topPderivSet {R : Type u_1} [CommRing R] [IsRegularLocalRing R] [Algebra ℚ R] {n : ℕ} (c : RegularCoords R n) (hn : 0 < n) (I : Ideal R) (r : ℕ) : c.Dpow r I = Ideal.span (c.topPderivSet (↑I) r)

In characteristic zero, Dʳ(I) is generated by the r-th iterated partials of the elements of I alone, provided there is a coordinate (0 < n) (Kollár's remark in [Kol07, Definition 73]).