Differential operators of finite order

Let A be a commutative R-algebra and M, N modules over A. Grothendieck's algebraic definition of differential operators uses only commutators with multiplication by elements of A. For an R-linear map D : M →ₗ[R] N and a : A, the commutator smulCommutator R a D is x ↦ D (a • x) - a • D x. The R-submodule differentialOperators R A M N m of operators of order at most m is defined recursively: order at most 0 means A-linear, and D has order at most m + 1 when every commutator smulCommutator R a D has order at most m.

For the algebra of smooth functions on a manifold acting on spaces of smooth sections of vector bundles, this is the classical characterisation of linear differential operators of order at most m by the vanishing of (m + 1)-fold commutators with multiplication by functions, and the iterated commutator [⋯[P, f], …, f] with m copies of f is m! times the principal symbol of P evaluated at df. This file develops the algebraic theory:

• mem_differentialOperators_iff_forall_list_prod: order at most m means that every (m + 1)-fold iterated commutator vanishes; the commutators with different elements commute (smulCommutator_comm).
• differentialOperators_mono and comp_mem_differentialOperators: the orders are increasing and add under composition, so the operators on M form a filtered ring (SetLike.GradedMonoid).
• Derivation.mem_differentialOperators_one and differentialOperatorsOneEquiv: an operator D : A →ₗ[R] M has order at most one exactly when D = δ + (· • m) for a derivation δ and m : M, and this splitting is unique, with m = D 1.
• AlgEquiv.conjDifferentialOperators: conjugation D ↦ e ∘ D ∘ e⁻¹ by an algebra isomorphism e : A ≃ B preserves the order of operators on the algebra itself.
• apply_mem_smul_top_of_mem_pow_smul_top: an operator of order at most m sends I ^ (m + 1) • M into I • N for every ideal I, so the value of D x modulo I depends only on x modulo I ^ (m + 1). For the vanishing ideal of a point this is the statement that a differential operator of order m factors through m-jets.
• smulCommutator_pow_comp_of_mem: the top iterated commutators of a composition multiply, ad_a ^ (m + k) (P ∘ Q) = (m + k).choose m • (ad_a ^ m P ∘ ad_a ^ k Q). Dividing by factorials over a ℚ-algebra, this is multiplicativity of principal symbols.
• derivative_comp_derivative_notMem_differentialOperators_one: the second derivative on R[X] does not have order one when 2 ≠ 0 in R, since [[∂², X], X] = 2.

References

• A. Grothendieck, Éléments de géométrie algébrique IV, Quatrième partie, §16.8.
• I. Kolář, P. W. Michor, J. Slovák, Natural Operations in Differential Geometry, §§12, 19.

Commutators with scalar multiplication

def TauCeti.smulCommutator (R : Type u_1) {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] (a : A) : Module.End R (M →ₗ[R] N)

The commutator x ↦ D (a • x) - a • D x of an R-linear map D : M →ₗ[R] N with multiplication by a : A, as an R-linear operator on M →ₗ[R] N.

@[simp]

theorem TauCeti.smulCommutator_apply_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] (a : A) (D : M →ₗ[R] N) (x : M) : ((smulCommutator R a) D) x = D (a • x) - a • D x

theorem TauCeti.smulCommutator_eq_lie {R : Type u_1} {A : Type u_2} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] (a : A) (D : Module.End R N) : (smulCommutator R a) D = ⁅D, (Algebra.lsmul R R N) a⁆

For endomorphisms, smulCommutator R a is the Lie bracket with multiplication by a in the associative algebra Module.End R N.

theorem TauCeti.apply_smul_eq_smulCommutator_add {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] (a : A) (D : M →ₗ[R] N) (x : M) : D (a • x) = ((smulCommutator R a) D) x + a • D x

@[simp]

theorem TauCeti.smulCommutator_eq_zero_iff {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] {a : A} {D : M →ₗ[R] N} : (smulCommutator R a) D = 0 ↔ ∀ (x : M), D (a • x) = a • D x

@[simp]

theorem TauCeti.smulCommutator_zero {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] : smulCommutator R 0 = 0

