Taylor exponentials of locally nilpotent derivations

Let D be a derivation of a commutative algebra A over ℚ which is locally nilpotent: every element is killed by some iterate of D. Its Taylor exponential

exp D a = ∑ Dⁿ a / n!

is then a finite sum for each a, and it is an algebra endomorphism of A. No global nilpotence bound is needed, so the construction applies to the invariant vector fields of unipotent groups on their infinite-dimensional coordinate rings.

Multiplicativity comes from the general Leibniz rule Derivation.iterate_apply_mul, Dⁿ (a * b) = ∑ (n choose i) Dⁱ a Dⁿ⁻ⁱ b. After division by factorials it says that the Taylor expansion a ↦ ∑ (Dⁿ a / n!) Xⁿ is an algebra homomorphism into the polynomial ring A[X]; the Taylor exponential is its evaluation at X = 1.

If a locally nilpotent derivation maps an ideal into itself, so does its Taylor exponential. For the derivative d / dX of a polynomial ring, scaled by r, the Taylor exponential is the Taylor shift p ↦ p (X + r).

Main declarations

• Derivation.taylorExpPolynomial: the Taylor expansion a ↦ ∑ (Dⁿ a / n!) Xⁿ of a locally nilpotent derivation, as an algebra homomorphism into A[X].
• Derivation.taylorExp: the Taylor exponential of a locally nilpotent derivation, as an algebra homomorphism.
• Derivation.taylorExp_apply_eq_sum: any iterate killing a gives a finite expansion of taylorExp D a.
• Derivation.taylorExp_apply_eq_locallyNilpotentExp: the Taylor exponential is the exponential Module.End.locallyNilpotentExp of the underlying linear endomorphism.
• Derivation.taylorExp_apply_of_apply_eq_zero: the Taylor exponential fixes the elements killed by the derivation.
• Derivation.taylorExp_apply_mem: the Taylor exponential preserves every ideal mapped into itself by the derivation.
• Derivation.map_taylorExp: Taylor exponentials are natural for additive maps intertwining two derivations.
• Polynomial.taylorExp_smul_derivative': for the scaled derivative of a polynomial ring the Taylor exponential is Polynomial.taylorAlgHom.

References

• G. Freudenburg, Algebraic Theory of Locally Nilpotent Derivations, Encyclopaedia of Mathematical Sciences 136, Springer (2006), Chapter 1.

theorem Derivation.inv_factorial_smul_iterate_apply_mul {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommRing A] [Algebra R A] [Algebra ℚ A] (D : Derivation R A A) (n : ℕ) (a b : A) : (↑n.factorial)⁻¹ • (⇑D)^[n] (a * b) = ∑ ij ∈ Finset.antidiagonal n, (↑ij.1.factorial)⁻¹ • (⇑D)^[ij.1] a * (↑ij.2.factorial)⁻¹ • (⇑D)^[ij.2] b

The divided Leibniz rule: dividing the general Leibniz rule by n! removes the binomial coefficients.

noncomputable def Derivation.taylorExpPolynomial {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommRing A] [Algebra R A] [Algebra ℚ A] (D : Derivation R A A) (hD : ∀ (a : A), ∃ (n : ℕ), (⇑D)^[n] a = 0) : A →ₐ[R] Polynomial A

The Taylor expansion a ↦ ∑ (Dⁿ a / n!) Xⁿ of a locally nilpotent derivation D, an algebra homomorphism into A[X]. Its evaluation at X = 1 is the Taylor exponential.

@[simp]

theorem Derivation.coeff_taylorExpPolynomial {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommRing A] [Algebra R A] [Algebra ℚ A] (D : Derivation R A A) (hD : ∀ (a : A), ∃ (n : ℕ), (⇑D)^[n] a = 0) (a : A) (n : ℕ) : ((D.taylorExpPolynomial hD) a).coeff n = (↑n.factorial)⁻¹ • (⇑D)^[n] a

The coefficients of the Taylor expansion are the Taylor terms Dⁿ a / n!.

theorem Derivation.support_taylorExpPolynomial_subset_range {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommRing A] [Algebra R A] [Algebra ℚ A] (D : Derivation R A A) (hD : ∀ (a : A), ∃ (n : ℕ), (⇑D)^[n] a = 0) {a : A} {n : ℕ} (hn : (⇑D)^[n] a = 0) : ((D.taylorExpPolynomial hD) a).support ⊆ Finset.range n

Any iterate killing an element bounds the support of its Taylor expansion.

theorem Derivation.aeval_taylorExpPolynomial_eq_sum {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommRing A] [Algebra R A] [Algebra ℚ A] (D : Derivation R A A) (hD : ∀ (a : A), ∃ (n : ℕ), (⇑D)^[n] a = 0) (c : A) {a : A} {n : ℕ} (hn : (⇑D)^[n] a = 0) : (Polynomial.aeval c) ((D.taylorExpPolynomial hD) a) = ∑ i ∈ Finset.range n, c ^ i * (↑i.factorial)⁻¹ • (⇑D)^[i] a

