Partial derivatives in a symmetric algebra

A linear form φ on a module M over a commutative semiring R extends uniquely to a derivation SymmetricAlgebra.pderiv φ of the symmetric algebra Sym M, sending each generator ι m to the scalar φ m. For the polynomial functions Sym(V*) on a vector space V, the derivative along the evaluation at v ∈ V is the directional derivative along v. In the coordinates of a basis b of M, the derivative along the coordinate form b.coord j is Mathlib's partial derivative MvPolynomial.pderiv j (SymmetricAlgebra.equivMvPolynomial_pderiv_coord).

Main definitions

• SymmetricAlgebra.pderiv: the derivative of Sym M along a linear form on M.

Main results

• SymmetricAlgebra.pderiv_map: the chain rule for the derivatives along linear forms.
• SymmetricAlgebra.pderiv_mem_homogeneousSubmodule: a derivative lowers degrees by one.
• SymmetricAlgebra.lift_pderiv_comp_of_map_eq_self: the scaled chain rule for a homogeneous fixed polynomial evaluated at an eigenpoint.
• SymmetricAlgebra.pderiv_eq_sum: a derivative along a linear form expands along the derivatives along the coordinate forms of a finite basis.
• SymmetricAlgebra.equivMvPolynomial_pderiv_coord: in coordinates, the derivatives along the coordinate forms are the partial derivatives of polynomials.

References

• J. E. Humphreys, Reflection Groups and Coxeter Groups, Cambridge University Press (1990), Chapter 3 (partial derivatives of polynomial functions).

noncomputable def SymmetricAlgebra.pderiv {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] : Module.Dual R M →ₗ[R] Derivation R (SymmetricAlgebra R M) (SymmetricAlgebra R M)

The derivative of Sym M along a linear form φ on M: the derivation sending each generator ι m to the scalar φ m. In the coordinates of a basis b of M, the derivative along the coordinate form b.coord j is the partial derivative in the variable b j.

@[simp]

theorem SymmetricAlgebra.pderiv_ι {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (φ : Module.Dual R M) (m : M) : (pderiv φ) ((ι R M) m) = (algebraMap R (SymmetricAlgebra R M)) (φ m)

The derivative along φ sends the generator ι m to the scalar φ m.

theorem SymmetricAlgebra.pderiv_map {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] (g : M →ₗ[R] N) (φ : Module.Dual R N) (p : SymmetricAlgebra R M) : (pderiv φ) ((map R g) p) = (map R g) ((pderiv (φ ∘ₗ g)) p)

The chain rule. Differentiating the image of p under the map induced by g : M → N along φ is the image of the derivative of p along φ ∘ g.

theorem SymmetricAlgebra.pderiv_mem_homogeneousSubmodule {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (φ : Module.Dual R M) {n : ℕ} {p : SymmetricAlgebra R M} (hp : p ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n) : (pderiv φ) p ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M (n - 1)

A derivative along a linear form lowers degrees by one: it sends the degree-n part of Sym M to the degree-(n - 1) part.

theorem SymmetricAlgebra.lift_pderiv_comp_of_map_eq_self {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (p : SymmetricAlgebra R M) {d : ℕ} (hp : p ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R M d) {g : M →ₗ[R] M} (hg : (map R g) p = p) (x : Module.Dual R M) {c : R} (hx : x ∘ₗ g = c • x) (φ : Module.Dual R M) : (lift x) ((pderiv φ) p) = c ^ (d - 1) * (lift x) ((pderiv (φ ∘ₗ g)) p)

The differential of a homogeneous fixed polynomial at an eigenpoint satisfies the scaled chain rule. No nonzero-Jacobian or invertibility hypothesis is needed here.

theorem SymmetricAlgebra.pderiv_eq_sum {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : Type u_3} [Fintype n] (b : Module.Basis n R M) (φ : Module.Dual R M) (p : SymmetricAlgebra R M) : (pderiv φ) p = ∑ j : n, (algebraMap R (SymmetricAlgebra R M)) (φ (b j)) * (pderiv (b.coord j)) p

A derivative along a linear form φ expands along the derivatives along the coordinate forms of a finite basis b, with coefficients the values φ (b j).

theorem SymmetricAlgebra.equivMvPolynomial_pderiv_coord {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : Type u_3} (b : Module.Basis n R M) (i : n) (p : SymmetricAlgebra R M) : (equivMvPolynomial b) ((pderiv (b.coord i)) p) = (MvPolynomial.pderiv i) ((equivMvPolynomial b) p)

In the coordinates of a basis b, the derivative along the coordinate form b.coord i is Mathlib's partial derivative MvPolynomial.pderiv i in the variable i.