The Euler operator along a subset of coordinates and the Taylor criterion

The order of a function f along a closed subspace C at a point is the largest p with f ∈ I_C^p [BM97, Chapter I, §3]; in coordinates adapted to a submanifold it is read off the Taylor expansion of f in the coordinates defining the submanifold. This file proves the algebra behind that reading. In a commutative algebra R over a field k of characteristic zero with elements x_i and derivations ∂_i (pd i) satisfying ∂_i x_j = δ_ij on a finite index set S, let J_S = (x_i : i ∈ S). The Euler operator E_S f = ∑_{i ∈ S} x_i ∂_i f satisfies E_S f − a f ∈ J_S^{a+1} for f ∈ J_S^a (eulerS_sub_nsmul_mem: the Euler identity behind the characteristic-zero clause (3) of [Kol07, Lemma 74], with the maximal ideal replaced by J_S), hence f ∈ J_S^a and ∂_i f ∈ J_S^a for all i ∈ S force f ∈ J_S^{a+1} (mem_pow_succ_of_forall_pderiv_mem; a is invertible in characteristic zero). By induction this gives the Taylor criterion along S: f ∈ J_S^p iff every iterated derivative of f along fewer than p coordinates of S lies in J_S (mem_coordIdeal_pow_iff; the easy direction is that a derivation lowers the power of an ideal by one, derivation_apply_mem_pow_of_mem_pow_succ). On the stalk of an analytic manifold with the coordinate derivations of a chart adapted to a submanifold Y, and S the indices of the coordinates defining Y, J_S is the ideal of Y and "∂_S^l f ∈ J_S" reads "∂_S^l f vanishes on Y" — the coefficient functions of the expansion f = ∑_α f_α(w) z^α in Hironaka/Manifold/BlowUp/Transform/OrderAlong.lean, where this criterion computes the order of an ideal sheaf along the centre of a blow-up.

def IsLocalRing.coordIdeal {R : Type u_2} [CommRing R] {ι : Type u_3} (x : ι → R) (S : Finset ι) : Ideal R

The ideal J_S generated by the coordinates indexed by S (on a stalk, with S the indices of the coordinates defining a submanifold Y in an adapted chart, the ideal of Y).

Equations

• IsLocalRing.coordIdeal x S = Ideal.span (x '' ↑S)

theorem IsLocalRing.x_mem_coordIdeal {R : Type u_2} [CommRing R] {ι : Type u_3} (x : ι → R) (S : Finset ι) {i : ι} (hi : i ∈ S) : x i ∈ coordIdeal x S

The coordinates indexed by S lie in J_S.

theorem IsLocalRing.derivation_apply_mem_pow_of_mem_pow_succ {k : Type u_1} [Field k] {R : Type u_2} [CommRing R] [Algebra k R] (D : Derivation k R R) (J : Ideal R) (m : ℕ) {f : R} : f ∈ J ^ (m + 1) → D f ∈ J ^ m

A derivation lowers the power of an ideal by one.

def IsLocalRing.iterD {k : Type u_1} [Field k] {R : Type u_2} [CommRing R] [Algebra k R] {ι : Type u_3} (pd : ι → Derivation k R R) (l : List ι) (f : R) : R

Iterated derivatives along a list of indices, iterD [i₁, …, iₖ] f = ∂_{i₁} (∂_{i₂} (… (∂_{iₖ} f))).

Equations

• IsLocalRing.iterD pd l f = List.foldr (fun (i : ι) (g : R) => (pd i) g) f l

theorem IsLocalRing.iterD_nil {k : Type u_1} [Field k] {R : Type u_2} [CommRing R] [Algebra k R] {ι : Type u_3} (pd : ι → Derivation k R R) (f : R) : iterD pd [] f = f

The empty iterated derivative is the identity.

theorem IsLocalRing.iterD_cons {k : Type u_1} [Field k] {R : Type u_2} [CommRing R] [Algebra k R] {ι : Type u_3} (pd : ι → Derivation k R R) (i : ι) (l : List ι) (f : R) : iterD pd (i :: l) f = (pd i) (iterD pd l f)

One more derivative in front.

theorem IsLocalRing.iterD_append_singleton {k : Type u_1} [Field k] {R : Type u_2} [CommRing R] [Algebra k R] {ι : Type u_3} (pd : ι → Derivation k R R) (l : List ι) (i : ι) (f : R) : iterD pd (l ++ [i]) f = iterD pd l ((pd i) f)

One more derivative at the back.

theorem IsLocalRing.iterD_mem_pow {k : Type u_1} [Field k] {R : Type u_2} [CommRing R] [Algebra k R] {ι : Type u_3} (pd : ι → Derivation k R R) (J : Ideal R) (l : List ι) {p : ℕ} {f : R} : f ∈ J ^ (p + l.length) → iterD pd l f ∈ J ^ p

Iterated derivatives lower the power of an ideal by the length.

def IsLocalRing.eulerS {k : Type u_1} [Field k] {R : Type u_2} [CommRing R] [Algebra k R] {ι : Type u_3} (x : ι → R) (pd : ι → Derivation k R R) (S : Finset ι) (f : R) : R