theorem TauCeti.smulCommutator_add {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] (a b : A) : smulCommutator R (a + b) = smulCommutator R a + smulCommutator R b

@[simp]

theorem TauCeti.smulCommutator_algebraMap {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] (r : R) : smulCommutator R ((algebraMap R A) r) = 0

@[simp]

theorem TauCeti.smulCommutator_one {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] : smulCommutator R 1 = 0

theorem TauCeti.smulCommutator_comm {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] (a b : A) (D : M →ₗ[R] N) : (smulCommutator R a) ((smulCommutator R b) D) = (smulCommutator R b) ((smulCommutator R a) D)

Commutators with multiplication by two elements commute: both iterated commutators equal x ↦ D ((a * b) • x) - a • D (b • x) - b • D (a • x) + (a * b) • D x.

theorem TauCeti.commute_smulCommutator {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] (a b : A) : Commute (smulCommutator R a) (smulCommutator R b)

theorem TauCeti.smulCommutator_mul {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] (a b : A) (D : M →ₗ[R] N) : (smulCommutator R (a * b)) D = a • (smulCommutator R b) D + b • (smulCommutator R a) D + (smulCommutator R b) ((smulCommutator R a) D)

The commutator with a product: [D, a * b] = a • [D, b] + b • [D, a] + [[D, a], b].

theorem TauCeti.smulCommutator_smul {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] (r : R) (a : A) : smulCommutator R (r • a) = r • smulCommutator R a

theorem TauCeti.smulCommutator_apply_smul {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] (a g : A) (D : M →ₗ[R] N) : (smulCommutator R a) (g • D) = g • (smulCommutator R a) D

The commutator with a commutes with multiplying the values of an operator by g : A.

theorem TauCeti.commute_smulCommutator_list_prod {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] {m : ℕ} (b : A) (a : Fin m → A) : Commute (smulCommutator R b) (List.ofFn fun (i : Fin m) => smulCommutator R (a i)).prod

An iterated commutator commutes with each further commutator.

theorem TauCeti.list_prod_smulCommutator_apply_smul {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] {m : ℕ} (a : Fin m → A) (g : A) (D : M →ₗ[R] N) : (List.ofFn fun (i : Fin m) => smulCommutator R (a i)).prod (g • D) = g • (List.ofFn fun (i : Fin m) => smulCommutator R (a i)).prod D

Iterated commutators commute with multiplying the values of an operator by g : A.

theorem TauCeti.smulCommutator_comp {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} {O : Type u_5} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] [AddCommGroup O] [Module A O] [Module R O] [IsScalarTower R A O] (a : A) (P : N →ₗ[R] O) (Q : M →ₗ[R] N) : (smulCommutator R a) (P ∘ₗ Q) = P ∘ₗ (smulCommutator R a) Q + (smulCommutator R a) P ∘ₗ Q

The Leibniz rule for commutators of a composition: [P ∘ Q, a] = P ∘ [Q, a] + [P, a] ∘ Q.

theorem TauCeti.smulCommutator_pow_comp {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} {O : Type u_5} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] [AddCommGroup O] [Module A O] [Module R O] [IsScalarTower R A O] (a : A) (P : N →ₗ[R] O) (Q : M →ₗ[R] N) (n : ℕ) : (smulCommutator R a ^ n) (P ∘ₗ Q) = ∑ ij ∈ Finset.antidiagonal n, n.choose ij.1 • (smulCommutator R a ^ ij.1) P ∘ₗ (smulCommutator R a ^ ij.2) Q

The general Leibniz rule for iterated commutators of a composition.

Adapted from LieModule.toEnd_pow_lie and LieAlgebra.ad_pow_lie in Mathlib.

The order filtration

def TauCeti.differentialOperators (R : Type u_1) (A : Type u_2) (M : Type u_3) (N : Type u_4) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] : ℕ → Submodule R (M →ₗ[R] N)

The R-submodule of differential operators M → N of order at most m, in the sense of Grothendieck: order at most 0 means commuting with multiplication by every a : A, and D has order at most m + 1 when every commutator smulCommutator R a D has order at most m.

