mathlibdocumentation

data.mv_polynomial.derivation

Derivations of multivariate polynomials #

In this file we prove that a derivation of mv_polynomial σ R is determined by its values on all monomials mv_polynomial.X i. We also provide a constructor mv_polynomial.mk_derivation that builds a derivation from its values on X is and a linear equivalence mv_polynomial.equiv_derivation between σ → A and derivation (mv_polynomial σ R) A.

noncomputable def mv_polynomial.mk_derivationₗ {σ : Type u_1} (R : Type u_2) {A : Type u_3} [ A] [module R) A] (f : σ → A) :

The derivation on mv_polynomial σ R that takes value f i on X i, as a linear map. Use mv_polynomial.mk_derivation instead.

Equations
theorem mv_polynomial.mk_derivationₗ_monomial {σ : Type u_1} {R : Type u_2} {A : Type u_3} [ A] [module R) A] (f : σ → A) (s : σ →₀ ) (r : R) :
r) = r s.sum (λ (i : σ) (k : ), (mv_polynomial.monomial (s - 1)) k f i)
theorem mv_polynomial.mk_derivationₗ_C {σ : Type u_1} {R : Type u_2} {A : Type u_3} [ A] [module R) A] (f : σ → A) (r : R) :
= 0
theorem mv_polynomial.mk_derivationₗ_X {σ : Type u_1} {R : Type u_2} {A : Type u_3} [ A] [module R) A] (f : σ → A) (i : σ) :
= f i
@[simp]
theorem mv_polynomial.derivation_C {σ : Type u_1} {R : Type u_2} {A : Type u_3} [ A] [module R) A] (D : R) A) (a : R) :
D = 0
@[simp]
theorem mv_polynomial.derivation_C_mul {σ : Type u_1} {R : Type u_2} {A : Type u_3} [ A] [module R) A] (D : R) A) (a : R) (f : R) :
D * f) = a D f
theorem mv_polynomial.derivation_eq_on_supported {σ : Type u_1} {R : Type u_2} {A : Type u_3} [ A] [module R) A] {D₁ D₂ : R) A} {s : set σ} (h : s) {f : R} (hf : f ) :
D₁ f = D₂ f

If two derivations agree on X i, i ∈ s, then they agree on all polynomials from mv_polynomial.supported R s.

theorem mv_polynomial.derivation_eq_of_forall_mem_vars {σ : Type u_1} {R : Type u_2} {A : Type u_3} [ A] [module R) A] {D₁ D₂ : R) A} {f : R} (h : ∀ (i : σ), i f.varsD₁ = D₂ ) :
D₁ f = D₂ f
theorem mv_polynomial.derivation_eq_zero_of_forall_mem_vars {σ : Type u_1} {R : Type u_2} {A : Type u_3} [ A] [module R) A] {D : R) A} {f : R} (h : ∀ (i : σ), i f.varsD = 0) :
D f = 0
@[ext]
theorem mv_polynomial.derivation_ext {σ : Type u_1} {R : Type u_2} {A : Type u_3} [ A] [module R) A] {D₁ D₂ : R) A} (h : ∀ (i : σ), D₁ = D₂ ) :
D₁ = D₂
theorem mv_polynomial.leibniz_iff_X {σ : Type u_1} {R : Type u_2} {A : Type u_3} [ A] [module R) A] [ R) A] (D : →ₗ[R] A) (h₁ : D 1 = 0) :
(∀ (p q : R), D (p * q) = p D q + q D p) ∀ (s : σ →₀ ) (i : σ), D 1 * = D + D 1)
noncomputable def mv_polynomial.mk_derivation {σ : Type u_1} (R : Type u_2) {A : Type u_3} [ A] [module R) A] [ R) A] (f : σ → A) :
R) A

The derivation on mv_polynomial σ R that takes value f i on X i.

Equations
@[simp]
theorem mv_polynomial.mk_derivation_X {σ : Type u_1} (R : Type u_2) {A : Type u_3} [ A] [module R) A] [ R) A] (f : σ → A) (i : σ) :
= f i
theorem mv_polynomial.mk_derivation_monomial {σ : Type u_1} (R : Type u_2) {A : Type u_3} [ A] [module R) A] [ R) A] (f : σ → A) (s : σ →₀ ) (r : R) :
r) = r s.sum (λ (i : σ) (k : ), (mv_polynomial.monomial (s - 1)) k f i)
noncomputable def mv_polynomial.mk_derivation_equiv {σ : Type u_1} (R : Type u_2) {A : Type u_3} [ A] [module R) A] [ R) A] :
(σ → A) ≃ₗ[R] R) A

mv_polynomial.mk_derivation as a linear equivalence.

Equations