The Euler operator along S, E_S f = ∑_{i ∈ S} x_i ∂_i f.

Equations

• IsLocalRing.eulerS x pd S f = ∑ i ∈ S, x i * (pd i) f

theorem IsLocalRing.eulerS_add {k : Type u_1} [Field k] {R : Type u_2} [CommRing R] [Algebra k R] {ι : Type u_3} (x : ι → R) (pd : ι → Derivation k R R) (S : Finset ι) (f g : R) : eulerS x pd S (f + g) = eulerS x pd S f + eulerS x pd S g

The Euler operator is additive.

theorem IsLocalRing.eulerS_mul {k : Type u_1} [Field k] {R : Type u_2} [CommRing R] [Algebra k R] {ι : Type u_3} (x : ι → R) (pd : ι → Derivation k R R) (S : Finset ι) (f g : R) : eulerS x pd S (f * g) = f * eulerS x pd S g + g * eulerS x pd S f

The Leibniz rule for the Euler operator.

theorem IsLocalRing.eulerS_mem {k : Type u_1} [Field k] {R : Type u_2} [CommRing R] [Algebra k R] {ι : Type u_3} (x : ι → R) (pd : ι → Derivation k R R) (S : Finset ι) (f : R) : eulerS x pd S f ∈ coordIdeal x S

E_S f ∈ J_S for every f.

theorem IsLocalRing.eulerS_x {k : Type u_1} [Field k] {R : Type u_2} [CommRing R] [Algebra k R] {ι : Type u_3} (x : ι → R) (pd : ι → Derivation k R R) (S : Finset ι) [DecidableEq ι] (hx : ∀ i ∈ S, ∀ j ∈ S, (pd i) (x j) = if i = j then 1 else 0) {j : ι} (hj : j ∈ S) : eulerS x pd S (x j) = x j

E_S x_j = x_j for j ∈ S (the Euler identity on the coordinates).

theorem IsLocalRing.eulerS_sub_self_mem_sq {k : Type u_1} [Field k] {R : Type u_2} [CommRing R] [Algebra k R] {ι : Type u_3} (x : ι → R) (pd : ι → Derivation k R R) (S : Finset ι) [DecidableEq ι] (hx : ∀ i ∈ S, ∀ j ∈ S, (pd i) (x j) = if i = j then 1 else 0) {h : R} (hh : h ∈ coordIdeal x S) : eulerS x pd S h - h ∈ coordIdeal x S ^ 2

E_S h − h ∈ J_S² for h ∈ J_S.

theorem IsLocalRing.eulerS_sub_nsmul_mem {k : Type u_1} [Field k] {R : Type u_2} [CommRing R] [Algebra k R] {ι : Type u_3} (x : ι → R) (pd : ι → Derivation k R R) (S : Finset ι) [DecidableEq ι] (hx : ∀ i ∈ S, ∀ j ∈ S, (pd i) (x j) = if i = j then 1 else 0) {a : ℕ} (ha : 1 ≤ a) {f : R} (hf : f ∈ coordIdeal x S ^ a) : eulerS x pd S f - ↑a * f ∈ coordIdeal x S ^ (a + 1)

The Euler identity along S: E_S f − a f ∈ J_S^{a+1} for f ∈ J_S^a, a ≥ 1.

theorem IsLocalRing.mem_pow_succ_of_forall_pderiv_mem {k : Type u_1} [Field k] {R : Type u_2} [CommRing R] [Algebra k R] {ι : Type u_3} (x : ι → R) (pd : ι → Derivation k R R) (S : Finset ι) [DecidableEq ι] (hx : ∀ i ∈ S, ∀ j ∈ S, (pd i) (x j) = if i = j then 1 else 0) [CharZero k] {a : ℕ} (ha : 1 ≤ a) {f : R} (hf : f ∈ coordIdeal x S ^ a) (hd : ∀ i ∈ S, (pd i) f ∈ coordIdeal x S ^ a) : f ∈ coordIdeal x S ^ (a + 1)

If f ∈ J_S^a and all ∂_i f, i ∈ S, lie in J_S^a, then f ∈ J_S^{a+1} (a ≥ 1).

theorem IsLocalRing.mem_coordIdeal_pow_iff {k : Type u_1} [Field k] {R : Type u_2} [CommRing R] [Algebra k R] {ι : Type u_3} (x : ι → R) (pd : ι → Derivation k R R) (S : Finset ι) [DecidableEq ι] (hx : ∀ i ∈ S, ∀ j ∈ S, (pd i) (x j) = if i = j then 1 else 0) [CharZero k] (p : ℕ) (f : R) : f ∈ coordIdeal x S ^ p ↔ ∀ (l : List ι), (∀ i ∈ l, i ∈ S) → l.length < p → iterD pd l f ∈ coordIdeal x S

The Taylor criterion along S: f ∈ J_S^p iff every iterated derivative of f along fewer than p coordinates of S lies in J_S (the algebraic form of the order along a closed subspace, [BM97, Chapter I, §3]).