theorem TauCeti.mem_differentialOperators_zero_iff_smulCommutator {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] {D : M →ₗ[R] N} : D ∈ differentialOperators R A M N 0 ↔ ∀ (a : A), (smulCommutator R a) D = 0

theorem TauCeti.mem_differentialOperators_zero_iff {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] {D : M →ₗ[R] N} : D ∈ differentialOperators R A M N 0 ↔ ∀ (a : A) (x : M), D (a • x) = a • D x

An operator has order at most 0 exactly when it is A-linear.

theorem TauCeti.mem_differentialOperators_succ_iff {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] {D : M →ₗ[R] N} {m : ℕ} : D ∈ differentialOperators R A M N (m + 1) ↔ ∀ (a : A), (smulCommutator R a) D ∈ differentialOperators R A M N m

theorem TauCeti.smulCommutator_mem_differentialOperators {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] {D : M →ₗ[R] N} {m : ℕ} (hD : D ∈ differentialOperators R A M N (m + 1)) (a : A) : (smulCommutator R a) D ∈ differentialOperators R A M N m

theorem TauCeti.smulCommutator_eq_zero_of_mem_differentialOperators_zero {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] {D : M →ₗ[R] N} (hD : D ∈ differentialOperators R A M N 0) (a : A) : (smulCommutator R a) D = 0

theorem LinearMap.restrictScalars_mem_differentialOperators_zero {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] (f : M →ₗ[A] N) : ↑R f ∈ TauCeti.differentialOperators R A M N 0

An A-linear map is a differential operator of order 0.

theorem TauCeti.differentialOperators_le_succ {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] (m : ℕ) : differentialOperators R A M N m ≤ differentialOperators R A M N (m + 1)

theorem TauCeti.differentialOperators_mono {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] : Monotone (differentialOperators R A M N)

theorem TauCeti.smul_mem_differentialOperators {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] (g : A) {D : M →ₗ[R] N} {m : ℕ} (hD : D ∈ differentialOperators R A M N m) : g • D ∈ differentialOperators R A M N m

Multiplying the values of a differential operator by g : A preserves its order.

theorem TauCeti.mem_differentialOperators_iff_forall_list_prod {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] {D : M →ₗ[R] N} {m : ℕ} : D ∈ differentialOperators R A M N m ↔ ∀ (a : Fin (m + 1) → A), (List.ofFn fun (i : Fin (m + 1)) => smulCommutator R (a i)).prod D = 0

A differential operator has order at most m exactly when all its (m + 1)-fold iterated commutators with multiplication by elements of A vanish.

theorem TauCeti.smulCommutator_pow_mem_differentialOperators {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] {D : M →ₗ[R] N} {m j : ℕ} (hD : D ∈ differentialOperators R A M N (m + j)) (a : A) : (smulCommutator R a ^ j) D ∈ differentialOperators R A M N m

theorem TauCeti.list_prod_smulCommutator_mem_differentialOperators {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] {D : M →ₗ[R] N} {m k : ℕ} (hD : D ∈ differentialOperators R A M N (k + m)) (a : Fin m → A) : (List.ofFn fun (i : Fin m) => smulCommutator R (a i)).prod D ∈ differentialOperators R A M N k

An m-fold iterated commutator lowers the order by m.

theorem TauCeti.smulCommutator_pow_eq_zero {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] {D : M →ₗ[R] N} {m j : ℕ} (hD : D ∈ differentialOperators R A M N m) (hj : m < j) (a : A) : (smulCommutator R a ^ j) D = 0

The j-fold commutator of an operator of order at most m vanishes when m < j.

theorem TauCeti.comp_mem_differentialOperators {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} {O : Type u_5} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] [AddCommGroup O] [Module A O] [Module R O] [IsScalarTower R A O] {P : N →ₗ[R] O} {Q : M →ₗ[R] N} {m k : ℕ} (hP : P ∈ differentialOperators R A N O m) (hQ : Q ∈ differentialOperators R A M N k) : P ∘ₗ Q ∈ differentialOperators R A M O (m + k)

Orders add under composition.