Evaluating a Taylor expansion at any point gives a finite sum whenever an iterate kills the input.

noncomputable def Derivation.taylorExp {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommRing A] [Algebra R A] [Algebra ℚ A] (D : Derivation R A A) (hD : ∀ (a : A), ∃ (n : ℕ), (⇑D)^[n] a = 0) : A →ₐ[R] A

The Taylor exponential a ↦ ∑ Dⁿ a / n! of a locally nilpotent derivation D of a commutative ℚ-algebra. The sum is finite because some iterate of D kills a, and the map is an algebra endomorphism by the general Leibniz rule.

@[simp]

theorem Derivation.aeval_one_taylorExpPolynomial {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommRing A] [Algebra R A] [Algebra ℚ A] (D : Derivation R A A) (hD : ∀ (a : A), ∃ (n : ℕ), (⇑D)^[n] a = 0) (a : A) : (Polynomial.aeval 1) ((D.taylorExpPolynomial hD) a) = (D.taylorExp hD) a

The Taylor exponential is the evaluation of the Taylor expansion at X = 1.

theorem Derivation.taylorExp_apply_eq_sum {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommRing A] [Algebra R A] [Algebra ℚ A] (D : Derivation R A A) (hD : ∀ (a : A), ∃ (n : ℕ), (⇑D)^[n] a = 0) {a : A} {n : ℕ} (hn : (⇑D)^[n] a = 0) : (D.taylorExp hD) a = ∑ i ∈ Finset.range n, (↑i.factorial)⁻¹ • (⇑D)^[i] a

Finite expansion of the Taylor exponential. If D^[n] kills a, then the Taylor exponential of a is the sum of its first n Taylor terms.

theorem Derivation.taylorExp_apply_eq_locallyNilpotentExp {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommRing A] [Algebra R A] [Algebra ℚ A] (D : Derivation R A A) (hD : ∀ (a : A), ∃ (n : ℕ), (⇑D)^[n] a = 0) (a : A) : (D.taylorExp hD) a = (Module.End.locallyNilpotentExp ↑D ⋯) a

The Taylor exponential is the exponential of the underlying endomorphism. As a linear map, the Taylor exponential of D is Module.End.locallyNilpotentExp of the linear map underlying D, which is locally nilpotent since its powers are the iterates of D.

theorem Derivation.taylorExp_apply_of_apply_eq_zero {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommRing A] [Algebra R A] [Algebra ℚ A] (D : Derivation R A A) (hD : ∀ (a : A), ∃ (n : ℕ), (⇑D)^[n] a = 0) {a : A} (ha : D a = 0) : (D.taylorExp hD) a = a

Constants of the derivation are fixed by its Taylor exponential: if D kills a, then the Taylor exponential of D fixes a.

@[simp]

theorem Derivation.taylorExp_zero {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommRing A] [Algebra R A] [Algebra ℚ A] (hD : ∀ (a : A), ∃ (n : ℕ), (⇑0)^[n] a = 0) : taylorExp 0 hD = AlgHom.id R A

The Taylor exponential of the zero derivation is the identity.

theorem Derivation.taylorExp_apply_mem {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommRing A] [Algebra R A] [Algebra ℚ A] (D : Derivation R A A) (hD : ∀ (a : A), ∃ (n : ℕ), (⇑D)^[n] a = 0) {I : Ideal A} (hI : ∀ x ∈ I, D x ∈ I) {a : A} (ha : a ∈ I) : (D.taylorExp hD) a ∈ I

The Taylor exponential preserves stable ideals. If a locally nilpotent derivation maps an ideal into itself, so does its Taylor exponential.

theorem Derivation.map_taylorExp {R : Type u_1} [CommSemiring R] {A : Type u_2} [CommRing A] [Algebra R A] [Algebra ℚ A] (D : Derivation R A A) (hD : ∀ (a : A), ∃ (n : ℕ), (⇑D)^[n] a = 0) {R' : Type u_3} {B : Type u_4} [CommSemiring R'] [CommRing B] [Algebra R' B] [Algebra ℚ B] (D' : Derivation R' B B) (hD' : ∀ (b : B), ∃ (n : ℕ), (⇑D')^[n] b = 0) {F : Type u_5} [FunLike F A B] [AddMonoidHomClass F A B] (f : F) (hf : ∀ (a : A), f (D a) = D' (f a)) (a : A) : f ((D.taylorExp hD) a) = (D'.taylorExp hD') (f a)

Naturality of Taylor exponentials. An additive map intertwining two locally nilpotent derivations, possibly over different base rings, intertwines their Taylor exponentials.

theorem Polynomial.taylorExp_smul_derivative' {R : Type u_1} [CommRing R] [Algebra ℚ R] (r : R) : (r • derivative').taylorExp ⋯ = taylorAlgHom r

Taylor's formula for polynomials. Over a ℚ-algebra, the Taylor exponential of the scaled derivative r • d / dX is the Taylor shift p ↦ p (X + r).