instance TauCeti.instGradedMonoidNatLinearMapIdSubmoduleDifferentialOperators (R : Type u_1) (A : Type u_2) (N : Type u_4) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] : SetLike.GradedMonoid (differentialOperators R A N N)

The differential operators on N form a filtered ring under composition.

theorem TauCeti.smulCommutator_pow_comp_of_mem {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} {O : Type u_5} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] [AddCommGroup O] [Module A O] [Module R O] [IsScalarTower R A O] {P : N →ₗ[R] O} {Q : M →ₗ[R] N} {m k : ℕ} (hP : P ∈ differentialOperators R A N O m) (hQ : Q ∈ differentialOperators R A M N k) (a : A) : (smulCommutator R a ^ (m + k)) (P ∘ₗ Q) = (m + k).choose m • (smulCommutator R a ^ m) P ∘ₗ (smulCommutator R a ^ k) Q

The top iterated commutators of a composition multiply: for P of order at most m and Q of order at most k, the (m + k)-fold commutator of P ∘ Q with a is (m + k).choose m times the composition of the m-fold commutator of P with the k-fold commutator of Q.

Locality: differential operators factor through jets

theorem TauCeti.apply_mem_smul_top_of_mem_pow_smul_top {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] [AddCommGroup N] [Module A N] [Module R N] [IsScalarTower R A N] {D : M →ₗ[R] N} {m : ℕ} (hD : D ∈ differentialOperators R A M N m) (I : Ideal A) {x : M} (hx : x ∈ I ^ (m + 1) • ⊤) : D x ∈ I • ⊤

A differential operator of order at most m sends I ^ (m + 1) • M into I • N. Thus the class of D x modulo I • N depends only on the class of x modulo I ^ (m + 1) • M.

First-order operators on the algebra

theorem Derivation.mem_differentialOperators_one {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommGroup M] [Module A M] [Module R M] [IsScalarTower R A M] (D : Derivation R A M) : ↑D ∈ TauCeti.differentialOperators R A A M 1

A derivation is a differential operator of order at most one: its commutator with multiplication by a is multiplication by D a.

def LinearMap.derivationOfMemDifferentialOperatorsOne {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommGroup M] [Module A M] [Module R M] [IsScalarTower R A M] (D : A →ₗ[R] M) (hD : D ∈ TauCeti.differentialOperators R A A M 1) : Derivation R A M

For D : A →ₗ[R] M of order at most one, f ↦ D f - f • D 1 is a derivation.

@[simp]

theorem LinearMap.derivationOfMemDifferentialOperatorsOne_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommGroup M] [Module A M] [Module R M] [IsScalarTower R A M] (D : A →ₗ[R] M) (hD : D ∈ TauCeti.differentialOperators R A A M 1) (f : A) : (D.derivationOfMemDifferentialOperatorsOne hD) f = D f - f • D 1

def TauCeti.differentialOperatorsOneEquiv (R : Type u_1) (A : Type u_2) (M : Type u_3) [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommGroup M] [Module A M] [Module R M] [IsScalarTower R A M] : ↥(differentialOperators R A A M 1) ≃ₗ[R] Derivation R A M × M

The first-order operators A → M are exactly the sums δ + (· • m) of a derivation δ and multiplication by m : M, with δ and m = D 1 determined by D.

@[simp]

theorem TauCeti.differentialOperatorsOneEquiv_apply_fst_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommGroup M] [Module A M] [Module R M] [IsScalarTower R A M] (D : ↥(differentialOperators R A A M 1)) (f : A) : ((differentialOperatorsOneEquiv R A M) D).1 f = ↑D f - f • ↑D 1

@[simp]

theorem TauCeti.differentialOperatorsOneEquiv_apply_snd {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommGroup M] [Module A M] [Module R M] [IsScalarTower R A M] (D : ↥(differentialOperators R A A M 1)) : ((differentialOperatorsOneEquiv R A M) D).2 = ↑D 1

@[simp]

theorem TauCeti.coe_differentialOperatorsOneEquiv_symm_apply {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommGroup M] [Module A M] [Module R M] [IsScalarTower R A M] (p : Derivation R A M × M) (f : A) : ↑((differentialOperatorsOneEquiv R A M).symm p) f = p.1 f + f • p.2

theorem TauCeti.mem_differentialOperators_one_iff {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommGroup M] [Module A M] [Module R M] [IsScalarTower R A M] {D : A →ₗ[R] M} : D ∈ differentialOperators R A A M 1 ↔ ∃ (δ : Derivation R A M), ∀ (f : A), D f = δ f + f • D 1

An operator D : A →ₗ[R] M has order at most one exactly when it is a derivation plus multiplication by D 1.

Transport along algebra isomorphisms

theorem AlgEquiv.smulCommutator_conj {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (e : A ≃ₐ[R] B) (a : A) (D : A →ₗ[R] A) : (TauCeti.smulCommutator R (e a)) (e.toLinearMap ∘ₗ D ∘ₗ e.symm.toLinearMap) = e.toLinearMap ∘ₗ (TauCeti.smulCommutator R a) D ∘ₗ e.symm.toLinearMap

Conjugating an operator D on A by an algebra isomorphism e : A ≃ B carries its commutator with a to the commutator of the conjugate with e a.

theorem AlgEquiv.conj_mem_differentialOperators {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (e : A ≃ₐ[R] B) {D : A →ₗ[R] A} {m : ℕ} (hD : D ∈ TauCeti.differentialOperators R A A A m) : e.toLinearMap ∘ₗ D ∘ₗ e.symm.toLinearMap ∈ TauCeti.differentialOperators R B B B m

Conjugation by an algebra isomorphism preserves the order of a differential operator.

theorem AlgEquiv.list_prod_smulCommutator_conj {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (e : A ≃ₐ[R] B) {m : ℕ} (a : Fin m → A) (D : A →ₗ[R] A) : (List.ofFn fun (i : Fin m) => TauCeti.smulCommutator R (e (a i))).prod (e.toLinearMap ∘ₗ D ∘ₗ e.symm.toLinearMap) = e.toLinearMap ∘ₗ (List.ofFn fun (i : Fin m) => TauCeti.smulCommutator R (a i)).prod D ∘ₗ e.symm.toLinearMap

Iterated commutators commute with conjugation by an algebra isomorphism e, the entries being transported by e.

def AlgEquiv.conjDifferentialOperators {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (e : A ≃ₐ[R] B) (m : ℕ) : ↥(TauCeti.differentialOperators R A A A m) ≃ₗ[R] ↥(TauCeti.differentialOperators R B B B m)

Conjugation D ↦ e ∘ D ∘ e⁻¹ by an algebra isomorphism e : A ≃ B, as a linear equivalence between the differential operators of order at most m on A and on B.

@[simp]

theorem AlgEquiv.coe_conjDifferentialOperators {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (e : A ≃ₐ[R] B) {m : ℕ} (D : ↥(TauCeti.differentialOperators R A A A m)) : ↑((e.conjDifferentialOperators m) D) = e.toLinearMap ∘ₗ ↑D ∘ₗ e.symm.toLinearMap

@[simp]

theorem AlgEquiv.conjDifferentialOperators_symm {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (e : A ≃ₐ[R] B) {m : ℕ} : (e.conjDifferentialOperators m).symm = e.symm.conjDifferentialOperators m

The second derivative on polynomials

theorem TauCeti.derivative_comp_derivative_mem_differentialOperators_two {R : Type u_1} [CommRing R] : Polynomial.derivative ∘ₗ Polynomial.derivative ∈ differentialOperators R (Polynomial R) (Polynomial R) (Polynomial R) 2

The second derivative on R[X] has order at most two, as a composition of two derivations.

theorem TauCeti.derivative_comp_derivative_notMem_differentialOperators_one {R : Type u_1} [CommRing R] (h : 2 ≠ 0) : Polynomial.derivative ∘ₗ Polynomial.derivative ∉ differentialOperators R (Polynomial R) (Polynomial R) (Polynomial R) 1

The second derivative on R[X] does not have order at most one when 2 ≠ 0 in R: its double commutator with multiplication by X sends 1 to 2.